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 a = f . u;
set b = f . v;
set c = f . w;
A4: Carrier f c= {u,v,w} by RLVECT_2:def 8;

A5: now

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:28; :: thesis: verum

end;

now

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

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

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)

now

assume A9: Carrier f <> {} ; :: thesis: contradiction
consider x being Element of Carrier f;
A10: x is VECTOR of V by A9, TARSKI:def 3;
then f . x <> 0 by A9, RLVECT_2:28;
hence contradiction by A5, A6, A7, A8, A10; :: thesis: verum

end;

then f = ZeroLC V by RLVECT_2:def 7;
hence Sum f = 0. V by RLVECT_2:48
.= (f . u) * u by A6, RLVECT_1:23
.= ((f . u) * u) + (0. V) by RLVECT_1:10
.= ((f . u) * u) + ((f . v) * v) by A7, RLVECT_1:23
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:10
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A8, RLVECT_1:23 ;
:: thesis: verum

end;

suppose A11: f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A12: Carrier f = {w}

proof

thus Carrier f c= {w} :: according to XBOOLE_0:def 10 :: thesis: {w} c= Carrier f

proof

let x be set ; :: 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
A15: f . x <> 0 by A13, RLVECT_2:28;
( x <> u & x <> v & x <> w ) by A6, A7, A13, A14, RLVECT_2:28, TARSKI:def 1;
hence contradiction by A5, A13, A15; :: thesis: verum

end;

w in Carrier f by A11, RLVECT_2:28;
hence {w} c= Carrier f by ZFMISC_1:37; :: thesis: verum

end;

set F = <*w*>;
A16: rng <*w*> = {w} by FINSEQ_1:56;
A17: <*w*> is one-to-one by FINSEQ_3:102;
f (#) <*w*> = <*((f . w) * w)*> by RLVECT_2:42;
then Sum f = Sum <*((f . w) * w)*> by A12, A16, A17, RLVECT_2:def 10
.= (f . w) * w by RLVECT_1:61
.= (0. V) + ((f . w) * w) by RLVECT_1:10
.= ((0. V) + (0. V)) + ((f . w) * w) by RLVECT_1:10
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by A6, RLVECT_1:23 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A7, RLVECT_1:23; :: thesis: verum

end;

end;

end;

hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum

end;

suppose A18: f . v <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

now

per cases ( f . w = 0 or f . w <> 0 ) ;

suppose A19: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A20: Carrier f = {v}

proof

thus Carrier f c= {v} :: according to XBOOLE_0:def 10 :: thesis: {v} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume that
A21: x in Carrier f and
A22: not x in {v} ; :: thesis: contradiction
A23: f . x <> 0 by A21, RLVECT_2:28;
( x <> u & x <> v & x <> w ) by A6, A19, A21, A22, RLVECT_2:28, TARSKI:def 1;
hence contradiction by A5, A21, A23; :: thesis: verum

end;

v in Carrier f by A18, RLVECT_2:28;
hence {v} c= Carrier f by ZFMISC_1:37; :: thesis: verum

end;

set F = <*v*>;
A24: rng <*v*> = {v} by FINSEQ_1:56;
A25: <*v*> is one-to-one by FINSEQ_3:102;
f (#) <*v*> = <*((f . v) * v)*> by RLVECT_2:42;
then Sum f = Sum <*((f . v) * v)*> by A20, A24, A25, RLVECT_2:def 10
.= (f . v) * v by RLVECT_1:61
.= (0. V) + ((f . v) * v) by RLVECT_1:10
.= ((0. V) + ((f . v) * v)) + (0. V) by RLVECT_1:10
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A6, RLVECT_1:23 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A19, RLVECT_1:23; :: thesis: verum

end;

suppose A26: f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A27: Carrier f = {v,w}

proof

thus Carrier f c= {v,w} :: according to XBOOLE_0:def 10 :: thesis: {v,w} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v,w} )
assume that
A28: x in Carrier f and
A29: not x in {v,w} ; :: thesis: contradiction
A30: f . x <> 0 by A28, RLVECT_2:28;
( x <> v & x <> w & x <> u ) by A6, A28, A29, RLVECT_2:28, TARSKI:def 2;
hence contradiction by A5, A28, A30; :: thesis: verum

end;

( v in Carrier f & w in Carrier f ) by A18, A26, RLVECT_2:28;
hence {v,w} c= Carrier f by ZFMISC_1:38; :: thesis: verum

end;

