The abstract of the Mizar article:

Linear Combinations in Vector Space

by

Wojciech A. Trybulec

Received July 27, 1990

MML identifier: VECTSP_6

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, RLVECT_1, BINOP_1, VECTSP_1, LATTICES, FUNCT_1, FINSET_1,
      RELAT_1, BOOLE, ARYTM_1, RLVECT_2, FUNCT_2, SEQ_1, FINSEQ_4, RLSUB_1,
      CARD_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XCMPLX_0, XREAL_0, FINSET_1,
      FINSEQ_1, RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, NAT_1, CARD_1, STRUCT_0,
      RLVECT_1, VECTSP_1, FINSEQ_4, VECTSP_4, PRE_TOPC;
 constructors REAL_1, NAT_1, RLVECT_2, VECTSP_4, FINSEQ_4, PRE_TOPC, XREAL_0,
      MEMBERED, PARTFUN1, XBOOLE_0;
 clusters FUNCT_1, VECTSP_1, RLVECT_2, RELSET_1, STRUCT_0, PRE_TOPC, FINSET_1,
      ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

 reserve p,q,r for FinSequence,
         x,y,y1,y2 for set,
         i,k,n for Nat,
         GF for add-associative right_zeroed right_complementable
      Abelian associative left_unital distributive (non empty doubleLoopStr),
         V for Abelian add-associative right_zeroed right_complementable
      VectSp-like (non empty VectSpStr over GF),
         u,v,v1,v2,v3,w for Element of V,
         a,b for Element of GF,
         F,G,H for FinSequence of the carrier of V,
         A,B for Subset of V,
         f for Function of the carrier of V, the carrier of GF;

definition
  let GF be non empty ZeroStr; let V be non empty VectSpStr over GF;
 canceled 3;

  mode Linear_Combination of V ->
   Element of Funcs(the carrier of V, the carrier of GF) means
:: VECTSP_6:def 4
   ex T being finite Subset of V st
    for v being Element of V st not v in T holds it.v = 0.GF;
end;

reserve L,L1,L2,L3 for Linear_Combination of V;


definition let GF be non empty ZeroStr; let V be non empty VectSpStr over GF;
   let L be Linear_Combination of V;
 func Carrier(L) -> finite Subset of V equals
:: VECTSP_6:def 5
   {v where v is Element of V: L.v <> 0.GF};
end;

canceled 18;

theorem :: VECTSP_6:19
   x in Carrier(L) iff ex v st x = v & L.v <> 0.GF;

theorem :: VECTSP_6:20
 L.v = 0.GF iff not v in Carrier(L);

definition let GF be non empty ZeroStr; let V be non empty VectSpStr over GF;
 func ZeroLC(V) -> Linear_Combination of V means
:: VECTSP_6:def 6
   Carrier(it) = {};
end;

canceled;

theorem :: VECTSP_6:22
 ZeroLC(V).v = 0.GF;

definition let GF be non empty ZeroStr; let V be non empty VectSpStr over GF;
  let A be Subset of V;
 mode Linear_Combination of A -> Linear_Combination of V means
:: VECTSP_6:def 7
   Carrier(it) c= A;
end;

reserve l for Linear_Combination of A;

canceled 2;

theorem :: VECTSP_6:25
   A c= B implies l is Linear_Combination of B;

theorem :: VECTSP_6:26
 ZeroLC(V) is Linear_Combination of A;

theorem :: VECTSP_6:27
 for l being Linear_Combination of {}(the carrier of V) holds
  l = ZeroLC(V);

theorem :: VECTSP_6:28
   L is Linear_Combination of Carrier(L);

