let x be set ; :: thesis: for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let V be RealLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let v1, v2, v3 be VECTOR of V; :: thesis: ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
thus ( x in Lin {v1,v2,v3} implies ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) :: thesis: ( ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Lin {v1,v2,v3} )

proof

assume A1: x in Lin {v1,v2,v3} ; :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

now

per cases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ;

suppose A2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

consider l being Linear_Combination of {v1,v2,v3} such that
A3: x = Sum l by A1, RLVECT_3:17;
x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, Th9;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: verum

end;

suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

then A4: ( {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {v3,v3,v1} ) by ENUMSET1:70, ENUMSET1:100;

now

per cases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A4, ENUMSET1:70;

suppose {v1,v2,v3} = {v1,v2} ; :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

then consider a, b being Real such that
A5: x = (a * v1) + (b * v2) by A1, Th14;
x = ((a * v1) + (b * v2)) + (0. V) by A5, RLVECT_1:10
.= ((a * v1) + (b * v2)) + (0 * v3) by RLVECT_1:23 ;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: verum

end;

suppose {v1,v2,v3} = {v1,v3} ; :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

then consider a, b being Real such that
A6: x = (a * v1) + (b * v3) by A1, Th14;
x = ((a * v1) + (0. V)) + (b * v3) by A6, RLVECT_1:10
.= ((a * v1) + (0 * v2)) + (b * v3) by RLVECT_1:23 ;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: verum

end;

end;

end;

hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: verum

end;

end;

end;

hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: verum

end;

given a, b, c being Real such that A7: x = ((a * v1) + (b * v2)) + (c * v3) ; :: thesis: x in Lin {v1,v2,v3}

now

per cases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ;

suppose A8: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; :: thesis: x in Lin {v1,v2,v3}

now

per cases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A8;

suppose v1 = v2 ; :: thesis: x in Lin {v1,v2,v3}

then ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A7, ENUMSET1:70, RLVECT_1:def 9;
hence x in Lin {v1,v2,v3} by Th14; :: thesis: verum

end;

suppose A9: v1 = v3 ; :: thesis: x in Lin {v1,v2,v3}

then A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:98
.= {v2,v1} by ENUMSET1:70 ;
x = (b * v2) + ((a * v1) + (c * v1)) by A7, A9, RLVECT_1:def 6
.= (b * v2) + ((a + c) * v1) by RLVECT_1:def 9 ;
hence x in Lin {v1,v2,v3} by A10, Th14; :: thesis: verum

end;

suppose A11: v2 = v3 ; :: thesis: x in Lin {v1,v2,v3}

then A12: x = (a * v1) + ((b * v2) + (c * v2)) by A7, RLVECT_1:def 6
.= (a * v1) + ((b + c) * v2) by RLVECT_1:def 9 ;
{v1,v2,v3} = {v2,v2,v1} by A11, ENUMSET1:100
.= {v1,v2} by ENUMSET1:70 ;
hence x in Lin {v1,v2,v3} by A12, Th14; :: thesis: verum

end;

end;

end;

hence x in Lin {v1,v2,v3} ; :: thesis: verum

end;

suppose A13: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; :: thesis: x in Lin {v1,v2,v3}

then A14: v1 <> v2 ;
A15: v1 <> v3 by A13;
A16: v2 <> v3 by A13;
deffunc H₁( VECTOR of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A17: f . v1 = a and
A18: f . v2 = b and
A19: f . v3 = c and
A20: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds
f . v = H₁(v) from RLVECT_4:sch 1(A14, A15, A16);
reconsider f = f as Element of Funcs the carrier of V,REAL by FUNCT_2:11;

now

let v be VECTOR of V; :: thesis: ( not v in {v1,v2,v3} implies f . v = 0 )
assume not v in {v1,v2,v3} ; :: thesis: f . v = 0
then ( v <> v1 & v <> v2 & v <> v3 ) by ENUMSET1:def 1;
hence f . v = 0 by A20; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {v1,v2,v3}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v1,v2,v3} )
assume that
A21: x in Carrier f and
A22: not x in {v1,v2,v3} ; :: thesis: contradiction
( x <> v1 & x <> v2 & x <> v3 ) by A22, ENUMSET1:def 1;
then f . x = 0 by A20, A21;
hence contradiction by A21, RLVECT_2:28; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 8;
x = Sum f by A7, A13, A17, A18, A19, Th9;
hence x in Lin {v1,v2,v3} by RLVECT_3:17; :: thesis: verum

end;

end;

end;

hence x in Lin {v1,v2,v3} ; :: thesis: verum