let A, Q, B, C be POINT of BK-model-Plane; ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C )
consider a being Element of BK_model such that
A1:
A = a
and
BK_to_T2 A = BK_to_REAL2 a
by Def01;
consider q being Element of BK_model such that
A2:
Q = q
and
BK_to_T2 Q = BK_to_REAL2 q
by Def01;
consider b being Element of BK_model such that
A3:
B = b
and
BK_to_T2 B = BK_to_REAL2 b
by Def01;
consider c being Element of BK_model such that
A4:
C = c
and
BK_to_T2 C = BK_to_REAL2 c
by Def01;
per cases
( b <> c or b = c )
;
suppose
b <> c
;
ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C )A5:
for
q1,
a1,
b1,
c1 being
POINT of
BK-model-Plane st
q1 <> a1 holds
ex
x being
POINT of
BK-model-Plane st
(
between q1,
a1,
x &
a1,
x equiv b1,
c1 )
proof
let q1,
a1,
b1,
c1 be
POINT of
BK-model-Plane;
( q1 <> a1 implies ex x being POINT of BK-model-Plane st
( between q1,a1,x & a1,x equiv b1,c1 ) )
assume A6:
q1 <> a1
;
ex x being POINT of BK-model-Plane st
( between q1,a1,x & a1,x equiv b1,c1 )
reconsider Q1 =
q1,
A1 =
a1,
B1 =
b1,
C1 =
c1 as
Element of
BK_model ;
reconsider pQ1 =
Q1,
pA1 =
A1,
pB1 =
B1,
pC1 =
C1 as non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) by Th61;
consider qaR being
Element of
absolute such that A7:
for
p,
q,
r being non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) st
p = q1 &
q = a1 &
r = qaR holds
between RP3_to_T2 p,
RP3_to_T2 q,
RP3_to_T2 r
by A6, Th58;
reconsider pqaR =
qaR as non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) by Th62;
per cases
( B1 = C1 or B1 <> C1 )
;
suppose A8:
B1 = C1
;
ex x being POINT of BK-model-Plane st
( between q1,a1,x & a1,x equiv b1,c1 )reconsider x =
a1 as
Element of
BK_model ;
reconsider x =
x as
POINT of
BK-model-Plane ;
take
x
;
( between q1,a1,x & a1,x equiv b1,c1 )
Tn2TR (BK_to_T2 a1) in LSeg (
(Tn2TR (BK_to_T2 q1)),
(Tn2TR (BK_to_T2 x)))
by RLTOPSP1:68;
then
between BK_to_T2 q1,
BK_to_T2 a1,
BK_to_T2 x
by GTARSKI2:20;
hence
between q1,
a1,
x
by Th05;
a1,x equiv b1,c1thus
a1,
x equiv b1,
c1
by A8, Th60;
verum end; suppose A9:
B1 <> C1
;
ex x being POINT of BK-model-Plane st
( between q1,a1,x & a1,x equiv b1,c1 )consider bcP being
Element of
absolute such that A10:
for
p,
q,
r being non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) st
p = b1 &
q = c1 &
r = bcP holds
between RP3_to_T2 p,
RP3_to_T2 q,
RP3_to_T2 r
by A9, Th58;
reconsider pbcP =
bcP as non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) by Th62;
consider N being
invertible Matrix of 3,
F_Real such that A11:
(homography N) .: absolute = absolute
and A12:
(homography N) . B1 = A1
and A13:
(homography N) . bcP = qaR
by BKMODEL2:56;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum }
;
then reconsider h =
homography N as
Element of
EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry
by A11, BKMODEL2:def 6;
then
h in EnsK-isometry
by BKMODEL2:def 7;
then reconsider h =
homography N as
Element of
SubGroupK-isometry by BKMODEL2:def 8;
h = homography N
;
then reconsider x =
(homography N) . C1 as
Element of
BK_model by BKMODEL3:36;
reconsider x =
x as
POINT of
BK-model-Plane ;
reconsider px =
x as non
point_at_infty Element of
(ProjectiveSpace (TOP-REAL 3)) by Th61;
take
x
;
( between q1,a1,x & a1,x equiv b1,c1 )now ( between q1,a1,x & a1,x equiv b1,c1 )thus
between q1,
a1,
x
a1,x equiv b1,c1proof
A14:
between RP3_to_T2 pQ1,
RP3_to_T2 pA1,
RP3_to_T2 pqaR
by A7;
(
between RP3_to_T2 pB1,
RP3_to_T2 pC1,
RP3_to_T2 pbcP &
h = homography N &
pB1 in BK_model &
pC1 in BK_model &
pbcP in absolute )
by A10;
then A15:
between RP3_to_T2 pA1,
RP3_to_T2 px,
RP3_to_T2 pqaR
by A12, A13, Th41;
set tq =
RP3_to_T2 pQ1;
set ta =
RP3_to_T2 pA1;
set tx =
RP3_to_T2 px;
set tr =
RP3_to_T2 pqaR;
A16:
between RP3_to_T2 pQ1,
RP3_to_T2 pA1,
RP3_to_T2 px
by A15, A14, GTARSKI3:17;
hence
between q1,
a1,
x
by A16, Th05;
verum
end;
ex
h being
Element of
SubGroupK-isometry ex
N being
invertible Matrix of 3,
F_Real st
(
h = homography N &
(homography N) . a1 = b1 &
(homography N) . x = c1 )
hence
a1,
x equiv b1,
c1
by BKMODEL3:def 8;
verum end; hence
(
between q1,
a1,
x &
a1,
x equiv b1,
c1 )
;
verum end; end;
end;
(
q = a implies ex
x being
POINT of
BK-model-Plane st
(
between Q,
A,
x &
A,
x equiv B,
C ) )
proof
assume A24:
q = a
;
ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C )
consider Q3 being
Element of
BK_model such that A25:
a <> Q3
by BKMODEL3:11;
reconsider q3 =
Q3 as
Element of
BK-model-Plane ;
consider x being
POINT of
BK-model-Plane such that
between q3,
A,
x
and A26:
A,
x equiv B,
C
by A25, A1, A5;
take
x
;
( between Q,A,x & A,x equiv B,C )
between BK_to_T2 A,
BK_to_T2 A,
BK_to_T2 x
by GTARSKI1:17;
hence
(
between Q,
A,
x &
A,
x equiv B,
C )
by A26, A1, A24, A2, Th05;
verum
end; hence
ex
x being
POINT of
BK-model-Plane st
(
between Q,
A,
x &
A,
x equiv B,
C )
by A1, A2, A5;
verum end; suppose A27:
b = c
;
ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C )set X =
A;
take
A
;
( between Q,A,A & A,A equiv B,C )
between BK_to_T2 Q,
BK_to_T2 A,
BK_to_T2 A
by GTARSKI1:14;
hence
between Q,
A,
A
by Th05;
A,A equiv B,Cthus
A,
A equiv B,
C
by A27, A3, A4, Th60;
verum end; end;