let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V holds
( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) )
let u, v, w be VECTOR of V; :: thesis: ( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) )
thus ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent implies for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) :: thesis: ( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) implies ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) )

proof

assume that
A1: u <> v and
A2: u <> w and
A3: v <> w and
A4: {u,v,w} is linearly-independent ; :: thesis: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 )
let a, b, c be Real; :: thesis: ( ((a * u) + (b * v)) + (c * w) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume A5: ((a * u) + (b * v)) + (c * w) = 0. V ; :: thesis: ( a = 0 & b = 0 & c = 0 )
deffunc H₁( VECTOR of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A6: f . u = a and
A7: f . v = b and
A8: f . w = c and
A9: for x being VECTOR of V st x <> u & x <> v & x <> w holds
f . x = H₁(x) from RLVECT_4:sch 1(A1, A2, A3);
reconsider f = f as Element of Funcs the carrier of V,REAL by FUNCT_2:11;

now

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

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {u,v,w}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,v,w} )
assume A10: x in Carrier f ; :: thesis: x in {u,v,w}
then f . x <> 0 by RLVECT_2:28;
then ( x = u or x = v or x = w ) by A9, A10;
hence x in {u,v,w} by ENUMSET1:def 1; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {u,v,w} by RLVECT_2:def 8;
0. V = Sum f by A1, A2, A3, A5, A6, A7, A8, Th9;
then ( not v in Carrier f & not w in Carrier f & not u in Carrier f ) by A4, RLVECT_3:def 1;
hence ( a = 0 & b = 0 & c = 0 ) by A6, A7, A8, RLVECT_2:28; :: thesis: verum

end;

assume A11: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; :: thesis: ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent )

A12: now

assume A13: ( u = v or u = w or v = w ) ; :: thesis: contradiction

now

per cases ( u = v or u = w or v = w ) by A13;

suppose u = v ; :: thesis: contradiction

then ((1 * u) + ((- 1) * v)) + (0 * w) = (u + ((- 1) * u)) + (0 * w) by RLVECT_1:def 9
.= (u + (- u)) + (0 * w) by RLVECT_1:29
.= (u + (- u)) + (0. V) by RLVECT_1:23
.= u + (- u) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
hence contradiction by A11; :: thesis: verum

end;

suppose u = w ; :: thesis: contradiction

then ((1 * u) + (0 * v)) + ((- 1) * w) = (u + (0 * v)) + ((- 1) * u) by RLVECT_1:def 9
.= (u + (0. V)) + ((- 1) * u) by RLVECT_1:23
.= (u + (0. V)) + (- u) by RLVECT_1:29
.= u + (- u) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
hence contradiction by A11; :: thesis: verum

end;

suppose v = w ; :: thesis: contradiction

then ((0 * u) + (1 * v)) + ((- 1) * w) = ((0 * u) + (1 * v)) + (- v) by RLVECT_1:29
.= ((0. V) + (1 * v)) + (- v) by RLVECT_1:23
.= ((0. V) + v) + (- v) by RLVECT_1:def 9
.= v + (- v) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
hence contradiction by A11; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence ( u <> v & u <> w & v <> w ) ; :: thesis: {u,v,w} is linearly-independent
let l be Linear_Combination of {u,v,w}; :: according to RLVECT_3:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume Sum l = 0. V ; :: thesis: Carrier l = {}
then (((l . u) * u) + ((l . v) * v)) + ((l . w) * w) = 0. V by A12, Th9;
then A14: ( l . u = 0 & l . v = 0 & l . w = 0 ) by A11;
thus Carrier l c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Carrier l

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in {} )
assume A15: x in Carrier l ; :: thesis: x in {}
Carrier l c= {u,v,w} by RLVECT_2:def 8;
then ( x = u or x = v or x = w ) by A15, ENUMSET1:def 1;
hence x in {} by A14, A15, RLVECT_2:28; :: thesis: verum

end;

thus {} c= Carrier l by XBOOLE_1:2; :: thesis: verum