:: VECTSP_3 semantic presentation

theorem :: VECTSP_3:1

canceled;

theorem :: VECTSP_3:2

canceled;

theorem :: VECTSP_3:3

canceled;

theorem :: VECTSP_3:4

canceled;

theorem :: VECTSP_3:5

canceled;

theorem :: VECTSP_3:6

canceled;

theorem :: VECTSP_3:7

canceled;

theorem :: VECTSP_3:8

canceled;

theorem Th9: :: VECTSP_3:9

for R being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for a being Element of R
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of R
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)

proof end;

theorem :: VECTSP_3:10

for R being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for a being Element of R
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of R
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)

proof end;

theorem :: VECTSP_3:11

canceled;

theorem :: VECTSP_3:12

canceled;

theorem :: VECTSP_3:13

for R being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty Abelian add-associative right_zeroed right_complementable VectSpStr of R
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)

proof end;

theorem :: VECTSP_3:14

canceled;

theorem :: VECTSP_3:15

canceled;

theorem :: VECTSP_3:16

canceled;

theorem :: VECTSP_3:17

canceled;

theorem :: VECTSP_3:18

canceled;

theorem :: VECTSP_3:19

canceled;

theorem :: VECTSP_3:20

canceled;

theorem :: VECTSP_3:21

proof end;

theorem :: VECTSP_3:22

canceled;

theorem :: VECTSP_3:23

for R being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for a being Element of R
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of R
for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)

proof end;

theorem :: VECTSP_3:24

for R being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for a being Element of R
for V being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)

proof end;

theorem :: VECTSP_3:25

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds - (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: VECTSP_3:26

canceled;

theorem :: VECTSP_3:27

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u

proof end;

theorem :: VECTSP_3:28

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for v, u, w being Element of V holds - (Sum <*v,u,w*>) = ((- v) - u) - w

proof end;

theorem :: VECTSP_3:29

canceled;

theorem :: VECTSP_3:30

canceled;

theorem :: VECTSP_3:31

canceled;

theorem :: VECTSP_3:32

canceled;

theorem :: VECTSP_3:33

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for v being Element of V holds
( Sum <*v,(- v)*> = 0. V & Sum <*(- v),v*> = 0. V )

proof end;

theorem :: VECTSP_3:34

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for v, w being Element of V holds
( Sum <*v,(- w)*> = v - w & Sum <*(- w),v*> = v - w )

proof end;

theorem :: VECTSP_3:35

for V being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for v, w being Element of V holds
( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )

proof end;