let V be RealLinearSpace; :: thesis: for p, q, u, v being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V
let p, q, u, v be Element of V; :: thesis: for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V
let a1, b1, a2, b2 be Real; :: thesis: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V implies v = 0. V )
assume A1: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero ) ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )

now

assume ( u <> 0. V & v <> 0. V ) ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
A2: for p, q, u, v being Element of V
for a1, a2, b1, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V holds
are_Prop u,v

proof

let p, q, u, v be Element of V; :: thesis: for a1, a2, b1, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V holds
are_Prop u,v
let a1, a2, b1, b2 be Real; :: thesis: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero & a1 = 0 & u <> 0. V & v <> 0. V implies are_Prop u,v )
assume that
A3: ( not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & not p is zero & not q is zero ) and
A4: a1 = 0 and
A5: ( u <> 0. V & v <> 0. V ) ; :: thesis: are_Prop u,v
0 = (- a2) * b1 by A3, A4;
then A6: ( - a2 = 0 or b1 = 0 ) by XCMPLX_1:6;

A7: now

assume b1 = 0 ; :: thesis: contradiction
then u = (0. V) + (0 * q) by A3, A4, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23 ;
hence contradiction by A5, RLVECT_1:10; :: thesis: verum

end;

then A8: b1 " <> 0 by XCMPLX_1:203;
( u = (0. V) + (b1 * q) & v = (0. V) + (b2 * q) ) by A3, A4, A6, A7, RLVECT_1:23;
then ( u = b1 * q & v = b2 * q ) by RLVECT_1:10;
then v = b2 * ((b1 " ) * u) by A7, ANALOAF:12;
then v = (b2 * (b1 " )) * u by RLVECT_1:def 9;
then A9: ( 1 * v = (b2 * (b1 " )) * u & 1 <> 0 ) by RLVECT_1:def 9;

now

assume b2 * (b1 " ) = 0 ; :: thesis: contradiction
then b2 = 0 by A8, XCMPLX_1:6;
then v = (0. V) + (0 * q) by A3, A6, A7, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23 ;
hence contradiction by A5, RLVECT_1:10; :: thesis: verum

end;

hence are_Prop u,v by A9, Def2; :: thesis: verum

end;

now

assume A10: ( a1 <> 0 & a2 <> 0 ) ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )

A11: now

assume A12: b1 = 0 ; :: thesis: are_Prop u,v
then b2 = 0 by A1, A10, XCMPLX_1:6;
then ( u = (a1 * p) + (0. V) & v = (a2 * p) + (0. V) ) by A1, A12, RLVECT_1:23;
then A13: ( u = a1 * p & v = a2 * p & a1 " <> 0 ) by A10, RLVECT_1:10, XCMPLX_1:203;
then v = a2 * ((a1 " ) * u) by A10, ANALOAF:12
.= (a2 * (a1 " )) * u by RLVECT_1:def 9 ;
then ( 1 * v = (a2 * (a1 " )) * u & a2 * (a1 " ) <> 0 & 1 <> 0 ) by A10, A13, RLVECT_1:def 9, XCMPLX_1:6;
hence are_Prop u,v by Def2; :: thesis: verum

end;

now

assume A14: b1 <> 0 ; :: thesis: are_Prop u,v
A15: ( b2 * u = ((a1 * b2) * p) + ((b2 * b1) * q) & b1 * v = ((a2 * b1) * p) + ((b1 * b2) * q) ) by A1, Lm5;
b2 <> 0 by A1, A10, A14, XCMPLX_1:6;
hence are_Prop u,v by A1, A14, A15, Def2; :: thesis: verum

end;

hence ( are_Prop u,v or u = 0. V or v = 0. V ) by A11; :: thesis: verum

end;

hence ( are_Prop u,v or u = 0. V or v = 0. V ) by A1, A2; :: thesis: verum

end;

hence ( are_Prop u,v or u = 0. V or v = 0. V ) ; :: thesis: verum