set F = <*v,w*>;
A31: rng <*v,w*> = {v,w} by FINSEQ_2:147;
A32: <*v,w*> is one-to-one by A3, FINSEQ_3:103;
f (#) <*v,w*> = <*((f . v) * v),((f . w) * w)*> by RLVECT_2:43;
then Sum f = Sum <*((f . v) * v),((f . w) * w)*> by A27, A31, A32, RLVECT_2:def 10
.= ((f . v) * v) + ((f . w) * w) by RLVECT_1:62
.= ((0. V) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A6, RLVECT_1:23; :: 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 A33: f . u <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

now

per cases ( f . v = 0 or f . v <> 0 ) ;

suppose A34: f . v = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

now

per cases ( f . w = 0 or f . w <> 0 ) ;

suppose A35: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A36: Carrier f = {u}

proof

thus Carrier f c= {u} :: according to XBOOLE_0:def 10 :: thesis: {u} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u} )
assume that
A37: x in Carrier f and
A38: not x in {u} ; :: thesis: contradiction
A39: f . x <> 0 by A37, RLVECT_2:28;
( x <> u & x <> v & x <> w ) by A34, A35, A37, A38, RLVECT_2:28, TARSKI:def 1;
hence contradiction by A5, A37, A39; :: thesis: verum

end;

u in Carrier f by A33, RLVECT_2:28;
hence {u} c= Carrier f by ZFMISC_1:37; :: thesis: verum

end;

set F = <*u*>;
A40: rng <*u*> = {u} by FINSEQ_1:56;
A41: <*u*> is one-to-one by FINSEQ_3:102;
f (#) <*u*> = <*((f . u) * u)*> by RLVECT_2:42;
then Sum f = Sum <*((f . u) * u)*> by A36, A40, A41, RLVECT_2:def 10
.= (f . u) * u by RLVECT_1:61
.= ((f . u) * u) + (0. V) by RLVECT_1:10
.= (((f . u) * u) + (0. V)) + (0. V) by RLVECT_1:10
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A34, RLVECT_1:23 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A35, RLVECT_1:23; :: thesis: verum

end;

suppose A42: f . w <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A43: Carrier f = {u,w}

proof

thus Carrier f c= {u,w} :: according to XBOOLE_0:def 10 :: thesis: {u,w} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,w} )
assume that
A44: x in Carrier f and
A45: not x in {u,w} ; :: thesis: contradiction
A46: f . x <> 0 by A44, RLVECT_2:28;
( x <> v & x <> w & x <> u ) by A34, A44, A45, RLVECT_2:28, TARSKI:def 2;
hence contradiction by A5, A44, A46; :: thesis: verum

end;

( u in Carrier f & w in Carrier f ) by A33, A42, RLVECT_2:28;
hence {u,w} c= Carrier f by ZFMISC_1:38; :: thesis: verum

end;

set F = <*u,w*>;
A47: rng <*u,w*> = {u,w} by FINSEQ_2:147;
A48: <*u,w*> is one-to-one by A2, FINSEQ_3:103;
f (#) <*u,w*> = <*((f . u) * u),((f . w) * w)*> by RLVECT_2:43;
then Sum f = Sum <*((f . u) * u),((f . w) * w)*> by A43, A47, A48, RLVECT_2:def 10
.= ((f . u) * u) + ((f . w) * w) by RLVECT_1:62
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A34, RLVECT_1:23; :: thesis: verum

end;

end;

end;

hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; :: thesis: verum

end;

suppose A49: f . v <> 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

now

per cases ( f . w = 0 or f . w <> 0 ) ;

suppose A50: f . w = 0 ; :: thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)

A51: Carrier f = {u,v}

proof

thus Carrier f c= {u,v} :: according to XBOOLE_0:def 10 :: thesis: {u,v} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,v} )
assume that
A52: x in Carrier f and
A53: not x in {u,v} ; :: thesis: contradiction
A54: f . x <> 0 by A52, RLVECT_2:28;
( x <> v & x <> w & x <> u ) by A50, A52, A53, RLVECT_2:28, TARSKI:def 2;
hence contradiction by A5, A52, A54; :: thesis: verum

end;

( v in Carrier f & u in Carrier f ) by A33, A49, RLVECT_2:28;
hence {u,v} c= Carrier f by ZFMISC_1:38; :: thesis: verum

end;

set F = <*u,v*>;
A55: rng <*u,v*> = {u,v} by FINSEQ_2:147;
A56: <*u,v*> is one-to-one by A1, FINSEQ_3:103;
f (#) <*u,v*> = <*((f . u) * u),((f . v) * v)*> by RLVECT_2:43;
then Sum f = Sum <*((f . u) * u),((f . v) * v)*> by A51, A55, A56, RLVECT_2:def 10
.= ((f . u) * u) + ((f . v) * v) by RLVECT_1:62
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:10 ;
hence Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A50, RLVECT_1:23; :: thesis: verum

end;

suppose A57: 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 set ; :: 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 A33, A49, A57, RLVECT_2:28; :: thesis: verum

end;

then A58: Carrier f = {u,v,w} by A4, XBOOLE_0:def 10;
set F = <*u,v,w*>;
A59: rng <*u,v,w*> = {u,v,w} by FINSEQ_2:148;
A60: <*u,v,w*> is one-to-one by A1, A2, A3, FINSEQ_3:104;
f (#) <*u,v,w*> = <*((f . u) * u),((f . v) * v),((f . w) * w)*> by RLVECT_2:44;
then Sum f = Sum <*((f . u) * u),((f . v) * v),((f . w) * w)*> by A58, A59, A60, RLVECT_2:def 10
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:63 ;
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