:: Finite Sums of Vectors in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 12, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

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 right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed VectSp-like VectSpStr of R
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of 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 right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed VectSp-like VectSpStr of R
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of 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 right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable Abelian add-associative right_zeroed 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 Element of 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

for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed VectSp-like VectSpStr of R holds a * (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: VECTSP_3:22

canceled;

theorem :: VECTSP_3:23

for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed 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 right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed 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 right_complementable Abelian add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V

proof end;

theorem :: VECTSP_3:26

canceled;

theorem :: VECTSP_3:27

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

proof end;

theorem :: VECTSP_3:28

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
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 right_complementable Abelian add-associative right_zeroed addLoopStr
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 right_complementable Abelian add-associative right_zeroed addLoopStr
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 right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds
( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )

proof end;