:: Linear Combinations in Vector Space
::  by Wojciech A. Trybulec
::
:: Received July 27, 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, ALGSTR_0, BINOP_1,
      VECTSP_1, LATTICES, XBOOLE_0, STRUCT_0, FUNCT_1, RLVECT_2, FUNCT_2,
      FINSET_1, SUPINF_2, FUNCOP_1, TARSKI, VALUED_1, NAT_1, RELAT_1, PARTFUN1,
      XXREAL_0, CARD_1, ORDINAL4, ARYTM_3, CARD_3, MESFUNC1, RLSUB_1, ARYTM_1,
      FINSEQ_4;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XXREAL_0, FINSET_1, PARTFUN1, FINSEQ_1, RELAT_1, FUNCT_1,
      FUNCT_2, FUNCOP_1, NAT_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1,
      GROUP_1, VECTSP_1, FINSEQ_4, VFUNCT_1, VECTSP_4;
 constructors PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, MEMBERED,
      FINSEQ_4, VECTSP_4, RELSET_1, VFUNCT_1;
 registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, MEMBERED, STRUCT_0,
      VECTSP_1, XXREAL_0, CARD_1, FINSEQ_1, XCMPLX_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

reserve p,q,r for FinSequence,
  x,y,y1,y2 for set,
  i,k for Element of NAT,
  GF for add-associative right_zeroed right_complementable Abelian associative
  well-unital distributive non empty doubleLoopStr,
  V for Abelian
  add-associative right_zeroed right_complementable vector-distributive
  scalar-distributive scalar-associative scalar-unital
   non empty ModuleStr over GF,
  u,v,v1,v2,v3,w for Element of V,
  a,b for Element of GF,
  F,G ,H for FinSequence of V,
  A,B for Subset of V,
  f for Function of V, GF;

definition
  let GF be non empty ZeroStr;
  let V be non empty ModuleStr over GF;

  mode Linear_Combination of V ->
       Element of Funcs(the carrier of V, the carrier of GF) means
:: VECTSP_6:def 1

  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 ModuleStr over GF;
  let L be Linear_Combination of V;
  func Carrier(L) -> finite Subset of V equals
:: VECTSP_6:def 2
  {v where v is Element of V: L.v <> 0.GF};
end;

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

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

definition
  let GF be non empty ZeroStr;
  let V be non empty ModuleStr over GF;
  func ZeroLC(V) -> Linear_Combination of V means
:: VECTSP_6:def 3

  Carrier(it) = {};
end;

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

definition
  let GF be non empty ZeroStr;
  let V be non empty ModuleStr over GF;
  let A be Subset of V;
  mode Linear_Combination of A -> Linear_Combination of V means
:: VECTSP_6:def 4

    Carrier (it) c= A;
end;

reserve l for Linear_Combination of A;

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

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

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

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

definition
  let GF be non empty addLoopStr;
  let V be non empty ModuleStr over GF;
  let F be FinSequence of the carrier of V;
  let f be Function of V, GF;
  func f (#) F -> FinSequence of V means
:: VECTSP_6:def 5

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

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

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

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

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

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

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

definition
  let GF be non empty addLoopStr;
  let V be non empty ModuleStr 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 6

  ex F being FinSequence of the carrier of V st
  F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;

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

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

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

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

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

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

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

theorem :: VECTSP_6:21
  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 ModuleStr over GF;
  let L1,L2 be Linear_Combination of V;
  redefine pred L1 = L2 means
:: VECTSP_6:def 7
  for v being Element of V holds L1.v = L2.v;
end;

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

theorem :: VECTSP_6:22
  (L1+L2).v = L1.v + L2.v;

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

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

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

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

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

definition
  let GF,V,a,L;
  func a * L -> Linear_Combination of V means
:: VECTSP_6:def 9

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

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

theorem :: VECTSP_6:29
  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:30
  0.GF * L = ZeroLC(V);

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

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

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

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

theorem :: VECTSP_6:35
  1.GF * L = L;

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

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

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

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

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

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

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

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

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

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

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

theorem :: VECTSP_6:45
  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:46
  Sum(- L) = - Sum(L);

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

::
::  Auxiliary theorems.
::

theorem :: VECTSP_6:48
  (- 1.GF) * a = - a;

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