let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V
for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)
let u, v, w be VECTOR of V; :: thesis: for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)
let f be Linear_Combination of {u,v,w}; :: thesis: ( u <> v & u <> w & v <> w implies Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) )
assume that
A1: u <> v and
A2: u <> w and
A3: v <> w ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
set c = f . w;
set b = f . v;
set a = f . u;
A4: Carrier f c= {u,v,w} by RLVECT_2:def 6;
A5: now :: thesis: for x being VECTOR of V st x <> v & x <> u & x <> w holds
f . x = 0
let x be VECTOR of V; :: thesis: ( x <> v & x <> u & x <> w implies f . x = 0 )
assume ( x <> v & x <> u & x <> w ) ; :: thesis: f . x = 0
then not x in Carrier f by A4, ENUMSET1:def 1;
hence f . x = 0 by RLVECT_2:19; :: thesis: verum
end;
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . u = 0 or f . u <> 0 ) ;
suppose A6: f . u = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . v = 0 or f . v <> 0 ) ;
suppose A7: f . v = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . w = 0 or f . w <> 0 ) ;
suppose A8: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
then f = ZeroLC V by RLVECT_2:def 5;
hence Sum f = 0. V by RLVECT_2:30
.= (f . u) * u by A6, RLVECT_1:10
.= ((f . u) * u) + (0. V) by RLVECT_1:4
.= ((f . u) * u) + ((f . v) * v) by A7, RLVECT_1:10
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A8, RLVECT_1:10 ;
:: thesis: verum
end;
suppose A11: f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A12: Carrier f c= {w}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {w} )
assume that
A13: x in Carrier f and
A14: not x in {w} ; :: thesis: contradiction
( f . x <> 0 & x <> w ) by A13, A14, RLVECT_2:19, TARSKI:def 1;
hence contradiction by A5, A6, A7, A13; :: thesis: verum
end;
w in Carrier f by A11, RLVECT_2:19;
then A15: Carrier f = {w} by A12, ZFMISC_1:33;
set F = <*w*>;
A16: f (#) <*w*> = <*((f . w) * w)*> by RLVECT_2:26;
( rng <*w*> = {w} & <*w*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then Sum f = Sum <*((f . w) * w)*> by A15, A16, RLVECT_2:def 8
.= (f . w) * w by RLVECT_1:44
.= (0. V) + ((f . w) * w) by RLVECT_1:4
.= ((0. V) + (0. V)) + ((f . w) * w) by RLVECT_1:4
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by A6, RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A7, RLVECT_1:10; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
suppose A17: f . v <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . w = 0 or f . w <> 0 ) ;
suppose A18: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A19: Carrier f c= {v}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume that
A20: x in Carrier f and
A21: not x in {v} ; :: thesis: contradiction
( f . x <> 0 & x <> v ) by A20, A21, RLVECT_2:19, TARSKI:def 1;
hence contradiction by A5, A6, A18, A20; :: thesis: verum
end;
v in Carrier f by A17, RLVECT_2:19;
then A22: Carrier f = {v} by A19, ZFMISC_1:33;
set F = <*v*>;
A23: f (#) <*v*> = <*((f . v) * v)*> by RLVECT_2:26;
( rng <*v*> = {v} & <*v*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then Sum f = Sum <*((f . v) * v)*> by A22, A23, RLVECT_2:def 8
.= (f . v) * v by RLVECT_1:44
.= (0. V) + ((f . v) * v) by RLVECT_1:4
.= ((0. V) + ((f . v) * v)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A6, RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A18, RLVECT_1:10; :: thesis: verum
end;
suppose f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
then A24: w in Carrier f by RLVECT_2:19;
A25: Carrier f c= {v,w}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v,w} )
assume that
A26: x in Carrier f and
A27: not x in {v,w} ; :: thesis: contradiction
A28: x <> w by A27, TARSKI:def 2;
( f . x <> 0 & x <> v ) by A26, A27, RLVECT_2:19, TARSKI:def 2;
hence contradiction by A5, A6, A26, A28; :: thesis: verum
end;
v in Carrier f by A17, RLVECT_2:19;
then {v,w} c= Carrier f by A24, ZFMISC_1:32;
then A29: Carrier f = {v,w} by A25;
set F = <*v,w*>;
A30: f (#) <*v,w*> = <*((f . v) * v),((f . w) * w)*> by RLVECT_2:27;
( rng <*v,w*> = {v,w} & <*v,w*> is one-to-one ) by A3, FINSEQ_2:127, FINSEQ_3:94;
then Sum f = Sum <*((f . v) * v),((f . w) * w)*> by A29, A30, RLVECT_2:def 8
.= ((f . v) * v) + ((f . w) * w) by RLVECT_1:45
.= ((0. V) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:4 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A6, RLVECT_1:10; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
suppose A31: f . u <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . v = 0 or f . v <> 0 ) ;
suppose A32: f . v = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . w = 0 or f . w <> 0 ) ;
suppose A33: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A34: Carrier f c= {u}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u} )
assume that
A35: x in Carrier f and
A36: not x in {u} ; :: thesis: contradiction
( f . x <> 0 & x <> u ) by A35, A36, RLVECT_2:19, TARSKI:def 1;
hence contradiction by A5, A32, A33, A35; :: thesis: verum
end;
u in Carrier f by A31, RLVECT_2:19;
then A37: Carrier f = {u} by A34, ZFMISC_1:33;
set F = <*u*>;
A38: f (#) <*u*> = <*((f . u) * u)*> by RLVECT_2:26;
( rng <*u*> = {u} & <*u*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then Sum f = Sum <*((f . u) * u)*> by A37, A38, RLVECT_2:def 8
.= (f . u) * u by RLVECT_1:44
.= ((f . u) * u) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + (0. V)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A32, RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A33, RLVECT_1:10; :: thesis: verum
end;
suppose f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
then A39: w in Carrier f by RLVECT_2:19;
A40: Carrier f c= {u,w}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,w} )
assume that
A41: x in Carrier f and
A42: not x in {u,w} ; :: thesis: contradiction
A43: x <> u by A42, TARSKI:def 2;
( f . x <> 0 & x <> w ) by A41, A42, RLVECT_2:19, TARSKI:def 2;
hence contradiction by A5, A32, A41, A43; :: thesis: verum
end;
u in Carrier f by A31, RLVECT_2:19;
then {u,w} c= Carrier f by A39, ZFMISC_1:32;
then A44: Carrier f = {u,w} by A40;
set F = <*u,w*>;
A45: f (#) <*u,w*> = <*((f . u) * u),((f . w) * w)*> by RLVECT_2:27;
( rng <*u,w*> = {u,w} & <*u,w*> is one-to-one ) by A2, FINSEQ_2:127, FINSEQ_3:94;
then Sum f = Sum <*((f . u) * u),((f . w) * w)*> by A44, A45, RLVECT_2:def 8
.= ((f . u) * u) + ((f . w) * w) by RLVECT_1:45
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by RLVECT_1:4 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A32, RLVECT_1:10; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
suppose A46: f . v <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
per cases ( f . w = 0 or f . w <> 0 ) ;
suppose A47: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A48: Carrier f c= {u,v}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,v} )
assume that
A49: x in Carrier f and
A50: not x in {u,v} ; :: thesis: contradiction
A51: x <> u by A50, TARSKI:def 2;
( f . x <> 0 & x <> v ) by A49, A50, RLVECT_2:19, TARSKI:def 2;
hence contradiction by A5, A47, A49, A51; :: thesis: verum
end;
( v in Carrier f & u in Carrier f ) by A31, A46, RLVECT_2:19;
then {u,v} c= Carrier f by ZFMISC_1:32;
then A52: Carrier f = {u,v} by A48;
set F = <*u,v*>;
A53: f (#) <*u,v*> = <*((f . u) * u),((f . v) * v)*> by RLVECT_2:27;
( rng <*u,v*> = {u,v} & <*u,v*> is one-to-one ) by A1, FINSEQ_2:127, FINSEQ_3:94;
then Sum f = Sum <*((f . u) * u),((f . v) * v)*> by A52, A53, RLVECT_2:def 8
.= ((f . u) * u) + ((f . v) * v) by RLVECT_1:45
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:4 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A47, RLVECT_1:10; :: thesis: verum
end;
suppose A54: f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
{u,v,w} c= Carrier f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {u,v,w} or x in Carrier f )
assume x in {u,v,w} ; :: thesis: x in Carrier f
then ( x = u or x = v or x = w ) by ENUMSET1:def 1;
hence x in Carrier f by A31, A46, A54, RLVECT_2:19; :: thesis: verum
end;
then A55: Carrier f = {u,v,w} by A4;
set F = <*u,v,w*>;
A56: f (#) <*u,v,w*> = <*((f . u) * u),((f . v) * v),((f . w) * w)*> by RLVECT_2:28;
( rng <*u,v,w*> = {u,v,w} & <*u,v,w*> is one-to-one ) by A1, A2, A3, FINSEQ_2:128, FINSEQ_3:95;
then Sum f = Sum <*((f . u) * u),((f . v) * v),((f . w) * w)*> by A55, A56, RLVECT_2:def 8
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:46 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum
end;
end;
end;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum