let V be RealUnitarySpace; :: thesis: for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
let v1, v2, w1, w2 be VECTOR of V; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} implies ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) )
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent and
A3: v1 in Lin {w1,w2} and
A4: v2 in Lin {w1,w2} ; :: thesis: ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
consider r1, r2 being Real such that
A5: v1 = (r1 * w1) + (r2 * w2) by A3, Th32;
consider r3, r4 being Real such that
A6: v2 = (r3 * w1) + (r4 * w2) by A4, Th32;
set t = (r1 * r4) - (r2 * r3);
A7: now :: thesis: ( r1 = 0 implies not r2 = 0 )
assume ( r1 = 0 & r2 = 0 ) ; :: thesis: contradiction
then v1 = (0. V) + (0 * w2) by A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A2, RLVECT_3:11; :: thesis: verum
end;
now :: thesis: not r1 * r4 = r2 * r3
assume A8: r1 * r4 = r2 * r3 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( r1 <> 0 or r2 <> 0 ) by A7;
suppose A9: r1 <> 0 ; :: thesis: contradiction
((r1 ") * r1) * r4 = (r1 ") * (r2 * r3) by A8, XCMPLX_1:4;
then 1 * r4 = (r1 ") * (r2 * r3) by A9, XCMPLX_0:def 7;
then v2 = (r3 * w1) + ((r3 * ((r1 ") * r2)) * w2) by A6
.= (r3 * w1) + (r3 * (((r1 ") * r2) * w2)) by RLVECT_1:def 7
.= (r3 * 1) * (w1 + (((r1 ") * r2) * w2)) by RLVECT_1:def 5
.= (r3 * ((r1 ") * r1)) * (w1 + (((r1 ") * r2) * w2)) by A9, XCMPLX_0:def 7
.= ((r3 * (r1 ")) * r1) * (w1 + (((r1 ") * r2) * w2))
.= (r3 * (r1 ")) * (r1 * (w1 + (((r1 ") * r2) * w2))) by RLVECT_1:def 7
.= (r3 * (r1 ")) * ((r1 * w1) + (r1 * (((r1 ") * r2) * w2))) by RLVECT_1:def 5
.= (r3 * (r1 ")) * ((r1 * w1) + ((r1 * ((r1 ") * r2)) * w2)) by RLVECT_1:def 7
.= (r3 * (r1 ")) * ((r1 * w1) + (((r1 * (r1 ")) * r2) * w2))
.= (r3 * (r1 ")) * ((r1 * w1) + ((1 * r2) * w2)) by A9, XCMPLX_0:def 7
.= (r3 * (r1 ")) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:12; :: thesis: verum
end;
suppose A10: r2 <> 0 ; :: thesis: contradiction
(r2 ") * (r1 * r4) = (r2 ") * (r2 * r3) by A8
.= ((r2 ") * r2) * r3
.= 1 * r3 by A10, XCMPLX_0:def 7
.= r3 ;
then v2 = ((r4 * ((r2 ") * r1)) * w1) + (r4 * w2) by A6
.= (r4 * (((r2 ") * r1) * w1)) + (r4 * w2) by RLVECT_1:def 7
.= (r4 * 1) * ((((r2 ") * r1) * w1) + w2) by RLVECT_1:def 5
.= (r4 * ((r2 ") * r2)) * ((((r2 ") * r1) * w1) + w2) by A10, XCMPLX_0:def 7
.= ((r4 * (r2 ")) * r2) * ((((r2 ") * r1) * w1) + w2)
.= (r4 * (r2 ")) * (r2 * ((((r2 ") * r1) * w1) + w2)) by RLVECT_1:def 7
.= (r4 * (r2 ")) * ((r2 * (((r2 ") * r1) * w1)) + (r2 * w2)) by RLVECT_1:def 5
.= (r4 * (r2 ")) * (((r2 * ((r2 ") * r1)) * w1) + (r2 * w2)) by RLVECT_1:def 7
.= (r4 * (r2 ")) * ((((r2 * (r2 ")) * r1) * w1) + (r2 * w2))
.= (r4 * (r2 ")) * (((1 * r1) * w1) + (r2 * w2)) by A10, XCMPLX_0:def 7
.= (r4 * (r2 ")) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then A11: (r1 * r4) - (r2 * r3) <> 0 ;
A12: now :: thesis: ( r2 <> 0 implies ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) )
assume A13: r2 <> 0 ; :: thesis: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) )
(r2 ") * v1 = ((r2 ") * (r1 * w1)) + ((r2 ") * (r2 * w2)) by A5, RLVECT_1:def 5
.= (((r2 ") * r1) * w1) + ((r2 ") * (r2 * w2)) by RLVECT_1:def 7
.= (((r2 ") * r1) * w1) + (((r2 ") * r2) * w2) by RLVECT_1:def 7
.= (((r2 ") * r1) * w1) + (1 * w2) by A13, XCMPLX_0:def 7
.= (((r2 ") * r1) * w1) + w2 by RLVECT_1:def 8 ;
then A14: w2 = ((r2 ") * v1) - (((r2 ") * r1) * w1) by RLSUB_2:61;
then w2 = ((r2 ") * v1) - ((r2 ") * (r1 * w1)) by RLVECT_1:def 7;
then v2 = (r3 * w1) + (r4 * ((r2 ") * (v1 - (r1 * w1)))) by A6, RLVECT_1:34
.= (r3 * w1) + ((r4 * (r2 ")) * (v1 - (r1 * w1))) by RLVECT_1:def 7
.= (r3 * w1) + (((r4 * (r2 ")) * v1) - ((r4 * (r2 ")) * (r1 * w1))) by RLVECT_1:34
.= ((r3 * w1) + ((r4 * (r2 ")) * v1)) - ((r4 * (r2 ")) * (r1 * w1)) by RLVECT_1:def 3
.= (((r4 * (r2 ")) * v1) + (r3 * w1)) - (((r4 * (r2 ")) * r1) * w1) by RLVECT_1:def 7
.= ((r4 * (r2 ")) * v1) + ((r3 * w1) - (((r4 * (r2 ")) * r1) * w1)) by RLVECT_1:def 3
.= ((r4 * (r2 ")) * v1) + ((r3 - ((r4 * (r2 ")) * r1)) * w1) by RLVECT_1:35 ;
then r2 * v2 = (r2 * ((r4 * (r2 ")) * v1)) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def 5
.= ((r2 * (r4 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def 7
.= ((r4 * (r2 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1))
.= ((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by A13, XCMPLX_0:def 7
.= (r4 * v1) + ((r2 * (r3 - ((r4 * (r2 ")) * r1))) * w1) by RLVECT_1:def 7
.= (r4 * v1) + (((r2 * r3) - ((r2 * (r2 ")) * (r4 * r1))) * w1)
.= (r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1) by A13, XCMPLX_0:def 7
.= (r4 * v1) + ((- ((r1 * r4) - (r2 * r3))) * w1)
.= (r4 * v1) + (- (((r1 * r4) - (r2 * r3)) * w1)) by RLVECT_4:3 ;
then - (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1) by RLSUB_2:61;
then ((r1 * r4) - (r2 * r3)) * w1 = - ((r2 * v2) - (r4 * v1)) by RLVECT_1:17
.= (r4 * v1) + (- (r2 * v2)) by RLVECT_1:33 ;
then ((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def 7;
then 1 * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by A11, XCMPLX_0:def 7;
then w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def 8
.= ((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def 5
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def 7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * ((- r2) * v2)) by RLVECT_4:3
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((((r1 * r4) - (r2 * r3)) ") * (- r2)) * v2) by RLVECT_1:def 7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((- (((r1 * r4) - (r2 * r3)) ")) * r2) * v2)
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- (((r1 * r4) - (r2 * r3)) ")) * (r2 * v2)) by RLVECT_1:def 7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2))) by RLVECT_4:3 ;
hence w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by RLVECT_1:def 7; :: thesis: w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2)
then A15: w2 = ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))) by A14, RLVECT_1:def 7
.= ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2)))) by RLVECT_1:def 7
.= ((r2 ") * v1) - (((r2 ") * r1) * ((((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:34
.= ((r2 ") * v1) - (((r1 * (r2 ")) * (((r1 * r4) - (r2 * r3)) ")) * ((r4 * v1) - (r2 * v2))) by RLVECT_1:def 7
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * v1) - (r2 * v2)))
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def 7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def 7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - ((r2 ") * (r2 * v2))))) by RLVECT_1:34
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - (((r2 ") * r2) * v2)))) by RLVECT_1:def 7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (((r2 ") * r2) * v2)))) by RLVECT_1:def 7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (1 * v2)))) by A13, XCMPLX_0:def 7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - v2))) by RLVECT_1:def 8
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2)) by RLVECT_1:29
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def 7
.= (((r2 ") * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def 7
.= (((r2 ") * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def 7
.= (((r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:35 ;
(r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) = (r2 ") * (1 - (r1 * ((((r1 * r4) - (r2 * r3)) ") * r4)))
.= (r2 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) - ((((r1 * r4) - (r2 * r3)) ") * (r1 * r4))) by A11, XCMPLX_0:def 7
.= (((r2 ") * r2) * (((r1 * r4) - (r2 * r3)) ")) * (- r3)
.= (1 * (((r1 * r4) - (r2 * r3)) ")) * (- r3) by A13, XCMPLX_0:def 7
.= - ((((r1 * r4) - (r2 * r3)) ") * r3) ;
hence w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by A15, RLVECT_4:3; :: thesis: verum
end;
set a4 = (((r1 * r4) - (r2 * r3)) ") * r1;
set a3 = - ((((r1 * r4) - (r2 * r3)) ") * r3);
set a2 = - ((((r1 * r4) - (r2 * r3)) ") * r2);
set a1 = (((r1 * r4) - (r2 * r3)) ") * r4;
now :: thesis: ( r1 <> 0 implies ( w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) ) )
assume A16: r1 <> 0 ; :: thesis: ( w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) )
A17: (r1 ") + ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) = (r1 ") * (1 + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3)))
.= (r1 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3))) by A11, XCMPLX_0:def 7
.= (((r1 * r4) - (r2 * r3)) ") * (((r1 ") * r1) * r4)
.= (((r1 * r4) - (r2 * r3)) ") * (1 * r4) by A16, XCMPLX_0:def 7
.= (((r1 * r4) - (r2 * r3)) ") * r4 ;
(r1 ") * v1 = ((r1 ") * (r1 * w1)) + ((r1 ") * (r2 * w2)) by A5, RLVECT_1:def 5
.= (((r1 ") * r1) * w1) + ((r1 ") * (r2 * w2)) by RLVECT_1:def 7
.= (1 * w1) + ((r1 ") * (r2 * w2)) by A16, XCMPLX_0:def 7
.= w1 + ((r1 ") * (r2 * w2)) by RLVECT_1:def 8
.= w1 + ((r2 * (r1 ")) * w2) by RLVECT_1:def 7 ;
then A18: w1 = ((r1 ") * v1) - ((r2 * (r1 ")) * w2) by RLSUB_2:61;
then v2 = ((r3 * ((r1 ") * v1)) - (r3 * ((r2 * (r1 ")) * w2))) + (r4 * w2) by A6, RLVECT_1:34
.= (((r3 * (r1 ")) * v1) - (r3 * (((r1 ") * r2) * w2))) + (r4 * w2) by RLVECT_1:def 7
.= (((r3 * (r1 ")) * v1) - ((r3 * ((r1 ") * r2)) * w2)) + (r4 * w2) by RLVECT_1:def 7
.= (((r3 * (r1 ")) * v1) - (((r1 ") * (r3 * r2)) * w2)) + (r4 * w2)
.= ((((r1 ") * r3) * v1) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def 7
.= (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def 7 ;
then r1 * v2 = (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + (r1 * (r4 * w2)) by RLVECT_1:def 5
.= (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def 7
.= ((r1 * ((r1 ") * (r3 * v1))) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:34
.= (((r1 * (r1 ")) * (r3 * v1)) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def 7
.= (((r1 * (r1 ")) * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def 7
.= ((1 * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def 7
.= ((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def 7
.= ((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def 8
.= ((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2) by RLVECT_1:def 8
.= (r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2)) by RLVECT_1:29
.= (r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2)) by RLVECT_1:35
.= (r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2) by RLVECT_4:3
.= (r3 * v1) + (((r1 * r4) - (r2 * r3)) * w2) ;
then (((r1 * r4) - (r2 * r3)) ") * (r1 * v2) = ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (((r1 * r4) - (r2 * r3)) * w2)) by RLVECT_1:def 5
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w2) by RLVECT_1:def 7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (1 * w2) by A11, XCMPLX_0:def 7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + w2 by RLVECT_1:def 8 ;
hence w2 = ((((r1 * r4) - (r2 * r3)) ") * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLSUB_2:61
.= (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLVECT_1:def 7
.= (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:def 7 ;
:: thesis: w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))
hence w1 = ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (r1 ")) * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A18, RLVECT_1:def 5
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + (((r2 * (r1 ")) * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (((r1 ") * r1) * (((r1 * r4) - (r2 * r3)) "))) * v2))
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (1 * (((r1 * r4) - (r2 * r3)) "))) * v2)) by A16, XCMPLX_0:def 7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * ((- (((r1 * r4) - (r2 * r3)) ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_4:3
.= ((r1 ") * v1) - ((((r2 * (r1 ")) * (- (((r1 * r4) - (r2 * r3)) "))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - ((((((- jj) * (((r1 * r4) - (r2 * r3)) ")) * r2) * (r1 ")) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2))
.= ((r1 ") * v1) - (((((- jj) * (((r1 * r4) - (r2 * r3)) ")) * r2) * ((r1 ") * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - ((((- jj) * (((r1 * r4) - (r2 * r3)) ")) * (r2 * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - (((- jj) * ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - ((- ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:16
.= ((r1 ") * v1) - ((- (((((r1 * r4) - (r2 * r3)) ") * r2) * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - ((- ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= ((r1 ") * v1) - ((- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def 7
.= (((r1 ") * v1) - (- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:27
.= (((r1 ") * v1) + (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:17
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by A17, RLVECT_1:def 6 ;
:: thesis: verum
end;
then A19: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2) & w2 = ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) by A7, A12, RLVECT_4:3;
now :: thesis: for u being VECTOR of V holds
( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) )
let u be VECTOR of V; :: thesis: ( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) )
thus ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) :: thesis: ( u in Lin {v1,v2} implies u in Lin {w1,w2} )
proof
assume u in Lin {w1,w2} ; :: thesis: u in Lin {v1,v2}
then consider r5, r6 being Real such that
A20: u = (r5 * w1) + (r6 * w2) by Th32;
u = ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (r6 * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, A20, RLVECT_1:def 5
.= ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 5
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 7
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def 3
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def 3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 6
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def 6 ;
hence u in Lin {v1,v2} by Th32; :: thesis: verum
end;
assume u in Lin {v1,v2} ; :: thesis: u in Lin {w1,w2}
then consider r5, r6 being Real such that
A21: u = (r5 * v1) + (r6 * v2) by Th32;
u = (r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by A5, A6, A21, RLVECT_1:def 5
.= ((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by RLVECT_1:def 5
.= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2)) by RLVECT_1:def 3
.= (((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 3
.= ((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2)) by RLVECT_1:def 7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def 7
.= ((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def 6
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2)) by RLVECT_1:def 3
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2) by RLVECT_1:def 6 ;
hence u in Lin {w1,w2} by Th32; :: thesis: verum
end;
hence Lin {w1,w2} = Lin {v1,v2} by RUSUB_1:25; :: thesis: ( {w1,w2} is linearly-independent & w1 <> w2 )
now :: thesis: for a, b being Real st (a * w1) + (b * w2) = 0. V holds
( not a <> 0 & not b <> 0 )
let a, b be Real; :: thesis: ( (a * w1) + (b * w2) = 0. V implies ( not a <> 0 & not b <> 0 ) )
A22: ((r1 * r4) - (r2 * r3)) " <> 0 by A11, XCMPLX_1:202;
assume (a * w1) + (b * w2) = 0. V ; :: thesis: ( not a <> 0 & not b <> 0 )
then A23: 0. V = ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (b * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, RLVECT_1:def 5
.= ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 5
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def 7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 7
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def 3
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def 3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def 6
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (b * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def 6 ;
then 0 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * a) + ((- r3) * b)) by A1, A2, RLVECT_3:13;
then A24: (r4 * a) - (r3 * b) = 0 by A22, XCMPLX_1:6;
0 = (((r1 * r4) - (r2 * r3)) ") * (((- r2) * a) + (r1 * b)) by A1, A2, A23, RLVECT_3:13;
then A25: (r1 * b) + (- (r2 * a)) = 0 by A22, XCMPLX_1:6;
assume A26: ( a <> 0 or b <> 0 ) ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( a <> 0 or b <> 0 ) by A26;
suppose A27: a <> 0 ; :: thesis: contradiction
(a ") * (r1 * b) = ((a ") * a) * r2 by A25, XCMPLX_1:4;
then (a ") * (r1 * b) = 1 * r2 by A27, XCMPLX_0:def 7;
then r2 = r1 * ((a ") * b) ;
then v1 = (r1 * w1) + (r1 * (((a ") * b) * w2)) by A5, RLVECT_1:def 7;
then A28: v1 = r1 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def 5;
((a ") * a) * r4 = (a ") * (r3 * b) by A24, XCMPLX_1:4;
then 1 * r4 = (a ") * (r3 * b) by A27, XCMPLX_0:def 7;
then r4 = r3 * ((a ") * b) ;
then v2 = (r3 * w1) + (r3 * (((a ") * b) * w2)) by A6, RLVECT_1:def 7;
then v2 = r3 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def 5;
hence contradiction by A1, A2, A28, RLVECT_4:21; :: thesis: verum
end;
suppose A29: b <> 0 ; :: thesis: contradiction
((b ") * b) * r1 = (b ") * (r2 * a) by A25, XCMPLX_1:4;
then 1 * r1 = (b ") * (r2 * a) by A29, XCMPLX_0:def 7;
then r1 = r2 * ((b ") * a) ;
then v1 = (r2 * (((b ") * a) * w1)) + (r2 * w2) by A5, RLVECT_1:def 7;
then A30: v1 = r2 * ((((b ") * a) * w1) + w2) by RLVECT_1:def 5;
((b ") * b) * r3 = (b ") * (r4 * a) by A24, XCMPLX_1:4;
then 1 * r3 = (b ") * (r4 * a) by A29, XCMPLX_0:def 7;
then r3 = r4 * ((b ") * a) ;
then v2 = (r4 * (((b ") * a) * w1)) + (r4 * w2) by A6, RLVECT_1:def 7;
then v2 = r4 * ((((b ") * a) * w1) + w2) by RLVECT_1:def 5;
hence contradiction by A1, A2, A30, RLVECT_4:21; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence ( {w1,w2} is linearly-independent & w1 <> w2 ) by RLVECT_3:13; :: thesis: verum