The abstract of the Mizar article:

Linear Combinations in Real Linear Space

by

Wojciech A. Trybulec

Received April 8, 1990

MML identifier: RLVECT_2

[ Mizar article, MML identifier index ]

environ

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


begin

scheme LambdaSep1{D, R() -> non empty set, A() -> Element of D(),
                  B() -> Element of R(), F(set) -> Element of R()}:
 ex f being Function of D(),R() st
  f.A() = B() & for x being Element of D() st x <> A() holds f.x = F(x);

scheme LambdaSep2{D, R() -> non empty set, A1, A2() -> Element of D(),
                  B1, B2() -> Element of R(), F(set) -> Element of R()}:
 ex f being Function of D(),R() st
  f.A1() = B1() & f.A2() = B2() &
   for x being Element of D() st x <> A1() & x <> A2() holds f.x = F(x)
 provided
   A1() <> A2();

reserve X,Y,x,y,y1,y2 for set,
        p for FinSequence,
        i,j,k,l,n for Nat,
        V for RealLinearSpace,
        u,v,v1,v2,v3,w for VECTOR of V,
        a,b for Real,

        F,G,H1,H2 for FinSequence of the carrier of V,
        A,B for Subset of V,
        f for Function of the carrier of V, REAL;

definition let S be 1-sorted; let x;
 assume  x in S;
 func vector(S,x) -> Element of S equals
:: RLVECT_2:def 1
   x;
end;

canceled 2;

theorem :: RLVECT_2:3
 for S being non empty 1-sorted,v being Element of S
   holds vector(S,v) = v;

theorem :: RLVECT_2:4
 for V being Abelian add-associative right_zeroed right_complementable
                     (non empty LoopStr),
     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);

theorem :: RLVECT_2:5
   len F = len G &
  (for k st k in dom F holds G.k = a * F/.k) implies
   Sum(G) = a * Sum(F);

theorem :: RLVECT_2:6
 for V being Abelian add-associative right_zeroed right_complementable
                     (non empty LoopStr),
     F,G being FinSequence of the carrier of V st
 len F = len G & (for k st k in dom F holds G.k = - F/.k) holds
   Sum(G) = - Sum(F);

theorem :: RLVECT_2:7
   for V being Abelian add-associative right_zeroed right_complementable
                     (non empty LoopStr),
     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);

theorem :: RLVECT_2:8
 for V being Abelian add-associative right_zeroed right_complementable
                     (non empty LoopStr),
     F,G being FinSequence of the carrier of V
 for f being Permutation of dom F st
  len F = len G & (for i st i in dom G holds G.i = F.(f.i)) holds
   Sum(F) = Sum(G);

theorem :: RLVECT_2:9
   for V being Abelian add-associative right_zeroed right_complementable
           (non empty LoopStr),
     F,G being FinSequence of the carrier of V
 for f being Permutation of dom F st G = F * f holds
  Sum(F) = Sum(G);

definition let V be 1-sorted;
 cluster empty finite Subset of V;
end;



definition let V be 1-sorted; let S,T be finite Subset of V;
 redefine func S \/ T -> finite Subset of V;
  func S /\ T -> finite Subset of V;
  func S \ T -> finite Subset of V;
  func S \+\ T -> finite Subset of V;
end;

definition let V be non empty LoopStr,
               T be finite Subset of V;
 assume V is Abelian add-associative right_zeroed;
 canceled 2;

 func Sum(T) -> Element of V means
:: RLVECT_2:def 4
   ex F be FinSequence of the carrier of V st
    rng F = T & F is one-to-one & it = Sum(F);
end;

definition let V be non empty 1-sorted;
 cluster non empty finite Subset of V;
end;

definition let V be non empty 1-sorted; let v be Element of V;
 redefine func {v} -> finite Subset of V;
end;

definition let V be non empty 1-sorted;
 let v1,v2 be Element of V;
 redefine func {v1,v2} -> finite Subset of V;
end;

definition let V be non empty 1-sorted;
 let v1,v2,v3 be Element of V;
 redefine func {v1,v2,v3} -> finite Subset of V;
end;

canceled 4;

theorem :: RLVECT_2:14
 for V be Abelian add-associative right_zeroed (non empty LoopStr) holds
  Sum({}V) = 0.V;

theorem :: RLVECT_2:15
   for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     v be Element of V holds
   Sum{v} = v;

