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);