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
deffunc H1( VECTOR of V) -> Element of REAL = zz;
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 ) )
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
A5: ( f . u = aa & f . v = bb & f . w = cc ) and
A6: for x being VECTOR of V st x <> u & x <> v & x <> w holds
f . x = H1(x) from RLVECT_4:sch 1(A1, A2, A3);
 reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now :: thesis: for x being VECTOR of V st not x in {u,v,w} holds
f . x = 0
let x be VECTOR of V; :: thesis: ( not x in {u,v,w} implies f . x = 0 )
assume A7: not x in {u,v,w} ; :: thesis: f . x = 0
then A8: x <> w by ENUMSET1:def 1;
( x <> u & x <> v ) by A7, ENUMSET1:def 1;
hence f . x = 0 by A6, A8; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {u,v,w}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {u,v,w} )
assume A9: x in Carrier f ; :: thesis: x in {u,v,w}
then f . x <> 0 by RLVECT_2:19;
then ( x = u or x = v or x = w ) by A6, A9;
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 6;
assume ((a * u) + (b * v)) + (c * w) = 0. V ; :: thesis: ( a = 0 & b = 0 & c = 0 )
then A10: 0. V = Sum f by A1, A2, A3, A5, Th6;
then A11: not u in Carrier f by A4;
( not v in Carrier f & not w in Carrier f ) by A4, A10;
hence ( a = 0 & b = 0 & c = 0 ) by A5, A11, RLVECT_2:19; :: thesis: verum
end;
assume A12: 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 )
A13: now :: thesis: ( not u = v & not u = w & not v = w )
assume A14: ( u = v or u = w or v = w ) ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( u = v or u = w or v = w ) by A14;
suppose u = v ; :: thesis: contradiction
then ((1 * u) + ((- 1) * v)) + (0 * w) = (u + ((- 1) * u)) + (0 * w) by RLVECT_1:def 8
.= (u + (- u)) + (0 * w) by RLVECT_1:16
.= (u + (- u)) + (0. V) by RLVECT_1:10
.= u + (- u) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence contradiction by A12; :: thesis: verum
end;
suppose u = w ; :: thesis: contradiction
then ((1 * u) + (0 * v)) + ((- 1) * w) = (u + (0 * v)) + ((- 1) * u) by RLVECT_1:def 8
.= (u + (0. V)) + ((- 1) * u) by RLVECT_1:10
.= (u + (0. V)) + (- u) by RLVECT_1:16
.= u + (- u) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence contradiction by A12; :: thesis: verum
end;
suppose v = w ; :: thesis: contradiction
then ((0 * u) + (1 * v)) + ((- 1) * w) = ((0 * u) + (1 * v)) + (- v) by RLVECT_1:16
.= ((0. V) + (1 * v)) + (- v) by RLVECT_1:10
.= ((0. V) + v) + (- v) by RLVECT_1:def 8
.= v + (- v) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence contradiction by A12; :: 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 A15: (((l . u) * u) + ((l . v) * v)) + ((l . w) * w) = 0. V by A13, Th6;
then A16: l . w = 0 by A12;
A17: ( l . u = 0 & l . v = 0 ) by A12, A15;
thus Carrier l c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Carrier l
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in {} )
assume A18: x in Carrier l ; :: thesis: x in {}
Carrier l c= {u,v,w} by RLVECT_2:def 6;
then ( x = u or x = v or x = w ) by A18, ENUMSET1:def 1;
hence x in {} by A17, A16, A18, RLVECT_2:19; :: thesis: verum
end;
thus {} c= Carrier l ; :: thesis: verum