Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Finite Sums of Vectors in Vector Space

**by****Wojciech A. Trybulec**- Received July 12, 1990
- 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);

Back to top