:: Linear Combinations in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
mode Linear_Combination of V ->  Element of Funcs ( the carrier of V, the carrier of GF) means :Def1: :: 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;
existence
 ex b1 being Element of Funcs ( the carrier of V, the carrier of GF) ex T being finite Subset of V st
for v being Element of V st not v in T holds
b1 . v = 0. GF
proofend;
end;

:: deftheorem Def1 defines Linear_Combination VECTSP_6:def_1_:_
 for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for b3 being Element of Funcs ( the carrier of V, the carrier of GF) holds
( b3 is Linear_Combination of V iff ex T being finite Subset of V st
for v being Element of V st not v in T holds
b3 . v = 0. GF );

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 2
 {  v where v is Element of V : L . v <> 0. GF  }  ;
coherence
  {  v where v is Element of V : L . v <> 0. GF  }  is finite Subset of V
proofend;
end;

:: deftheorem  defines Carrier VECTSP_6:def_2_:_
 for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for L being Linear_Combination of V holds Carrier L =  {  v where v is Element of V : L . v <> 0. GF  }  ;

theorem :: VECTSP_6:1
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Element of V st
( x = v &amp; L . v <> 0. GF ) ) ;

theorem :: VECTSP_6:2
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds
( L . v = 0. GF iff not v in Carrier L )
proofend;

definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
func ZeroLC V ->  Linear_Combination of V means :Def3: :: VECTSP_6:def 3
 Carrier it = {} ;
existence
 ex b1 being Linear_Combination of V st Carrier b1 = {}
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st Carrier b1 = {} &amp; Carrier b2 = {} holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ZeroLC VECTSP_6:def_3_:_
 for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for b3 being Linear_Combination of V holds
( b3 = ZeroLC V iff Carrier b3 = {} );

theorem Th3: :: VECTSP_6:3
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds (ZeroLC V) . v = 0. GF
proofend;

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 :Def4: :: VECTSP_6:def 4
 Carrier it c= A;
existence
 ex b1 being Linear_Combination of V st Carrier b1 c= A
proofend;
end;

:: deftheorem Def4 defines Linear_Combination VECTSP_6:def_4_:_
 for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for A being Subset of V
for b4 being Linear_Combination of V holds
( b4 is Linear_Combination of A iff Carrier b4 c= A );

theorem :: VECTSP_6:4
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
proofend;

theorem Th5: :: VECTSP_6:5
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proofend;

theorem Th6: :: VECTSP_6:6
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proofend;

theorem :: VECTSP_6:7
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def4;

