:: Linear Combinations in Real Linear Space
::  by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, REAL_1, STRUCT_0, FUNCT_1,
      XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4,
      XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1,
      FUNCOP_1, VALUED_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, RLVECT_2,
      LATTICES, VECTSP_1, PRE_POLY, FUNCT_7;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1,
      NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1,
      RELSET_1, PRE_POLY, PARTFUN1, FUNCT_2, FUNCOP_1, DOMAIN_1, VALUED_1,
      FINSEQ_4, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REAL_1,
      RLSUB_1, NAT_1, BINOP_1, XXREAL_0;
 constructors PARTFUN1, BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1,
      FINSEQ_4, RLSUB_1, VALUED_1, RELSET_1, VECTSP_1, PRE_POLY, RLVECT_1,
      NUMBERS, GROUP_1;
 registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
      XREAL_0, STRUCT_0, RLVECT_1, RLSUB_1, VALUED_1, VALUED_0, MEMBERED,
      FINSEQ_1, CARD_1, VECTSP_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x,y,y1,y2 for set,
  p for FinSequence,
  i,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 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;

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

theorem :: RLVECT_2:2
  for V being Abelian add-associative right_zeroed
  right_complementable non empty addLoopStr, 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:3
  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:4
  for V being Abelian add-associative right_zeroed
  right_complementable non empty addLoopStr, 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:5
  for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, 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:6
  for V being Abelian add-associative right_zeroed
  right_complementable non empty addLoopStr, 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:7
  for V being Abelian add-associative right_zeroed right_complementable
  non empty addLoopStr, 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 non empty addLoopStr, T be finite Subset of V;
  assume
 V is Abelian add-associative right_zeroed;

  func Sum(T) -> Element of V means
:: RLVECT_2:def 2

  ex F be FinSequence of the carrier of V st rng F = T & F is one-to-one &
  it = Sum(F);
end;

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

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

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

theorem :: RLVECT_2:11
  for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, 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:12
  for V be Abelian add-associative right_zeroed non empty
  addLoopStr, S,T be finite Subset of V holds T misses S implies Sum(T \/ S) =
  Sum(T) + Sum(S);

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

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

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

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

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

theorem :: RLVECT_2:18
  for V be Abelian add-associative right_zeroed non empty addLoopStr,
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 3

    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;

notation
  let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
  synonym Carrier L for support L;
end;

definition
  let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
  redefine func Carrier(L) -> Subset of V equals
:: RLVECT_2:def 4
  {v where v is Element of V : L.v <> 0};
end;

registration
  let V be non empty addLoopStr, L be Linear_Combination of V;
  cluster Carrier(L) -> finite;
end;

theorem :: RLVECT_2:19
  for V be non empty addLoopStr, 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 addLoopStr;
  func ZeroLC(V) -> Linear_Combination of V means
:: RLVECT_2:def 5

  Carrier (it) = {};
end;

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

definition
  let V be non empty addLoopStr;
  let A be Subset of V;
  mode Linear_Combination of A -> Linear_Combination of V means
:: RLVECT_2:def 6

    Carrier (it) c= A;
end;

reserve l,l1,l2 for Linear_Combination of A;

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

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

theorem :: RLVECT_2:23
  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 7

  len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;

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

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

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

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

theorem :: RLVECT_2:28
  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 8

  ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;

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

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

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

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

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

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

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

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

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

definition
  let V be non empty addLoopStr;
  let L1,L2 be Linear_Combination of V;
  redefine func L1 + L2 -> Linear_Combination of V means
:: RLVECT_2:def 10

  for v being Element of V holds it.v = L1.v + L2.v;
end;

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

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

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

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

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

definition
  let V;
  let a be Real;
  let L;
  func a * L -> Linear_Combination of V means
:: RLVECT_2:def 11

  for v holds it.v = a * L.v;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

definition
  let V;
  func LinComb(V) -> set means
:: RLVECT_2:def 14

  x in it iff x is Linear_Combination of V;
end;

registration
  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 15
  e;
end;

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

definition
  let V;
  func LCAdd(V) -> BinOp of LinComb(V) means
:: RLVECT_2:def 17

  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 18

  for a,e holds it.[a,e] = a * @e;
end;

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

registration
  let V;
  cluster LC_RLSpace V -> strict non empty;
end;

registration
  let V;
  cluster LC_RLSpace V -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

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

theorem :: RLVECT_2:59
  0.LC_RLSpace(V) = ZeroLC(V);

theorem :: RLVECT_2:60
  the addF of LC_RLSpace(V) = LCAdd(V);

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

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

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

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

theorem :: RLVECT_2:65
  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 20
  the carrier of it = the set of all l ;
end;

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

theorem :: RLVECT_2:66
  for R being add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive non empty doubleLoopStr,
      a being
  Element of R for V being Abelian add-associative right_zeroed
  right_complementable vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty ModuleStr over R, F,G being
FinSequence 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 :: RLVECT_2:67
  for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
  of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, F,G being FinSequence 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);

theorem :: RLVECT_2:68
  for R being add-associative right_zeroed right_complementable Abelian
  associative well-unital distributive non empty doubleLoopStr for V being
Abelian add-associative right_zeroed right_complementable non empty ModuleStr
over R, F,G,H being FinSequence 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:69
  for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
  of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R holds a * Sum(<*>(the carrier of V)) =
  0.V;

theorem :: RLVECT_2:70
  for R being add-associative right_zeroed right_complementable Abelian
    associative well-unital distributive non empty doubleLoopStr,
  a being Element of R
  for V being Abelian add-associative right_zeroed right_complementable
    vector-distributive scalar-distributive scalar-associative scalar-unital
 non empty ModuleStr over R, v,u being Element of V holds a * Sum
  <* v,u *> = a * v + a * u;

theorem :: RLVECT_2:71
  for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
  of R for V being Abelian add-associative right_zeroed right_complementable
  vector-distributive scalar-distributive scalar-associative scalar-unital
   non empty ModuleStr over R, v,u,w being Element of V holds a *
  Sum<* v,u,w *> = a * v + a * u + a * w;