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;
then A11:
(r1 * r4) - (r2 * r3) <> 0
;
set t = (r1 * r4) - (r2 * r3);
A12:
now 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 9
.=
(((r2 " ) * r1) * w1) + ((r2 " ) * (r2 * w2))
by RLVECT_1:def 9
.=
(((r2 " ) * r1) * w1) + (((r2 " ) * r2) * w2)
by RLVECT_1:def 9
.=
(((r2 " ) * r1) * w1) + (1 * w2)
by A13, XCMPLX_0:def 7
.=
(((r2 " ) * r1) * w1) + w2
by RLVECT_1:def 9
;
then A14:
w2 = ((r2 " ) * v1) - (((r2 " ) * r1) * w1)
by RLSUB_2:78;
then
w2 = ((r2 " ) * v1) - ((r2 " ) * (r1 * w1))
by RLVECT_1:def 9;
then v2 =
(r3 * w1) + (r4 * ((r2 " ) * (v1 - (r1 * w1))))
by A6, RLVECT_1:48
.=
(r3 * w1) + ((r4 * (r2 " )) * (v1 - (r1 * w1)))
by RLVECT_1:def 9
.=
(r3 * w1) + (((r4 * (r2 " )) * v1) - ((r4 * (r2 " )) * (r1 * w1)))
by RLVECT_1:48
.=
((r3 * w1) + ((r4 * (r2 " )) * v1)) - ((r4 * (r2 " )) * (r1 * w1))
by RLVECT_1:def 6
.=
(((r4 * (r2 " )) * v1) + (r3 * w1)) - (((r4 * (r2 " )) * r1) * w1)
by RLVECT_1:def 9
.=
((r4 * (r2 " )) * v1) + ((r3 * w1) - (((r4 * (r2 " )) * r1) * w1))
by RLVECT_1:def 6
.=
((r4 * (r2 " )) * v1) + ((r3 - ((r4 * (r2 " )) * r1)) * w1)
by RLVECT_1:49
;
then r2 * v2 =
(r2 * ((r4 * (r2 " )) * v1)) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))
by RLVECT_1:def 9
.=
((r2 * (r4 * (r2 " ))) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))
by RLVECT_1:def 9
.=
((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 9
.=
(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:6
;
then
- (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1)
by RLSUB_2:78;
then ((r1 * r4) - (r2 * r3)) * w1 =
- ((r2 * v2) - (r4 * v1))
by RLVECT_1:30
.=
(r4 * v1) + (- (r2 * v2))
by RLVECT_1:47
;
then
((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) + (- (r2 * v2)))
by RLVECT_1:def 9;
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 9
.=
((((r1 * r4) - (r2 * r3)) " ) * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) " ) * (- (r2 * v2)))
by RLVECT_1:def 9
.=
(((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((((r1 * r4) - (r2 * r3)) " ) * (- (r2 * v2)))
by RLVECT_1:def 9
.=
(((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((((r1 * r4) - (r2 * r3)) " ) * ((- r2) * v2))
by RLVECT_4:6
.=
(((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * (- r2)) * v2)
by RLVECT_1:def 9
.=
(((((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 9
.=
(((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) " ) * (r2 * v2)))
by RLVECT_4:6
;
hence
w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2))
by RLVECT_1:def 9;
:: 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 9
.=
((r2 " ) * v1) - (((r2 " ) * r1) * (((((r1 * r4) - (r2 * r3)) " ) * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) " ) * (r2 * v2))))
by RLVECT_1:def 9
.=
((r2 " ) * v1) - (((r2 " ) * r1) * ((((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) - (r2 * v2))))
by RLVECT_1:48
.=
((r2 " ) * v1) - (((r1 * (r2 " )) * (((r1 * r4) - (r2 * r3)) " )) * ((r4 * v1) - (r2 * v2)))
by RLVECT_1:def 9
.=
((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 9
.=
((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((r2 " ) * ((r4 * v1) - (r2 * v2)))))
by RLVECT_1:def 9
.=
((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * (r4 * v1)) - ((r2 " ) * (r2 * v2)))))
by RLVECT_1:48
.=
((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * (r4 * v1)) - (((r2 " ) * r2) * v2))))
by RLVECT_1:def 9
.=
((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((((r2 " ) * r4) * v1) - (((r2 " ) * r2) * v2))))
by RLVECT_1:def 9
.=
((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 9
.=
((r2 " ) * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) " ) * v2)))
by RLVECT_1:48
.=
((r2 " ) * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * v2)))
by RLVECT_1:48
.=
(((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) " ) * v2))
by RLVECT_1:43
.=
(((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2)
by RLVECT_1:def 9
.=
(((r2 " ) * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) " )) * (((r2 " ) * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2)
by RLVECT_1:def 9
.=
(((r2 " ) * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) " )) * ((r2 " ) * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2)
by RLVECT_1:def 9
.=
(((r2 " ) - ((r1 * (((r1 * r4) - (r2 * r3)) " )) * ((r2 " ) * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2)
by RLVECT_1:49
;
(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:6;
:: thesis: verum end;
now 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 9
.=
(((r1 " ) * r1) * w1) + ((r1 " ) * (r2 * w2))
by RLVECT_1:def 9
.=
(1 * w1) + ((r1 " ) * (r2 * w2))
by A16, XCMPLX_0:def 7
.=
w1 + ((r1 " ) * (r2 * w2))
by RLVECT_1:def 9
.=
w1 + ((r2 * (r1 " )) * w2)
by RLVECT_1:def 9
;
then A18:
w1 = ((r1 " ) * v1) - ((r2 * (r1 " )) * w2)
by RLSUB_2:78;
then v2 =
((r3 * ((r1 " ) * v1)) - (r3 * ((r2 * (r1 " )) * w2))) + (r4 * w2)
by A6, RLVECT_1:48
.=
(((r3 * (r1 " )) * v1) - (r3 * (((r1 " ) * r2) * w2))) + (r4 * w2)
by RLVECT_1:def 9
.=
(((r3 * (r1 " )) * v1) - ((r3 * ((r1 " ) * r2)) * w2)) + (r4 * w2)
by RLVECT_1:def 9
.=
(((r3 * (r1 " )) * v1) - (((r1 " ) * (r3 * r2)) * w2)) + (r4 * w2)
.=
((((r1 " ) * r3) * v1) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2)
by RLVECT_1:def 9
.=
(((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2)
by RLVECT_1:def 9
;
then r1 * v2 =
(r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + (r1 * (r4 * w2))
by RLVECT_1:def 9
.=
(r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)
by RLVECT_1:def 9
.=
((r1 * ((r1 " ) * (r3 * v1))) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)
by RLVECT_1:48
.=
(((r1 * (r1 " )) * (r3 * v1)) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)
by RLVECT_1:def 9
.=
(((r1 * (r1 " )) * (r3 * v1)) - ((r1 * (r1 " )) * ((r3 * r2) * w2))) + ((r1 * r4) * w2)
by RLVECT_1:def 9
.=
((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 9
.=
((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2)
by RLVECT_1:def 9
.=
(r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2))
by RLVECT_1:43
.=
(r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2))
by RLVECT_1:49
.=
(r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2)
by RLVECT_4:6
.=
(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 9
.=
((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) * w2)
by RLVECT_1:def 9
.=
((((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 9
;
hence w2 =
((((r1 * r4) - (r2 * r3)) " ) * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1))
by RLSUB_2:78
.=
(((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) - ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1))
by RLVECT_1:def 9
.=
(- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2)
by RLVECT_1:def 9
;
:: 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 9
.=
((r1 " ) * v1) - (((r2 * (r1 " )) * (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1))) + (((r2 * (r1 " )) * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2))
by RLVECT_1:def 9
.=
((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 9
.=
((r1 " ) * v1) - (((r2 * (r1 " )) * ((- (((r1 * r4) - (r2 * r3)) " )) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_4:6
.=
((r1 " ) * v1) - ((((r2 * (r1 " )) * (- (((r1 * r4) - (r2 * r3)) " ))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - ((((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * r2) * (r1 " )) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
.=
((r1 " ) * v1) - (((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * r2) * ((r1 " ) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - ((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * (r2 * ((r1 " ) * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - (((- 1) * ((((r1 * r4) - (r2 * r3)) " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - ((- ((((r1 * r4) - (r2 * r3)) " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:29
.=
((r1 " ) * v1) - ((- (((((r1 * r4) - (r2 * r3)) " ) * r2) * ((r1 " ) * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - ((- ((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
((r1 " ) * v1) - ((- (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
by RLVECT_1:def 9
.=
(((r1 " ) * v1) - (- (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)
by RLVECT_1:41
.=
(((r1 " ) * v1) + (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)
by RLVECT_1:30
.=
(((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2))
by A17, RLVECT_1:def 9
;
:: 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:6;
set a1 = (((r1 * r4) - (r2 * r3)) " ) * r4;
set a2 = - ((((r1 * r4) - (r2 * r3)) " ) * r2);
set a3 = - ((((r1 * r4) - (r2 * r3)) " ) * r3);
set a4 = (((r1 * r4) - (r2 * r3)) " ) * r1;
now 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} )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 9
.=
((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2)))
by RLVECT_1:def 9
.=
(((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2))
by RLVECT_1:def 6
.=
(((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))
by RLVECT_1:def 6
.=
((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))
by RLVECT_1:def 9
.=
((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))
by RLVECT_1:def 9
.=
((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2))
by RLVECT_1:def 9
.=
((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2)
by RLVECT_1:def 9
.=
((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2)
by RLVECT_1:def 9
.=
(((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2))
by RLVECT_1:def 6
.=
(((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2)
by RLVECT_1:def 9
;
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 )
hence
( {w1,w2} is linearly-independent & w1 <> w2 )
by RLVECT_3:14; :: thesis: verum