let P, Q, R be Element of real_projective_plane; for u, v, w being non zero Element of (TOP-REAL 3)
for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
( R in BK_model & R <> P & P,R,Q are_collinear )
let u, v, w be non zero Element of (TOP-REAL 3); for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
( R in BK_model & R <> P & P,R,Q are_collinear )
let a, b, c, d be Real; ( P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| implies ( R in BK_model & R <> P & P,R,Q are_collinear ) )
assume that
A1:
P in BK_model
and
A2:
Q in absolute
and
A3:
P = Dir u
and
A4:
Q = Dir v
and
A5:
R = Dir w
and
A6:
u = |[a,b,1]|
and
A7:
v = |[c,d,1]|
and
A8:
w = |[((a + c) / 2),((b + d) / 2),1]|
; ( R in BK_model & R <> P & P,R,Q are_collinear )
reconsider PBK = P as Element of BK_model by A1;
consider u2 being non zero Element of (TOP-REAL 3) such that
A9:
( Dir u2 = PBK & u2 . 3 = 1 & BK_to_REAL2 PBK = |[(u2 . 1),(u2 . 2)]| )
by Def01;
A10: u . 3 =
u `3
by EUCLID_5:def 3
.=
1
by A6, EUCLID_5:2
;
then A11:
u = u2
by A3, A9, BKMODEL1:43;
reconsider S = |[(u . 1),(u . 2)]| as Element of (TOP-REAL 2) ;
A12: |.(S - |[0,0]|).| =
|.(|[(S `1),(S `2)]| - |[0,0]|).|
by EUCLID:53
.=
|.|[((S `1) - 0),((S `2) - 0)]|.|
by EUCLID:62
.=
|.S.|
by EUCLID:53
;
1 ^2 = 1
;
then
|.S.| ^2 < 1
by A9, A11, TOPREAL9:45, A12, SQUARE_1:16;
then
((S `1) ^2) + ((S `2) ^2) < 1
by JGRAPH_3:1;
then
((u . 1) ^2) + ((S `2) ^2) < 1
by EUCLID:52;
then A13:
((u . 1) ^2) + ((u . 2) ^2) < 1
by EUCLID:52;
( u `1 = a & u `2 = b & v `1 = c & v `2 = d )
by A6, A7, EUCLID_5:2;
then A14:
( u . 1 = a & u . 2 = b & v . 1 = c & v . 2 = d )
by EUCLID_5:def 1, EUCLID_5:def 2;
v `3 = 1
by A7, EUCLID_5:2;
then
v . 3 = 1
by EUCLID_5:def 3;
then
|[(v . 1),(v . 2)]| in circle (0,0,1)
by A2, A4, BKMODEL1:84;
then consider pp being Point of (TOP-REAL 2) such that
A15:
|[(v . 1),(v . 2)]| = pp
and
A16:
|.(pp - |[0,0]|).| = 1
;
1 =
|.|[((v . 1) - 0),((v . 2) - 0)]|.|
by A15, A16, EUCLID:62
.=
|.pp.|
by A15
;
then a17: 1 ^2 =
((pp `1) ^2) + ((pp `2) ^2)
by JGRAPH_1:29
.=
((v . 1) ^2) + ((pp `2) ^2)
by A15, EUCLID:52
.=
((v . 1) ^2) + ((v . 2) ^2)
by A15, EUCLID:52
;
( w `1 = (a + c) / 2 & w `2 = (b + d) / 2 )
by A8, EUCLID_5:2;
then A18:
( w . 1 = (a + c) / 2 & w . 2 = (b + d) / 2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
reconsider R1 = |[(w . 1),(w . 2)]| as Element of (TOP-REAL 2) ;
|.(R1 - |[0,0]|).| ^2 < 1
then
|.(R1 - |[0,0]|).| < 1
by SQUARE_1:52;
then
R1 in inside_of_circle (0,0,1)
;
then reconsider R1 = R1 as Element of inside_of_circle (0,0,1) ;
consider PR1 being Element of (TOP-REAL 2) such that
A20:
PR1 = R1
and
A21:
REAL2_to_BK R1 = Dir |[(PR1 `1),(PR1 `2),1]|
by Def02;
A22:
( w . 1 = w `1 & w . 2 = w `2 & w `3 = 1 )
by A8, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:2;
( PR1 `1 = w . 1 & PR1 `2 = w . 2 )
by A20, EUCLID:52;
then A23:
REAL2_to_BK R1 = Dir w
by A21, A22, EUCLID_5:3;
A24:
P <> R
proof
assume A25:
P = R
;
contradiction
w . 3 =
w `3
by EUCLID_5:def 3
.=
1
by A8, EUCLID_5:2
;
then A26:
(
u `1 = w `1 &
u `2 = w `2 )
by A25, A3, A5, A10, BKMODEL1:43;
(
u `1 = a &
w `1 = (a + c) / 2 &
u `2 = b &
w `2 = (b + d) / 2 )
by A6, A8, EUCLID_5:2;
hence
contradiction
by A26, A6, A7, A3, A4, A1, A2, Th01, XBOOLE_0:def 4;
verum
end;
0 =
|{u,v,w}|
by A6, A7, A8, BKMODEL1:20
.=
- |{u,w,v}|
by ANPROJ_8:29
;
hence
( R in BK_model & R <> P & P,R,Q are_collinear )
by A23, A24, A3, A4, A5, BKMODEL1:1; verum