Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Finite Sums of Vectors in Vector Space

by
Wojciech A. Trybulec

MML identifier: VECTSP_3
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, FINSEQ_1, RELAT_1, FUNCT_1, FINSEQ_4, BINOP_1, VECTSP_1,
LATTICES, ARYTM_1;
notation TARSKI, XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, STRUCT_0, RLVECT_1,
VECTSP_1, FINSEQ_4, NAT_1;
constructors VECTSP_1, FINSEQ_4, NAT_1, XREAL_0, MEMBERED, XBOOLE_0;
clusters VECTSP_1, RELSET_1, STRUCT_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;

begin

reserve x,y for set,
k,n for Nat;

canceled 8;

theorem :: VECTSP_3:9
for R being add-associative right_zeroed right_complementable Abelian
associative left_unital distributive (non empty doubleLoopStr),
a being Element of R
for V being Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr over R),
F,G being FinSequence of the carrier of V
st len F = len G &
for k 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);

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

canceled 2;

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

canceled 7;

theorem :: VECTSP_3:21
for R being add-associative right_zeroed right_complementable Abelian
associative left_unital distributive (non empty doubleLoopStr),
a being Element of R
for V being Abelian add-associative right_zeroed
right_complementable VectSp-like (non empty VectSpStr over R)
holds a * Sum(<*>(the carrier of V)) = 0.V;

canceled;

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

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

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

canceled;

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

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

canceled 4;

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

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

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

```