:: Linear Combinations in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let S be 1-sorted ;
let x be set ;
assume A1: x in S ;
func vector (S,x) ->  Element of S equals :Def1: :: RLVECT_2:def 1
x;
coherence
 x is Element of S by A1, STRUCT_0:def_5;
end;

:: deftheorem Def1 defines vector RLVECT_2:def_1_:_
 for S being 1-sorted
for x being set st x in S holds
vector (S,x) = x;

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

theorem Th2: :: RLVECT_2:2
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
proofend;

theorem :: RLVECT_2:3
for V being RealLinearSpace
for a being Real
for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proofend;

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

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

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

theorem :: RLVECT_2:7
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for 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
proofend;

definition
let V be non empty addLoopStr ;
let T be finite Subset of V;
assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ;
func Sum T ->  Element of V means :Def2: :: RLVECT_2:def 2
 ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & it = Sum F );
existence
 ex b1 being Element of V ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F )
proofend;
uniqueness
 for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b2 = Sum F ) holds
b1 = b2 by A1, RLVECT_1:42;
end;

:: deftheorem Def2 defines Sum RLVECT_2:def_2_:_
 for V being non empty addLoopStr
for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds
for b3 being Element of V holds
( b3 = Sum T iff ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b3 = Sum F ) );

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

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

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

theorem :: RLVECT_2:11
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v1, v2, v3 being Element of V st v1 <> v2 &amp; v2 <> v3 &amp; v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
proofend;

theorem Th12: :: RLVECT_2:12
for V being non empty Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V st T misses S holds
Sum (T \/ S) = (Sum T) + (Sum S)
proofend;

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

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

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

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

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

theorem :: RLVECT_2:18
for V being non empty Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82;

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

:: deftheorem Def3 defines Linear_Combination RLVECT_2:def_3_:_
 for V being non empty ZeroStr
for b2 being Element of Funcs ( the carrier of V,REAL) holds
( b2 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
b2 . v = 0 );

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

Lm1: now__::_thesis:_for_V_being_non_empty_addLoopStr_
for_L_being_Element_of_Funcs_(_the_carrier_of_V,REAL)_holds_Carrier_c=_the_carrier_of_V
let V be non empty addLoopStr ; ::_thesis: for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V
let L be Element of Funcs ( the carrier of V,REAL); ::_thesis: Carrier c= the carrier of V
A1: support L c= dom L by PRE_POLY:37;
thus  Carrier c= the carrier of V ::_thesis: verum
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Carrier or x in the carrier of V )
assume  x in support L ; ::_thesis: x in the carrier of V
then  x in dom L by A1;
hence  x in the carrier of V ; ::_thesis: verum
end;
end;

definition
let V be non empty addLoopStr ;
let L be Element of Funcs ( the carrier of V,REAL);
:: original:Carrier
redefine func Carrier L ->  Subset of V equals :: RLVECT_2:def 4
 {  v where v is Element of V : L . v <> 0  }  ;
coherence
 Carrier is Subset of V by Lm1;
compatibility
 for b1 being Subset of V holds
( b1 = Carrier iff b1 =  {  v where v is Element of V : L . v <> 0  }  )
proofend;
end;

:: deftheorem  defines Carrier RLVECT_2:def_4_:_
 for V being non empty addLoopStr
for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L =  {  v where v is Element of V : L . v <> 0  }  ;

registration
let V be non empty addLoopStr ;
let L be Linear_Combination of V;
cluster Carrier  ->  finite ;
coherence
 Carrier L is finite
proofend;
end;

theorem :: RLVECT_2:19
for V being non empty addLoopStr
for L being Linear_Combination of V
for v being Element of V holds
( L . v = 0 iff not v in Carrier L )
proofend;

definition
let V be non empty addLoopStr ;
func ZeroLC V ->  Linear_Combination of V means :Def5: :: RLVECT_2:def 5
 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 Def5 defines ZeroLC RLVECT_2:def_5_:_
 for V being non empty addLoopStr
for b2 being Linear_Combination of V holds
( b2 = ZeroLC V iff Carrier b2 = {} );

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

definition
let V be non empty addLoopStr ;
let A be Subset of V;
mode Linear_Combination of A ->  Linear_Combination of V means :Def6: :: RLVECT_2:def 6
 Carrier it c= A;
