let P1, P2 be Element of absolute ; for Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
let Q be Element of BK_model ; for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
let u, v, w be non zero Element of (TOP-REAL 3); ( Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear implies ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) ) )
assume that
A1:
( Dir u = P1 & Dir v = P2 & Dir w = Q )
and
A2:
( u . 3 = 1 & v . 3 = 1 & w . 3 = 1 )
and
A3:
( v . 1 = - (u . 1) & v . 2 = - (u . 2) )
and
A4:
P1,Q,P2 are_collinear
; ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
( u . 1 = u `1 & u . 2 = u `2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
then A6:
( u `3 = 1 & v `3 = 1 & w `3 = 1 & v `1 = - (u `1) & v `2 = - (u `2) )
by A2, A3, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
P1,P2,Q are_collinear
by A4, COLLSP:4;
then A7: 0 =
|{u,v,w}|
by A1, BKMODEL1:1
.=
(((((((u `1) * (- (u `2))) * 1) - ((1 * (- (u `2))) * (w `1))) - (((u `1) * 1) * (w `2))) + (((u `2) * 1) * (w `1))) - (((u `2) * (- (u `1))) * 1)) + ((1 * (- (u `1))) * (w `2))
by A6, ANPROJ_8:27
.=
2 * (((u `2) * (w `1)) - ((u `1) * (w `2)))
;
consider u9 being non zero Element of (TOP-REAL 3) such that
A8:
((u9 . 1) ^2) + ((u9 . 2) ^2) = 1
and
A9:
u9 . 3 = 1
and
A10:
P1 = Dir u9
by BKMODEL1:89;
A11:
u = u9
by A9, A10, A1, A2, BKMODEL1:43;
( not u `1 = 0 or not u `2 = 0 )
then consider e being Real such that
A13:
( w `1 = e * (u `1) & w `2 = e * (u `2) )
by A7, BKMODEL1:2;
( w . 1 = e * (u `1) & w . 2 = e * (u `2) )
by A13, EUCLID_5:def 1, EUCLID_5:def 2;
then A14:
( w . 1 = e * (u . 1) & w . 2 = e * (u . 2) )
by EUCLID_5:def 1, EUCLID_5:def 2;