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 :: thesis: ( u <> 0. V & v <> 0. V & not are_Prop u,v & not u = 0. V implies v = 0. V )
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 :: thesis: not b1 = 0
assume b1 = 0 ; :: thesis: contradiction
then u = (0. V) + (0 * q) by A7, A10, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10 ;
hence contradiction by A11; :: thesis: verum
end;
then A15: b1 " <> 0 by XCMPLX_1:202;
A16: now :: thesis: not b2 * (b1 ") = 0
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:10
.= (0. V) + (0. V) by RLVECT_1:10 ;
hence contradiction by A12; :: thesis: verum
end;
u = (0. V) + (b1 * q) by A7, A10, RLVECT_1:10;
then A17: u = b1 * q ;
v = (0. V) + (b2 * q) by A8, A13, A14, RLVECT_1:10;
then v = b2 * q ;
then v = b2 * ((b1 ") * u) by A14, A17, ANALOAF:5;
then v = (b2 * (b1 ")) * u by RLVECT_1:def 7;
then 1 * v = (b2 * (b1 ")) * u by RLVECT_1:def 8;
hence are_Prop u,v by A16; :: thesis: verum
end;
now :: thesis: ( a1 <> 0 & a2 <> 0 & not are_Prop u,v & not u = 0. V implies v = 0. V )
assume that
A18: a1 <> 0 and
A19: a2 <> 0 ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )
A20: now :: thesis: ( b1 = 0 implies are_Prop u,v )
a1 " <> 0 by A18, XCMPLX_1:202;
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:10;
then A23: v = a2 * p ;
u = (a1 * p) + (0. V) by A2, A22, RLVECT_1:10;
then u = a1 * p ;
then v = a2 * ((a1 ") * u) by A18, A23, ANALOAF:5
.= (a2 * (a1 ")) * u by RLVECT_1:def 7 ;
then 1 * v = (a2 * (a1 ")) * u by RLVECT_1:def 8;
hence are_Prop u,v by A21; :: thesis: verum
end;
now :: thesis: ( b1 <> 0 implies are_Prop u,v )
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; :: 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