let r be Real; :: thesis: for V being RealLinearSpace

for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)

let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)

let L be Linear_Combination of V; :: thesis: Sum (r (*) L) = r * (Sum L)

defpred S_{1}[ Nat] means for L being Linear_Combination of V st card (Carrier L) <= $1 holds

Sum (r (*) L) = r * (Sum L);

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A18, A1);

then S_{1}[ card (Carrier L)]
;

hence Sum (r (*) L) = r * (Sum L) ; :: thesis: verum

for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)

let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)

let L be Linear_Combination of V; :: thesis: Sum (r (*) L) = r * (Sum L)

defpred S

Sum (r (*) L) = r * (Sum L);

A1: for n being Nat st S

S

proof

A18:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= n + 1 implies Sum (r (*) L) = r * (Sum L) )

assume A3: card (Carrier L) <= n + 1 ; :: thesis: Sum (r (*) L) = r * (Sum L)

end;assume A2: S

let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= n + 1 implies Sum (r (*) L) = r * (Sum L) )

assume A3: card (Carrier L) <= n + 1 ; :: thesis: Sum (r (*) L) = r * (Sum L)

per cases
( r = 0 or r <> 0 )
;

end;

suppose
r = 0
; :: thesis: Sum (r (*) L) = r * (Sum L)

then
( r (*) L = ZeroLC V & r * (Sum L) = 0. V )
by Def2, RLVECT_1:10;

hence Sum (r (*) L) = r * (Sum L) by RLVECT_2:30; :: thesis: verum

end;hence Sum (r (*) L) = r * (Sum L) by RLVECT_2:30; :: thesis: verum

suppose A4:
r <> 0
; :: thesis: Sum (r (*) L) = r * (Sum L)

end;

per cases
( card (Carrier L) <= n or card (Carrier L) = n + 1 )
by A3, NAT_1:8;

end;

suppose A5:
card (Carrier L) = n + 1
; :: thesis: Sum (r (*) L) = r * (Sum L)

then
Carrier L <> {}
;

then consider p being object such that

A6: p in Carrier L by XBOOLE_0:def 1;

reconsider p = p as Element of V by A6;

A7: card ((Carrier L) \ {p}) = n by A5, A6, STIRL2_1:55;

consider Lp being Linear_Combination of {p} such that

A8: Lp . p = L . p by RLVECT_4:37;

set LLp = L - Lp;

(L - Lp) . p = (L . p) - (Lp . p) by RLVECT_2:54

.= 0 by A8 ;

then A9: not p in Carrier (L - Lp) by RLVECT_2:19;

A10: Carrier Lp c= {p} by RLVECT_2:def 6;

then A11: ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (Carrier L) \/ {p} ) by RLVECT_2:55, XBOOLE_1:9;

r * (Carrier Lp) c= {(r * p)}

then r (*) Lp is Linear_Combination of {(r * p)} by RLVECT_2:def 6;

then A14: Sum (r (*) Lp) = ((r (*) Lp) . (r * p)) * (r * p) by RLVECT_2:32