existence
 ex b1 being Linear_Combination of V st Carrier b1 c= A
proofend;
end;

:: deftheorem Def6 defines Linear_Combination RLVECT_2:def_6_:_
 for V being non empty addLoopStr
for A being Subset of V
for b3 being Linear_Combination of V holds
( b3 is Linear_Combination of A iff Carrier b3 c= A );

theorem :: RLVECT_2:21
for V being RealLinearSpace
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 Th22: :: RLVECT_2:22
for V being RealLinearSpace
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proofend;

theorem Th23: :: RLVECT_2:23
for V being RealLinearSpace
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proofend;

definition
let V be RealLinearSpace;
let F be FinSequence of V;
let f be Function of the carrier of V,REAL;
funcf (#) F ->  FinSequence of the carrier of V means :Def7: :: RLVECT_2:def 7
( len it = len F &amp; ( for i being Element of NAT st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
 ex b1 being FinSequence of the carrier of V st
( len b1 = len F &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of V st len b1 = len F &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) &amp; len b2 = len F &amp; ( for i being Element of NAT st i in dom b2 holds
b2 . i = (f . (F /. i)) * (F /. i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines (#) RLVECT_2:def_7_:_
 for V being RealLinearSpace
for F being FinSequence of V
for f being Function of the carrier of V,REAL
for b4 being FinSequence of the carrier of V holds
( b4 = f (#) F iff ( len b4 = len F &amp; ( for i being Element of NAT st i in dom b4 holds
b4 . i = (f . (F /. i)) * (F /. i) ) ) );

theorem Th24: :: RLVECT_2:24
for i being Element of NAT
for V being RealLinearSpace
for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F &amp; v = F . i holds
(f (#) F) . i = (f . v) * v
proofend;

theorem :: RLVECT_2:25
for V being RealLinearSpace
for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V
proofend;

theorem Th26: :: RLVECT_2:26
for V being RealLinearSpace
for v being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*>
proofend;

theorem Th27: :: RLVECT_2:27
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proofend;

theorem :: RLVECT_2:28
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proofend;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func Sum L ->  Element of V means :Def8: :: RLVECT_2:def 8
 ex F being FinSequence 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 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 V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) ) &amp; ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b2 = Sum (L (#) F) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines Sum RLVECT_2:def_8_:_
 for V being RealLinearSpace
for L being Linear_Combination of V
for b3 being Element of V holds
( b3 = Sum L iff ex F being FinSequence of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b3 = Sum (L (#) F) ) );

Lm2:  for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V
proofend;

theorem :: RLVECT_2:29
for V being RealLinearSpace
for A being Subset of V holds
( ( A <> {} &amp; A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proofend;

theorem :: RLVECT_2:30
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V by Lm2;

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

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

theorem Th33: :: RLVECT_2:33
for V being RealLinearSpace
for v1, v2 being VECTOR 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 :: RLVECT_2:34
for V being RealLinearSpace
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proofend;

theorem :: RLVECT_2:35
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
proofend;

theorem :: RLVECT_2:36
for V being RealLinearSpace
for v1, v2 being VECTOR 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 V be non empty addLoopStr ;
let L1, L2 be Linear_Combination of V;
:: original:=
redefine predL1 = L2 means :: RLVECT_2:def 9
 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 = RLVECT_2:def_9_:_
 for V being non empty addLoopStr
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 V be non empty addLoopStr ;
let L1, L2 be Linear_Combination of V;
:: original:+
redefine funcL1 + L2 ->  Linear_Combination of V means :Def10: :: RLVECT_2:def 10
 for v being Element of V holds it . v = (L1 . v) + (L2 . v);
coherence
 L1 + L2 is Linear_Combination of V
proofend;
compatibility
 for b1 being Linear_Combination of V holds
( b1 = L1 + L2 iff for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) )
proofend;
end;

:: deftheorem Def10 defines + RLVECT_2:def_10_:_
 for V being non empty addLoopStr
for L1, L2, b4 being Linear_Combination of V holds
( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) );

theorem Th37: :: RLVECT_2:37
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem Th38: :: RLVECT_2:38
for V being RealLinearSpace
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 :: RLVECT_2:39
for V being non empty addLoopStr
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 ;

theorem Th40: :: RLVECT_2:40
for V being RealLinearSpace
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proofend;

theorem Th41: :: RLVECT_2:41
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L &amp; (ZeroLC V) + L = L )
proofend;

definition
let V be RealLinearSpace;
let a be Real;
let L be Linear_Combination of V;
funca * L ->  Linear_Combination of V means :Def11: :: RLVECT_2:def 11
 for v being VECTOR of V holds it . v = a * (L . v);
existence
 ex b1 being Linear_Combination of V st
for v being VECTOR of V holds b1 . v = a * (L . v)
proofend;
uniqueness
 for b1, b2 being Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = a * (L . v) ) &amp; ( for v being VECTOR of V holds b2 . v = a * (L . v) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines * RLVECT_2:def_11_:_
 for V being RealLinearSpace
for a being Real
for L, b4 being Linear_Combination of V holds
( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) );

theorem Th42: :: RLVECT_2:42
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V st a <> 0 holds
Carrier (a * L) = Carrier L
proofend;

theorem Th43: :: RLVECT_2:43
for V being RealLinearSpace
for L being Linear_Combination of V holds 0 * L = ZeroLC V
proofend;

theorem Th44: :: RLVECT_2:44
for V being RealLinearSpace
for a being Real
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 Th45: :: RLVECT_2:45
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proofend;

theorem Th46: :: RLVECT_2:46
for V being RealLinearSpace
for a being Real
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proofend;

theorem Th47: :: RLVECT_2:47
for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
proofend;

theorem Th48: :: RLVECT_2:48
for V being RealLinearSpace
for L being Linear_Combination of V holds 1 * L = L
proofend;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func - L ->  Linear_Combination of V equals :: RLVECT_2:def 12
(- 1) * L;
correctness
coherence
(- 1) * L is Linear_Combination of V;
;
end;

:: deftheorem  defines - RLVECT_2:def_12_:_
 for V being RealLinearSpace
for L being Linear_Combination of V holds - L = (- 1) * L;

theorem Th49: :: RLVECT_2:49
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proofend;

theorem :: RLVECT_2:50
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proofend;

theorem :: RLVECT_2:51
for V being RealLinearSpace
for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th42;

theorem :: RLVECT_2:52
for V being RealLinearSpace
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 Th44;

theorem :: RLVECT_2:53
for V being RealLinearSpace
for L being Linear_Combination of V holds - (- L) = L
proofend;

definition
let V be RealLinearSpace;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 ->  Linear_Combination of V equals :: RLVECT_2:def 13
L1 + (- L2);
correctness
coherence
L1 + (- L2) is Linear_Combination of V;
;
end;

:: deftheorem  defines - RLVECT_2:def_13_:_
 for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th54: :: RLVECT_2:54
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proofend;

theorem :: RLVECT_2:55
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem :: RLVECT_2:56
for V being RealLinearSpace
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 Th57: :: RLVECT_2:57
for V being RealLinearSpace
for L being Linear_Combination of V holds L - L = ZeroLC V
proofend;

definition
let V be RealLinearSpace;
func LinComb V ->  set  means :Def14: :: RLVECT_2:def 14
 for x being set holds
( x in it iff x is Linear_Combination of V );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Linear_Combination of V )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Linear_Combination of V ) ) &amp; ( for x being set holds
( x in b2 iff x is Linear_Combination of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines LinComb RLVECT_2:def_14_:_
 for V being RealLinearSpace
for b2 being set holds
( b2 = LinComb V iff for x being set holds
( x in b2 iff x is Linear_Combination of V ) );

registration
let V be RealLinearSpace;
cluster LinComb V ->  non empty ;
coherence
 not LinComb V is empty
proofend;
end;

definition
let V be RealLinearSpace;
let e be Element of LinComb V;
func @ e ->  Linear_Combination of V equals :: RLVECT_2:def 15
e;
coherence
 e is Linear_Combination of V by Def14;
end;

:: deftheorem  defines @ RLVECT_2:def_15_:_
 for V being RealLinearSpace
for e being Element of LinComb V holds @ e = e;

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
func @ L ->  Element of LinComb V equals :: RLVECT_2:def 16
L;
coherence
 L is Element of LinComb V by Def14;
end;

:: deftheorem  defines @ RLVECT_2:def_16_:_
 for V being RealLinearSpace
for L being Linear_Combination of V holds @ L = L;

definition
let V be RealLinearSpace;
func LCAdd V ->  BinOp of (LinComb V) means :Def17: :: RLVECT_2:def 17
 for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);
existence
 ex b1 being BinOp of (LinComb V) st
for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2)
proofend;
uniqueness
 for b1, b2 being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) &amp; ( for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines LCAdd RLVECT_2:def_17_:_
 for V being RealLinearSpace
for b2 being BinOp of (LinComb V) holds
( b2 = LCAdd V iff for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) );

definition
let V be RealLinearSpace;
func LCMult V ->  Function of [:REAL,(LinComb V):],(LinComb V) means :Def18: :: RLVECT_2:def 18
 for a being Real
for e being Element of LinComb V holds it . [a,e] = a * (@ e);
existence
 ex b1 being Function of [:REAL,(LinComb V):],(LinComb V) st
for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
proofend;
uniqueness
 for b1, b2 being Function of [:REAL,(LinComb V):],(LinComb V) st ( for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) &amp; ( for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines LCMult RLVECT_2:def_18_:_
 for V being RealLinearSpace
for b2 being Function of [:REAL,(LinComb V):],(LinComb V) holds
( b2 = LCMult V iff for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) );

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

:: deftheorem  defines LC_RLSpace RLVECT_2:def_19_:_
 for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);

registration
let V be RealLinearSpace;
cluster LC_RLSpace V ->  non empty strict ;
coherence
 ( LC_RLSpace V is strict &amp; not LC_RLSpace V is empty ) ;
end;

registration
let V be RealLinearSpace;
cluster LC_RLSpace V ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( LC_RLSpace V is Abelian &amp; LC_RLSpace V is add-associative &amp; LC_RLSpace V is right_zeroed &amp; LC_RLSpace V is right_complementable &amp; LC_RLSpace V is vector-distributive &amp; LC_RLSpace V is scalar-distributive &amp; LC_RLSpace V is scalar-associative &amp; LC_RLSpace V is scalar-unital )
proofend;
end;

theorem :: RLVECT_2:58
for V being RealLinearSpace holds the carrier of (LC_RLSpace V) = LinComb V ;

theorem :: RLVECT_2:59
for V being RealLinearSpace holds 0. (LC_RLSpace V) = ZeroLC V ;

theorem :: RLVECT_2:60
for V being RealLinearSpace holds the addF of (LC_RLSpace V) = LCAdd V ;

theorem :: RLVECT_2:61
for V being RealLinearSpace holds the Mult of (LC_RLSpace V) = LCMult V ;

theorem Th62: :: RLVECT_2:62
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2
proofend;

theorem Th63: :: RLVECT_2:63
for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L
proofend;

theorem Th64: :: RLVECT_2:64
for V being RealLinearSpace
for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L
proofend;

theorem :: RLVECT_2:65
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2
proofend;

definition
let V be RealLinearSpace;
let A be Subset of V;
func LC_RLSpace A ->  strict Subspace of LC_RLSpace V means :: RLVECT_2:def 20
 the carrier of it =  {  l where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 =  {  l where l is Linear_Combination of A : verum  }
proofend;
uniqueness
 for b1, b2 being strict Subspace of LC_RLSpace V st the carrier of b1 =  {  l where l is Linear_Combination of A : verum  }  &amp; the carrier of b2 =  {  l where l is Linear_Combination of A : verum  }  holds
b1 = b2 by RLSUB_1:30;
end;

:: deftheorem  defines LC_RLSpace RLVECT_2:def_20_:_
 for V being RealLinearSpace
for A being Subset of V
for b3 being strict Subspace of LC_RLSpace V holds
( b3 = LC_RLSpace A iff the carrier of b3 =  {  l where l is Linear_Combination of A : verum  }  );

theorem Th66: :: RLVECT_2:66
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G &amp; ( for k being Element of NAT
for v being Element of V st k in dom F &amp; v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)
proofend;

theorem :: RLVECT_2:67
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
for F, G being FinSequence of V st len F = len G &amp; ( for k being Element of NAT st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)
proofend;

theorem :: RLVECT_2:68
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R
for F, G, H being FinSequence of V st len F = len G &amp; len F = len H &amp; ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) holds
Sum H = (Sum F) - (Sum G)
proofend;

theorem :: RLVECT_2:69
for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V
proofend;

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

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