:: VECTSP_3 semantic presentation

theorem Th1: :: VECTSP_3:1

canceled;

theorem Th2: :: VECTSP_3:2

canceled;

theorem Th3: :: VECTSP_3:3

canceled;

theorem Th4: :: VECTSP_3:4

canceled;

theorem Th5: :: VECTSP_3:5

canceled;

theorem Th6: :: VECTSP_3:6

canceled;

theorem Th7: :: VECTSP_3:7

canceled;

theorem Th8: :: VECTSP_3:8

canceled;

theorem Th9: :: VECTSP_3:9

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄, b₅ being FinSequence of the carrier of b₃ st len b₄ = len b₅ & ( for b₆ being Nat
for b₇ being Element of b₃ st b₆ in dom b₄ & b₇ = b₅ . b₆ holds
b₄ . b₆ = b₂ * b₇ ) holds
Sum b₄ = b₂ * (Sum b₅)

proof end;

theorem Th10: :: VECTSP_3:10

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄, b₅ being FinSequence of the carrier of b₃ st len b₄ = len b₅ & ( for b₆ being Nat st b₆ in dom b₄ holds
b₅ . b₆ = b₂ * (b₄ /. b₆) ) holds
Sum b₅ = b₂ * (Sum b₄)

proof end;

theorem Th11: :: VECTSP_3:11

canceled;

theorem Th12: :: VECTSP_3:12

canceled;

theorem Th13: :: VECTSP_3:13

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSpStr of b₁
for b₃, b₄, b₅ being FinSequence of the carrier of b₂ st len b₃ = len b₄ & len b₃ = len b₅ & ( for b₆ being Nat st b₆ in dom b₃ holds
b₅ . b₆ = (b₃ /. b₆) - (b₄ /. b₆) ) holds
Sum b₅ = (Sum b₃) - (Sum b₄)

proof end;

theorem Th14: :: VECTSP_3:14

canceled;

theorem Th15: :: VECTSP_3:15

canceled;

theorem Th16: :: VECTSP_3:16

canceled;

theorem Th17: :: VECTSP_3:17

canceled;

theorem Th18: :: VECTSP_3:18

canceled;

theorem Th19: :: VECTSP_3:19

canceled;

theorem Th20: :: VECTSP_3:20

canceled;

theorem Th21: :: VECTSP_3:21

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁ holds b₂ * (Sum (<*> the carrier of b₃)) = 0. b₃

proof end;

theorem Th22: :: VECTSP_3:22

canceled;

theorem Th23: :: VECTSP_3:23

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄, b₅ being Element of b₃ holds b₂ * (Sum <*b₄,b₅*>) = (b₂ * b₄) + (b₂ * b₅)

proof end;

theorem Th24: :: VECTSP_3:24

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄, b₅, b₆ being Element of b₃ holds b₂ * (Sum <*b₄,b₅,b₆*>) = ((b₂ * b₄) + (b₂ * b₅)) + (b₂ * b₆)

proof end;

theorem Th25: :: VECTSP_3:25

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

proof end;

theorem Th26: :: VECTSP_3:26

canceled;

theorem Th27: :: VECTSP_3:27

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds - (Sum <*b₂,b₃*>) = (- b₂) - b₃

proof end;

theorem Th28: :: VECTSP_3:28

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds - (Sum <*b₂,b₃,b₄*>) = ((- b₂) - b₃) - b₄

proof end;

theorem Th29: :: VECTSP_3:29

canceled;

theorem Th30: :: VECTSP_3:30

canceled;

theorem Th31: :: VECTSP_3:31

canceled;

theorem Th32: :: VECTSP_3:32

canceled;

theorem Th33: :: VECTSP_3:33

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

proof end;

theorem Th34: :: VECTSP_3:34

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( Sum <*b₂,(- b₃)*> = b₂ - b₃ & Sum <*(- b₃),b₂*> = b₂ - b₃ )

proof end;

theorem Th35: :: VECTSP_3:35

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( Sum <*(- b₂),(- b₃)*> = - (b₂ + b₃) & Sum <*(- b₃),(- b₂)*> = - (b₂ + b₃) )

proof end;