theorem :: RLVECT_2:16
   for V be Abelian add-associative right_zeroed right_complementable
  (non empty LoopStr),
     v1,v2 be Element of V holds
 v1 <> v2 implies Sum{v1,v2} = v1 + v2;

theorem :: RLVECT_2:17
   for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     v1,v2,v3 be Element of V holds
 v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3;

theorem :: RLVECT_2:18
 for V be Abelian add-associative right_zeroed (non empty LoopStr),
     S,T be finite Subset of V holds
 T misses S implies Sum(T \/ S) = Sum(T) + Sum(S);

theorem :: RLVECT_2:19
 for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S);

theorem :: RLVECT_2:20
   for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S);

theorem :: RLVECT_2:21
 for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T \ S) = Sum(T \/ S) - Sum(S);

theorem :: RLVECT_2:22
 for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T \ S) = Sum(T) - Sum(T /\ S);

theorem :: RLVECT_2:23
   for V be Abelian add-associative right_zeroed right_complementable
   (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S);

theorem :: RLVECT_2:24
   for V be Abelian add-associative right_zeroed (non empty LoopStr),
     S,T be finite Subset of V holds
 Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T);

definition let V be non empty ZeroStr;
 mode Linear_Combination of V -> Element of Funcs(the carrier of V, REAL) means
:: RLVECT_2:def 5
 ex T being finite Subset of V st
  for v being Element of V st not v in T holds it.v = 0;
end;

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

definition let V be non empty LoopStr, L be Linear_Combination of V;
 func Carrier(L) -> finite Subset of V equals
:: RLVECT_2:def 6
   {v where v is Element of V : L.v <> 0};
end;

canceled 3;

theorem :: RLVECT_2:28
  for V be non empty LoopStr, L be Linear_Combination of V,
      v be Element of V holds
    L.v = 0 iff not v in Carrier(L);

definition let V be non empty LoopStr;
 func ZeroLC(V) -> Linear_Combination of V means
:: RLVECT_2:def 7
   Carrier (it) = {};
end;

canceled;

theorem :: RLVECT_2:30
 for V be non empty LoopStr, v be Element of V holds
 ZeroLC(V).v = 0;

definition let V be non empty LoopStr; let A be Subset of V;
 mode Linear_Combination of A -> Linear_Combination of V means
:: RLVECT_2:def 8
   Carrier (it) c= A;
end;

reserve l,l1,l2 for Linear_Combination of A;

canceled 2;

theorem :: RLVECT_2:33
   A c= B implies l is Linear_Combination of B;

theorem :: RLVECT_2:34
 ZeroLC(V) is Linear_Combination of A;

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

