let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)

let v be VECTOR of V; :: thesis: for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)

let L be Linear_Combination of V; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

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

Sum (v + L) = ((sum L) * v) + (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(A16, A1);

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

hence Sum (v + L) = ((sum L) * v) + (Sum L) ; :: thesis: verum

for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)

let v be VECTOR of V; :: thesis: for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)

let L be Linear_Combination of V; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

defpred S

Sum (v + L) = ((sum L) * v) + (Sum L);

A1: for n being Nat st S

S

proof

A16:
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 (v + L) = ((sum L) * v) + (Sum L) )

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

end;assume A2: S

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

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

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

end;

suppose A4:
card (Carrier L) = n + 1
; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

then
not Carrier L is empty
;

then consider w being object such that

A5: w in Carrier L ;

reconsider w = w as Element of V by A5;

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

consider Lw being Linear_Combination of {w} such that

A7: Lw . w = L . w by RLVECT_4:37;

set LLw = L - Lw;

(L - Lw) . w = (L . w) - (Lw . w) by RLVECT_2:54

.= 0 by A7 ;

then A8: not w in Carrier (L - Lw) by RLVECT_2:19;

A9: Carrier Lw c= {w} by RLVECT_2:def 6;

then A10: ( Carrier (L - Lw) c= (Carrier L) \/ (Carrier Lw) & (Carrier L) \/ (Carrier Lw) c= (Carrier L) \/ {w} ) by RLVECT_2:55, XBOOLE_1:9;

(Carrier L) \/ {w} = Carrier L by A5, ZFMISC_1:40;

then Carrier (L - Lw) c= Carrier L by A10;

then card (Carrier (L - Lw)) <= n by A8, A6, NAT_1:43, ZFMISC_1:34;

then A11: Sum (v + (L - Lw)) = ((sum (L - Lw)) * v) + (Sum (L - Lw)) by A2;

A12: (L - Lw) + Lw = L + (Lw - Lw) by RLVECT_2:40

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

.= L by RLVECT_2:41 ;

then A13: Sum L = (Sum (L - Lw)) + (Sum Lw) by RLVECT_3:1

.= (Sum (L - Lw)) + ((Lw . w) * w) by RLVECT_2:32 ;

v + (Carrier Lw) c= v + {w} by A9, RLTOPSP1:8;

then v + (Carrier Lw) c= {(v + w)} by Lm3;

then Carrier (v + Lw) c= {(v + w)} by Th16;

then v + Lw is Linear_Combination of {(v + w)} by RLVECT_2:def 6;

then A14: Sum (v + Lw) = ((v + Lw) . (v + w)) * (v + w) by RLVECT_2:32

.= (Lw . ((v + w) - v)) * (v + w) by Def1

.= (Lw . w) * (v + w) by RLVECT_4:1 ;

A15: sum L = (sum (L - Lw)) + (sum Lw) by A12, Th34

.= (sum (L - Lw)) + (Lw . w) by A9, Th32 ;

v + L = (v + (L - Lw)) + (v + Lw) by A12, Th17;

hence Sum (v + L) = (Sum (v + (L - Lw))) + (Sum (v + Lw)) by RLVECT_3:1

.= (((sum (L - Lw)) * v) + (Sum (L - Lw))) + (((Lw . w) * v) + ((Lw . w) * w)) by A11, A14, RLVECT_1:def 5

.= ((((sum (L - Lw)) * v) + (Sum (L - Lw))) + ((Lw . w) * v)) + ((Lw . w) * w) by RLVECT_1:def 3

.= ((((sum (L - Lw)) * v) + ((Lw . w) * v)) + (Sum (L - Lw))) + ((Lw . w) * w) by RLVECT_1:def 3

.= (((sum L) * v) + (Sum (L - Lw))) + ((Lw . w) * w) by A15, RLVECT_1:def 6

.= ((sum L) * v) + (Sum L) by A13, RLVECT_1:def 3 ;

:: thesis: verum

end;then consider w being object such that

A5: w in Carrier L ;

reconsider w = w as Element of V by A5;

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

consider Lw being Linear_Combination of {w} such that

A7: Lw . w = L . w by RLVECT_4:37;

set LLw = L - Lw;