.= (Lp . ((r ") * (r * p))) * (r * p) by A4, Def2

.= (Lp . (((r ") * r) * p)) * (r * p) by RLVECT_1:def 7

.= (Lp . (1 * p)) * (r * p) by A4, XCMPLX_0:def 7

.= (Lp . p) * (r * p) by RLVECT_1:def 8 ;

A15: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40

.= L + (ZeroLC V) by RLVECT_2:57

.= L by RLVECT_2:41 ;

then A16: Sum L = (Sum (L - Lp)) + (Sum Lp) by RLVECT_3:1

.= (Sum (L - Lp)) + ((Lp . p) * p) by RLVECT_2:32 ;

(Carrier L) \/ {p} = Carrier L by A6, ZFMISC_1:40;

then Carrier (L - Lp) c= Carrier L by A11;

then card (Carrier (L - Lp)) <= n by A9, A7, NAT_1:43, ZFMISC_1:34;

then A17: Sum (r (*) (L - Lp)) = r * (Sum (L - Lp)) by A2;

r (*) L = (r (*) (L - Lp)) + (r (*) Lp) by A15, Th24;

hence Sum (r (*) L) = (Sum (r (*) (L - Lp))) + (Sum (r (*) Lp)) by RLVECT_3:1

.= (r * (Sum (L - Lp))) + (((Lp . p) * r) * p) by A14, A17, RLVECT_1:def 7

.= (r * (Sum (L - Lp))) + (r * ((Lp . p) * p)) by RLVECT_1:def 7

.= r * (Sum L) by A16, RLVECT_1:def 5 ;

:: thesis: verum

end;then consider p being object such that

A6: p in Carrier L by XBOOLE_0:def 1;

reconsider p = p as Element of V by A6;

A7: card ((Carrier L) \ {p}) = n by A5, A6, STIRL2_1:55;

consider Lp being Linear_Combination of {p} such that

A8: Lp . p = L . p by RLVECT_4:37;

set LLp = L - Lp;

(L - Lp) . p = (L . p) - (Lp . p) by RLVECT_2:54

.= 0 by A8 ;

then A9: not p in Carrier (L - Lp) by RLVECT_2:19;

A10: Carrier Lp c= {p} by RLVECT_2:def 6;

then A11: ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (Carrier L) \/ {p} ) by RLVECT_2:55, XBOOLE_1:9;

r * (Carrier Lp) c= {(r * p)}

proof

then
Carrier (r (*) Lp) c= {(r * p)}
by A4, Th23;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Carrier Lp) or x in {(r * p)} )

assume x in r * (Carrier Lp) ; :: thesis: x in {(r * p)}

then consider w being Element of V such that

A12: x = r * w and

A13: w in Carrier Lp ;

w = p by A10, A13, TARSKI:def 1;

hence x in {(r * p)} by A12, TARSKI:def 1; :: thesis: verum

end;assume x in r * (Carrier Lp) ; :: thesis: x in {(r * p)}

then consider w being Element of V such that

A12: x = r * w and

A13: w in Carrier Lp ;

w = p by A10, A13, TARSKI:def 1;

hence x in {(r * p)} by A12, TARSKI:def 1; :: thesis: verum

then r (*) Lp is Linear_Combination of {(r * p)} by RLVECT_2:def 6;

then A14: Sum (r (*) Lp) = ((r (*) Lp) . (r * p)) * (r * p) by RLVECT_2:32

.= (Lp . ((r ") * (r * p))) * (r * p) by A4, Def2

.= (Lp . (((r ") * r) * p)) * (r * p) by RLVECT_1:def 7

.= (Lp . (1 * p)) * (r * p) by A4, XCMPLX_0:def 7

.= (Lp . p) * (r * p) by RLVECT_1:def 8 ;

A15: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40

.= L + (ZeroLC V) by RLVECT_2:57

.= L by RLVECT_2:41 ;

then A16: Sum L = (Sum (L - Lp)) + (Sum Lp) by RLVECT_3:1

.= (Sum (L - Lp)) + ((Lp . p) * p) by RLVECT_2:32 ;

(Carrier L) \/ {p} = Carrier L by A6, ZFMISC_1:40;

then Carrier (L - Lp) c= Carrier L by A11;

then card (Carrier (L - Lp)) <= n by A9, A7, NAT_1:43, ZFMISC_1:34;

then A17: Sum (r (*) (L - Lp)) = r * (Sum (L - Lp)) by A2;

r (*) L = (r (*) (L - Lp)) + (r (*) Lp) by A15, Th24;

hence Sum (r (*) L) = (Sum (r (*) (L - Lp))) + (Sum (r (*) Lp)) by RLVECT_3:1

.= (r * (Sum (L - Lp))) + (((Lp . p) * r) * p) by A14, A17, RLVECT_1:def 7

.= (r * (Sum (L - Lp))) + (r * ((Lp . p) * p)) by RLVECT_1:def 7

.= r * (Sum L) by A16, RLVECT_1:def 5 ;

:: thesis: verum

proof

for n being Nat holds S
let L be Linear_Combination of V; :: thesis: ( card (Carrier L) <= 0 implies Sum (r (*) L) = r * (Sum L) )

assume card (Carrier L) <= 0 ; :: thesis: Sum (r (*) L) = r * (Sum L)

then Carrier L = {} ;

then A19: L = ZeroLC V by RLVECT_2:def 5;

then ( r * (0. V) = 0. V & Sum L = 0. V ) by RLVECT_2:30;

hence Sum (r (*) L) = r * (Sum L) by A19, Th26; :: thesis: verum

end;assume card (Carrier L) <= 0 ; :: thesis: Sum (r (*) L) = r * (Sum L)

then Carrier L = {} ;

then A19: L = ZeroLC V by RLVECT_2:def 5;

then ( r * (0. V) = 0. V & Sum L = 0. V ) by RLVECT_2:30;

hence Sum (r (*) L) = r * (Sum L) by A19, Th26; :: thesis: verum

then S

hence Sum (r (*) L) = r * (Sum L) ; :: thesis: verum