let V be RealUnitarySpace; :: thesis: for v1, v2, v3 being VECTOR of V
for x being set 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: for x being set holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let x be set ; :: 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, Th1;
x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, RLVECT_4:6;
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, Th32;
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, Th32;
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 Th32; :: 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, Th32; :: 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, Th32; :: 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 H1( set ) -> Element of REAL = In (0,REAL);
A14: v1 <> v3 by A13;
A15: v2 <> v3 by A13;
A16: v1 <> v2 by A13;
reconsider a = a, b = b, c = 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 = a & f . v2 = b & f . v3 = c ) and
A18: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds
f . v = H1(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, RLVECT_4:6;
hence x in Lin {v1,v2,v3} by Th1; :: thesis: verum
end;
end;
end;
hence x in Lin {v1,v2,v3} ; :: thesis: verum