(L - Lw) . w = (L . w) - (Lw . w) by RLVECT_2:54

.= 0 by A7 ;

then A8: not w in Carrier (L - Lw) by RLVECT_2:19;

A9: Carrier Lw c= {w} by RLVECT_2:def 6;

then A10: ( Carrier (L - Lw) c= (Carrier L) \/ (Carrier Lw) & (Carrier L) \/ (Carrier Lw) c= (Carrier L) \/ {w} ) by RLVECT_2:55, XBOOLE_1:9;

(Carrier L) \/ {w} = Carrier L by A5, ZFMISC_1:40;

then Carrier (L - Lw) c= Carrier L by A10;

then card (Carrier (L - Lw)) <= n by A8, A6, NAT_1:43, ZFMISC_1:34;

then A11: Sum (v + (L - Lw)) = ((sum (L - Lw)) * v) + (Sum (L - Lw)) by A2;

A12: (L - Lw) + Lw = L + (Lw - Lw) by RLVECT_2:40

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

.= L by RLVECT_2:41 ;

then A13: Sum L = (Sum (L - Lw)) + (Sum Lw) by RLVECT_3:1

.= (Sum (L - Lw)) + ((Lw . w) * w) by RLVECT_2:32 ;

v + (Carrier Lw) c= v + {w} by A9, RLTOPSP1:8;

then v + (Carrier Lw) c= {(v + w)} by Lm3;

then Carrier (v + Lw) c= {(v + w)} by Th16;

then v + Lw is Linear_Combination of {(v + w)} by RLVECT_2:def 6;

then A14: Sum (v + Lw) = ((v + Lw) . (v + w)) * (v + w) by RLVECT_2:32

.= (Lw . ((v + w) - v)) * (v + w) by Def1

.= (Lw . w) * (v + w) by RLVECT_4:1 ;

A15: sum L = (sum (L - Lw)) + (sum Lw) by A12, Th34

.= (sum (L - Lw)) + (Lw . w) by A9, Th32 ;

v + L = (v + (L - Lw)) + (v + Lw) by A12, Th17;

hence Sum (v + L) = (Sum (v + (L - Lw))) + (Sum (v + Lw)) by RLVECT_3:1

.= (((sum (L - Lw)) * v) + (Sum (L - Lw))) + (((Lw . w) * v) + ((Lw . w) * w)) by A11, A14, RLVECT_1:def 5

.= ((((sum (L - Lw)) * v) + (Sum (L - Lw))) + ((Lw . w) * v)) + ((Lw . w) * w) by RLVECT_1:def 3

.= ((((sum (L - Lw)) * v) + ((Lw . w) * v)) + (Sum (L - Lw))) + ((Lw . w) * w) by RLVECT_1:def 3

.= (((sum L) * v) + (Sum (L - Lw))) + ((Lw . w) * w) by A15, RLVECT_1:def 6

.= ((sum L) * v) + (Sum L) by A13, RLVECT_1:def 3 ;

:: thesis: verum

proof

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

assume card (Carrier L) <= 0 ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

then A17: Carrier L = {} V ;

then A18: ( L = ZeroLC V & Sum L = 0. V ) by RLVECT_2:34, RLVECT_2:def 5;

v + (Carrier L) = {} by A17, Th8;

then Carrier (v + L) = {} by Th16;

hence Sum (v + L) = 0. V by RLVECT_2:34

.= (0. V) + (0. V)

.= ((sum L) * v) + (Sum L) by A18, Th31, RLVECT_1:10 ;

:: thesis: verum

end;assume card (Carrier L) <= 0 ; :: thesis: Sum (v + L) = ((sum L) * v) + (Sum L)

then A17: Carrier L = {} V ;

then A18: ( L = ZeroLC V & Sum L = 0. V ) by RLVECT_2:34, RLVECT_2:def 5;

v + (Carrier L) = {} by A17, Th8;

then Carrier (v + L) = {} by Th16;

hence Sum (v + L) = 0. V by RLVECT_2:34

.= (0. V) + (0. V)

.= ((sum L) * v) + (Sum L) by A18, Th31, RLVECT_1:10 ;

:: thesis: verum

then S

hence Sum (v + L) = ((sum L) * v) + (Sum L) ; :: thesis: verum