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 that
A1: not are_Prop p,q and
A2: u = (a1 * p) + (b1 * q) and
A3: v = (a2 * p) + (b2 * q) and
A4: (a1 * b2) - (a2 * b1) = 0 and
A5: ( not p is zero & not q is zero ) ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )

now

assume that
u <> 0. V and
v <> 0. V ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
A6: 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
not are_Prop p,q and
A7: u = (a1 * p) + (b1 * q) and
A8: v = (a2 * p) + (b2 * q) and
A9: (a1 * b2) - (a2 * b1) = 0 and
not p is zero and
not q is zero and
A10: a1 = 0 and
A11: u <> 0. V and
A12: v <> 0. V ; :: thesis: are_Prop u,v
0 = (- a2) * b1 by A9, A10;
then A13: ( - a2 = 0 or b1 = 0 ) by XCMPLX_1:6;

A14: now

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

end;

then A15: b1 " <> 0 by XCMPLX_1:203;

A16: now

assume b2 * (b1 " ) = 0 ; :: thesis: contradiction
then b2 = 0 by A15, XCMPLX_1:6;
then v = (0. V) + (0 * q) by A8, A13, A14, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23 ;
hence contradiction by A12, RLVECT_1:10; :: thesis: verum

end;

u = (0. V) + (b1 * q) by A7, A10, RLVECT_1:23;
then A17: u = b1 * q by RLVECT_1:10;
v = (0. V) + (b2 * q) by A8, A13, A14, RLVECT_1:23;
then v = b2 * q by RLVECT_1:10;
then v = b2 * ((b1 " ) * u) by A14, A17, ANALOAF:12;
then v = (b2 * (b1 " )) * u by RLVECT_1:def 10;
then 1 * v = (b2 * (b1 " )) * u by RLVECT_1:def 11;
hence are_Prop u,v by A16, Def2; :: thesis: verum

end;

now

assume that
A18: a1 <> 0 and
A19: a2 <> 0 ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )

A20: now

a1 " <> 0 by A18, XCMPLX_1:203;
then A21: a2 * (a1 " ) <> 0 by A19, XCMPLX_1:6;
assume A22: b1 = 0 ; :: thesis: are_Prop u,v
then b2 = 0 by A4, A18, XCMPLX_1:6;
then v = (a2 * p) + (0. V) by A3, RLVECT_1:23;
then A23: v = a2 * p by RLVECT_1:10;
u = (a1 * p) + (0. V) by A2, A22, RLVECT_1:23;
then u = a1 * p by RLVECT_1:10;
then v = a2 * ((a1 " ) * u) by A18, A23, ANALOAF:12
.= (a2 * (a1 " )) * u by RLVECT_1:def 10 ;
then 1 * v = (a2 * (a1 " )) * u by RLVECT_1:def 11;
hence are_Prop u,v by A21, Def2; :: thesis: verum

end;

now

A24: ( b2 * u = ((a1 * b2) * p) + ((b2 * b1) * q) & b1 * v = ((a2 * b1) * p) + ((b1 * b2) * q) ) by A2, A3, Lm5;
assume A25: b1 <> 0 ; :: thesis: are_Prop u,v
then b2 <> 0 by A4, A19, XCMPLX_1:6;
hence are_Prop u,v by A4, A25, A24, Def2; :: thesis: verum

end;

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

end;

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

end;

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