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 :: thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)

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:14;
x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, Th6;
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:30, ENUMSET1:59;

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

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

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, Th11;
x = ((a * v1) + (b * v2)) + (0. V) by A5, RLVECT_1:4
.= ((a * v1) + (b * v2)) + (0 * v3) by RLVECT_1:10 ;
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, Th11;
x = ((a * v1) + (0. V)) + (b * v3) by A6, RLVECT_1:4
.= ((a * v1) + (0 * v2)) + (b * v3) by RLVECT_1:10 ;
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 :: thesis: x in Lin {v1,v2,v3}

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 :: thesis: x in Lin {v1,v2,v3}

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:30, RLVECT_1:def 6;
hence x in Lin {v1,v2,v3} by Th11; :: thesis: verum

end;

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

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

end;

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

then A12: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
.= {v1,v2} by ENUMSET1:30 ;
x = (a * v1) + ((b * v2) + (c * v2)) by A7, A11, RLVECT_1:def 3
.= (a * v1) + ((b + c) * v2) by RLVECT_1:def 6 ;
hence x in Lin {v1,v2,v3} by A12, Th11; :: 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}

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

now :: thesis: for v being VECTOR of V st not v in {v1,v2,v3} holds
f . v = 0

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

end;

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

proof

let x be object ; :: 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
A23: x <> v3 by A22, ENUMSET1:def 1;
( x <> v1 & x <> v2 ) by A22, ENUMSET1:def 1;
then f . x = 0 by A18, A21, A23;
hence contradiction by A21, RLVECT_2:19; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
x = Sum f by A7, A13, A17, Th6;
hence x in Lin {v1,v2,v3} by RLVECT_3:14; :: thesis: verum

end;

end;

end;

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