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 )

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 )

hence
( are_Prop u,v or u = 0. V or v = 0. V )
; :: thesis: verumassume 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

end;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;

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;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

then A15:
b1 " <> 0
by XCMPLX_1:202;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 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

A16: now :: thesis: not b2 * (b1 ") = 0

u = (0. V) + (b1 * q)
by A7, A10, RLVECT_1:10;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;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

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

now :: thesis: ( a1 <> 0 & a2 <> 0 & not are_Prop u,v & not u = 0. V implies v = 0. V )

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

A18: a1 <> 0 and

A19: a2 <> 0 ; :: thesis: ( are_Prop u,v or u = 0. V or v = 0. V )

end;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;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

now :: thesis: ( b1 <> 0 implies are_Prop u,v )

hence
( are_Prop u,v or u = 0. V or v = 0. V )
by A20; :: thesis: verumA24:
( 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;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