definition let GF be non empty LoopStr;
  let V be non empty VectSpStr over GF;
  let F be FinSequence of the carrier of V;
  let f be Function of the carrier of V, the carrier of GF;
 func f (#) F -> FinSequence of the carrier of V means
:: VECTSP_6:def 8
   len it = len F &
         for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;

canceled 3;

theorem :: VECTSP_6:32
 i in dom F & v = F.i implies (f (#) F).i = f.v * v;

theorem :: VECTSP_6:33
   f (#) <*>(the carrier of V) = <*>(the carrier of V);

theorem :: VECTSP_6:34
 f (#) <* v *> = <* f.v * v *>;

theorem :: VECTSP_6:35
 f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;

theorem :: VECTSP_6:36
   f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>;

theorem :: VECTSP_6:37
 f (#) (F ^ G) = (f (#) F) ^ (f (#) G);

definition let GF be non empty LoopStr;
           let V be non empty VectSpStr over GF;
           let L be Linear_Combination of V;
 assume  V is Abelian add-associative right_zeroed right_complementable;
 func Sum(L) -> Element of V means
:: VECTSP_6:def 9
   ex F being FinSequence of the carrier of V st
    F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;

canceled 2;

theorem :: VECTSP_6:40
   0.GF <> 1_ GF implies
 (A <> {} & A is lineary-closed iff for l holds Sum(l) in A);

theorem :: VECTSP_6:41
  Sum(ZeroLC(V)) = 0.V;

theorem :: VECTSP_6:42
   for l being Linear_Combination of {}(the carrier of V) holds
  Sum(l) = 0.V;

theorem :: VECTSP_6:43
 for l being Linear_Combination of {v} holds
  Sum(l) = l.v * v;

theorem :: VECTSP_6:44
 v1 <> v2 implies
  for l being Linear_Combination of {v1,v2} holds
    Sum(l) = l.v1 * v1 + l.v2 * v2;

theorem :: VECTSP_6:45
   Carrier(L) = {} implies Sum(L) = 0.V;

theorem :: VECTSP_6:46
   Carrier(L) = {v} implies Sum(L) = L.v * v;

theorem :: VECTSP_6:47
   Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2;

definition let GF be non empty ZeroStr;
           let V be non empty VectSpStr over GF;
           let L1,L2 be Linear_Combination of V;
 redefine pred L1 = L2 means
:: VECTSP_6:def 10
      for v being Element of V holds L1.v = L2.v;
end;

definition let GF; let V; let L1,L2;
 func L1 + L2 -> Linear_Combination of V means
:: VECTSP_6:def 11
   for v holds it.v = L1.v + L2.v;
end;

canceled 3;

theorem :: VECTSP_6:51
 Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: VECTSP_6:52
 L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 + L2 is Linear_Combination of A;

theorem :: VECTSP_6:53
 L1 + L2 = L2 + L1;

theorem :: VECTSP_6:54
   L1 + (L2 + L3) = L1 + L2 + L3;

theorem :: VECTSP_6:55
   L + ZeroLC(V) = L & ZeroLC(V) + L = L;

definition let GF; let V,a; let L;
 func a * L -> Linear_Combination of V means
:: VECTSP_6:def 12
   for v holds it.v = a * L.v;
end;

canceled 2;

theorem :: VECTSP_6:58
 Carrier(a * L) c= Carrier(L);

theorem :: VECTSP_6:59
 for GF being Field, V being VectSp of GF,
     a being Element of GF,
     L being Linear_Combination of V
  st a <> 0.GF holds Carrier(a * L) = Carrier(L);

theorem :: VECTSP_6:60
 0.GF * L = ZeroLC(V);

theorem :: VECTSP_6:61
 L is Linear_Combination of A implies a * L is Linear_Combination of A;

theorem :: VECTSP_6:62
   (a + b) * L = a * L + b * L;

theorem :: VECTSP_6:63
   a * (L1 + L2) = a * L1 + a * L2;

theorem :: VECTSP_6:64
 a * (b * L) = (a * b) * L;

theorem :: VECTSP_6:65
   1_ GF * L = L;

definition let GF; let V; let L;
 func - L -> Linear_Combination of V equals
:: VECTSP_6:def 13
   (- 1_ GF) * L;
 involutiveness;
end;

canceled;

theorem :: VECTSP_6:67
 (- L).v = - L.v;

theorem :: VECTSP_6:68
   L1 + L2 = ZeroLC(V) implies L2 = - L1;

theorem :: VECTSP_6:69
 Carrier(- L) = Carrier(L);

theorem :: VECTSP_6:70
 L is Linear_Combination of A implies - L is Linear_Combination of A;

definition let GF; let V; let L1,L2;
 func L1 - L2 -> Linear_Combination of V equals
:: VECTSP_6:def 14
   L1 + (- L2);
end;

canceled 2;

theorem :: VECTSP_6:73
 (L1 - L2).v = L1.v - L2.v;

theorem :: VECTSP_6:74
   Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: VECTSP_6:75
   L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 - L2 is Linear_Combination of A;

theorem :: VECTSP_6:76
 L - L = ZeroLC(V);

theorem :: VECTSP_6:77
 Sum(L1 + L2) = Sum(L1) + Sum(L2);

theorem :: VECTSP_6:78
   for GF being Field, V being VectSp of GF, L being Linear_Combination of V,
     a being Element of GF
 holds Sum(a * L) = a * Sum(L);

theorem :: VECTSP_6:79
 Sum(- L) = - Sum(L);

theorem :: VECTSP_6:80
   Sum(L1 - L2) = Sum(L1) - Sum(L2);

::
::  Auxiliary theorems.
::

theorem :: VECTSP_6:81
   (- 1_ GF) * a = - a;

theorem :: VECTSP_6:82
   for GF being Field holds - 1_ GF <> 0.GF;