definition let V; let F; let f;
 func f (#) F -> FinSequence of the carrier of V means
:: RLVECT_2:def 9
   len it = len F &
         for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;

canceled 4;

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

theorem :: RLVECT_2:41
   f (#) <*>(the carrier of V) = <*>(the carrier of V);

theorem :: RLVECT_2:42
 f (#) <* v *> = <* f.v * v *>;

theorem :: RLVECT_2:43
 f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;

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

definition let V; let L;
 func Sum(L) -> Element of V means
:: RLVECT_2:def 10
   ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;

canceled 2;

theorem :: RLVECT_2:47
   A <> {} & A is lineary-closed iff for l holds Sum(l) in A;

theorem :: RLVECT_2:48
   Sum(ZeroLC(V)) = 0.V;

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

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

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

theorem :: RLVECT_2:52
   Carrier(L) = {} implies Sum(L) = 0.V;

theorem :: RLVECT_2:53
   Carrier(L) = {v} implies Sum(L) = L.v * v;

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

definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V;
 redefine pred L1 = L2 means
:: RLVECT_2:def 11
      for v being Element of V holds L1.v = L2.v;
end;

definition let V be non empty LoopStr; let L1,L2 be Linear_Combination of V;
 func L1 + L2 -> Linear_Combination of V means
:: RLVECT_2:def 12
   for v being Element of V holds it.v = L1.v + L2.v;
end;

canceled 3;

theorem :: RLVECT_2:58
 Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: RLVECT_2:59
 L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 + L2 is Linear_Combination of A;

theorem :: RLVECT_2:60
  for V be non empty LoopStr, L1,L2 be Linear_Combination of V holds
    L1 + L2 = L2 + L1;

theorem :: RLVECT_2:61
 L1 + (L2 + L3) = L1 + L2 + L3;

theorem :: RLVECT_2:62
 L + ZeroLC(V) = L & ZeroLC(V) + L = L;

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

canceled 2;

theorem :: RLVECT_2:65
 a <> 0 implies Carrier(a * L) = Carrier(L);

theorem :: RLVECT_2:66
 0 * L = ZeroLC(V);

theorem :: RLVECT_2:67
 L is Linear_Combination of A implies a * L is Linear_Combination of A;

theorem :: RLVECT_2:68
 (a + b) * L = a * L + b * L;

theorem :: RLVECT_2:69
 a * (L1 + L2) = a * L1 + a * L2;

theorem :: RLVECT_2:70
 a * (b * L) = (a * b) * L;

theorem :: RLVECT_2:71
 1 * L = L;

definition let V,L;
 func - L -> Linear_Combination of V equals
:: RLVECT_2:def 14
   (- 1) * L;
end;

canceled;

theorem :: RLVECT_2:73
 (- L).v = - L.v;

theorem :: RLVECT_2:74
   L1 + L2 = ZeroLC(V) implies L2 = - L1;

theorem :: RLVECT_2:75
 Carrier(- L) = Carrier(L);

theorem :: RLVECT_2:76
 L is Linear_Combination of A implies - L is Linear_Combination of A;

theorem :: RLVECT_2:77
   - (- L) = L;

definition let V; let L1,L2;
 func L1 - L2 -> Linear_Combination of V equals
:: RLVECT_2:def 15
   L1 + (- L2);
end;

canceled;

theorem :: RLVECT_2:79
 (L1 - L2).v = L1.v - L2.v;

theorem :: RLVECT_2:80
   Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);

theorem :: RLVECT_2:81
   L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 - L2 is Linear_Combination of A;

theorem :: RLVECT_2:82
 L - L = ZeroLC(V);

definition let V;
 func LinComb(V) -> set means
:: RLVECT_2:def 16
   x in it iff x is Linear_Combination of V;
end;

definition let V;
 cluster LinComb(V) -> non empty;
end;

reserve e,e1,e2 for Element of LinComb(V);

definition let V; let e;
 func @e -> Linear_Combination of V equals
:: RLVECT_2:def 17
   e;
end;

definition let V; let L;
 func @L -> Element of LinComb(V) equals
:: RLVECT_2:def 18
   L;
end;

definition let V;
 func LCAdd(V) -> BinOp of LinComb(V) means
:: RLVECT_2:def 19
   for e1,e2 holds it.(e1,e2) = @e1 + @e2;
end;

definition let V;
 func LCMult(V) -> Function of [:REAL,LinComb(V):], LinComb(V) means
:: RLVECT_2:def 20
   for a,e holds it.[a,e] = a * @e;
end;

definition let V;
 func LC_RLSpace(V) -> RealLinearSpace equals
:: RLVECT_2:def 21
   RLSStruct (# LinComb(V), @ZeroLC(V), LCAdd(V), LCMult(V) #);
end;

definition let V;
 cluster LC_RLSpace(V) -> strict non empty;
end;

canceled 9;

theorem :: RLVECT_2:92
 the carrier of LC_RLSpace(V) = LinComb(V);

theorem :: RLVECT_2:93
   the Zero of LC_RLSpace(V) = ZeroLC(V);

theorem :: RLVECT_2:94
 the add of LC_RLSpace(V) = LCAdd(V);

theorem :: RLVECT_2:95
 the Mult of LC_RLSpace(V) = LCMult(V);

theorem :: RLVECT_2:96
 vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = L1 + L2;

theorem :: RLVECT_2:97
 a * vector(LC_RLSpace(V),L) = a * L;

theorem :: RLVECT_2:98
 - vector(LC_RLSpace(V),L) = - L;

theorem :: RLVECT_2:99
   vector(LC_RLSpace(V),L1) - vector(LC_RLSpace(V),L2) = L1 - L2;

definition let V; let A;
 func LC_RLSpace(A) -> strict Subspace of LC_RLSpace(V) means
:: RLVECT_2:def 22
     the carrier of it = {l : not contradiction};
end;

canceled 3;

theorem :: RLVECT_2:103
   k < n implies n - 1 is Nat;

canceled 3;

theorem :: RLVECT_2:107
   X is finite & Y is finite implies X \+\ Y is finite;

theorem :: RLVECT_2:108
   for f being Function st
  f " X = f " Y & X c= rng f & Y c= rng f holds X = Y;