let P, Q, R be Element of (ProjectiveSpace (TOP-REAL 3)); for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 <> 0 & v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds
( R <> P & R <> Q )
let u, v, w be non zero Element of (TOP-REAL 3); ( P = Dir u & Q = Dir v & R = Dir w & u `3 <> 0 & v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| implies ( R <> P & R <> Q ) )
assume that
A1:
P = Dir u
and
A2:
Q = Dir v
and
A3:
R = Dir w
and
A4:
u `3 <> 0
and
A5:
v `3 = 0
and
A6:
w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]|
; ( R <> P & R <> Q )
hereby R <> Q
assume
R = P
;
contradictionthen
are_Prop u,
w
by A1, A3, ANPROJ_1:22;
then consider a being
Real such that
a <> 0
and A7:
u = a * w
by ANPROJ_1:1;
A8:
|[(u `1),(u `2),(u `3)]| =
u
by EUCLID_5:3
.=
|[(a * (w `1)),(a * (w `2)),(a * (w `3))]|
by A7, EUCLID_5:7
;
then
|[(u `1),(u `2),(u `3)]| = |[(a * (w `1)),(a * (w `2)),(a * (u `3))]|
by A6, EUCLID_5:2;
then
u `3 = a * (u `3)
by FINSEQ_1:78;
then A9:
a = 1
by A4, XCMPLX_1:7;
(
w `1 = (u `1) + (v `1) &
w `2 = (u `2) + (v `2) &
w `3 = u `3 )
by A6, EUCLID_5:2;
then
(
u `1 = (u `1) + (v `1) &
u `2 = (u `2) + (v `2) )
by A8, A9, FINSEQ_1:78;
hence
contradiction
by A5, EUCLID_5:3, EUCLID_5:4;
verum
end;
hereby verum
assume
R = Q
;
contradictionthen
are_Prop v,
w
by A2, A3, ANPROJ_1:22;
then consider b being
Real such that A11:
b <> 0
and A12:
v = b * w
by ANPROJ_1:1;
|[(v `1),(v `2),(v `3)]| =
v
by EUCLID_5:3
.=
|[(b * (w `1)),(b * (w `2)),(b * (w `3))]|
by A12, EUCLID_5:7
;
then
|[(v `1),(v `2),(v `3)]| = |[(b * (w `1)),(b * (w `2)),(b * (u `3))]|
by A6, EUCLID_5:2;
hence
contradiction
by A4, A11, A5, FINSEQ_1:78;
verum
end;