definition
let GF be non empty addLoopStr ;
let V be non empty VectSpStr over GF;
let F be FinSequence of the carrier of V;
let f be Function of V,GF;
funcf (#) F ->  FinSequence of V means :Def5: :: VECTSP_6:def 5
( len it = len F &amp; ( for i being Nat st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
 ex b1 being FinSequence of V st
( len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of V st len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) &amp; len b2 = len F &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (f . (F /. i)) * (F /. i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines (#) VECTSP_6:def_5_:_
 for GF being non empty addLoopStr
for V being non empty VectSpStr over GF
for F being FinSequence of the carrier of V
for f being Function of V,GF
for b5 being FinSequence of V holds
( b5 = f (#) F iff ( len b5 = len F &amp; ( for i being Nat st i in dom b5 holds
b5 . i = (f . (F /. i)) * (F /. i) ) ) );

theorem Th8: :: VECTSP_6:8
for i being Element of NAT
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for F being FinSequence of V
for f being Function of V,GF st i in dom F &amp; v = F . i holds
(f (#) F) . i = (f . v) * v
proofend;

theorem :: VECTSP_6:9
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V
proofend;

theorem Th10: :: VECTSP_6:10
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>
proofend;

theorem Th11: :: VECTSP_6:11
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proofend;

theorem :: VECTSP_6:12
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2, v3 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proofend;

theorem Th13: :: VECTSP_6:13
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proofend;

definition
let GF be non empty addLoopStr ;
let V be non empty VectSpStr over GF;
let L be Linear_Combination of V;
assume A1: ( V is Abelian &amp; V is add-associative &amp; V is right_zeroed &amp; V is right_complementable ) ;
func Sum L ->  Element of V means :Def6: :: VECTSP_6:def 6
 ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; it = Sum (L (#) F) );
existence
 ex b1 being Element of V ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) )
proofend;
uniqueness
 for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) ) &amp; ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b2 = Sum (L (#) F) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Sum VECTSP_6:def_6_:_
 for GF being non empty addLoopStr
for V being non empty VectSpStr over GF
for L being Linear_Combination of V st V is Abelian &amp; V is add-associative &amp; V is right_zeroed &amp; V is right_complementable holds
for b4 being Element of V holds
( b4 = Sum L iff ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b4 = Sum (L (#) F) ) );

Lm1:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V
proofend;

theorem :: VECTSP_6:14
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} &amp; A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proofend;

theorem :: VECTSP_6:15
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V by Lm1;

theorem :: VECTSP_6:16
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proofend;

theorem Th17: :: VECTSP_6:17
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
proofend;

theorem Th18: :: VECTSP_6:18
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
proofend;

theorem :: VECTSP_6:19
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proofend;

theorem :: VECTSP_6:20
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
proofend;

theorem :: VECTSP_6:21
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for L being Linear_Combination of V st Carrier L = {v1,v2} &amp; v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
proofend;

definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
:: original:=
redefine predL1 = L2 means :: VECTSP_6:def 7
 for v being Element of V holds L1 . v = L2 . v;
compatibility
 ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;

:: deftheorem  defines = VECTSP_6:def_7_:_
 for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
funcL1 + L2 ->  Linear_Combination of V equals :: VECTSP_6:def 8
L1 + L2;
coherence
 L1 + L2 is Linear_Combination of V
proofend;
end;

:: deftheorem  defines + VECTSP_6:def_8_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2;

theorem Th22: :: VECTSP_6:22
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)
proofend;

theorem Th23: :: VECTSP_6:23
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem Th24: :: VECTSP_6:24
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A &amp; L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
proofend;

theorem Th25: :: VECTSP_6:25
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
proofend;

theorem :: VECTSP_6:26
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proofend;

theorem :: VECTSP_6:27
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L &amp; (ZeroLC V) + L = L )
proofend;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let a be Element of GF;
let L be Linear_Combination of V;
funca * L ->  Linear_Combination of V means :Def9: :: VECTSP_6:def 9
 for v being Element of V holds it . v = a * (L . v);
existence
 ex b1 being Linear_Combination of V st
for v being Element of V holds b1 . v = a * (L . v)
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being Element of V holds b1 . v = a * (L . v) ) &amp; ( for v being Element of V holds b2 . v = a * (L . v) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines * VECTSP_6:def_9_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L, b5 being Linear_Combination of V holds
( b5 = a * L iff for v being Element of V holds b5 . v = a * (L . v) );

theorem Th28: :: VECTSP_6:28
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L
proofend;

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

theorem Th30: :: VECTSP_6:30
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V
proofend;

theorem Th31: :: VECTSP_6:31
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
proofend;

theorem :: VECTSP_6:32
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proofend;

theorem :: VECTSP_6:33
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proofend;

theorem Th34: :: VECTSP_6:34
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
proofend;

theorem :: VECTSP_6:35
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (1. GF) * L = L
proofend;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L be Linear_Combination of V;
func - L ->  Linear_Combination of V equals :: VECTSP_6:def 10
(- (1. GF)) * L;
correctness
coherence
(- (1. GF)) * L is Linear_Combination of V;
;
involutiveness
 for b1, b2 being Linear_Combination of V st b1 = (- (1. GF)) * b2 holds
b2 = (- (1. GF)) * b1
proofend;
end;

:: deftheorem  defines - VECTSP_6:def_10_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds - L = (- (1. GF)) * L;

Lm2:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a
proofend;

theorem Th36: :: VECTSP_6:36
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proofend;

theorem :: VECTSP_6:37
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proofend;

Lm3:  for GF being Field holds - (1. GF) <> 0. GF
proofend;

theorem Th38: :: VECTSP_6:38
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
proofend;

theorem :: VECTSP_6:39
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by Th31;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 ->  Linear_Combination of V equals :: VECTSP_6:def 11
L1 + (- L2);
coherence
 L1 + (- L2) is Linear_Combination of V ;
end;

:: deftheorem  defines - VECTSP_6:def_11_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th40: :: VECTSP_6:40
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proofend;

theorem :: VECTSP_6:41
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem :: VECTSP_6:42
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A &amp; L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
proofend;

theorem Th43: :: VECTSP_6:43
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds L - L = ZeroLC V
proofend;

theorem Th44: :: VECTSP_6:44
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proofend;

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

theorem Th46: :: VECTSP_6:46
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proofend;

theorem :: VECTSP_6:47
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proofend;

::
:: Auxiliary theorems.
::
theorem :: VECTSP_6:48
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;

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