let P, Q be Element of BK_model ; ( P <> Q implies ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) ) )
assume A1:
P <> Q
; ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )
consider P1, P2, P3, P4 being Element of absolute , P5 being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A2:
P1 <> P2
and
A3:
P,Q,P1 are_collinear
and
A4:
P,Q,P2 are_collinear
and
A5:
P,P5,P3 are_collinear
and
A6:
Q,P5,P4 are_collinear
and
A7:
P1,P2,P3 are_mutually_distinct
and
A8:
P1,P2,P4 are_mutually_distinct
and
A9:
P5 in (tangent P1) /\ (tangent P2)
by A1, Th44;
consider N1 being invertible Matrix of 3,F_Real such that
A10:
(homography N1) .: absolute = absolute
and
A11:
(homography N1) . Dir101 = P1
and
A12:
(homography N1) . Dirm101 = P2
and
A13:
(homography N1) . Dir011 = P3
and
A14:
(homography N1) . Dir010 = P5
by A7, A9, Th37;
P2,P1,P4 are_mutually_distinct
by A8;
then consider N2 being invertible Matrix of 3,F_Real such that
A15:
(homography N2) .: absolute = absolute
and
A16:
(homography N2) . Dir101 = P2
and
A17:
(homography N2) . Dirm101 = P1
and
A18:
(homography N2) . Dir011 = P4
and
A19:
(homography N2) . Dir010 = P5
by A9, Th37;
reconsider N = N2 * (N1 ~) as invertible Matrix of 3,F_Real ;
A20: (homography N) . P1 =
(homography N2) . ((homography (N1 ~)) . P1)
by ANPROJ_9:13
.=
P2
by A11, A16, ANPROJ_9:15
;
A21: (homography N) . P2 =
(homography N2) . ((homography (N1 ~)) . P2)
by ANPROJ_9:13
.=
P1
by A12, A17, ANPROJ_9:15
;
A22: (homography N) . P3 =
(homography N2) . ((homography (N1 ~)) . P3)
by ANPROJ_9:13
.=
P4
by A13, A18, ANPROJ_9:15
;
A23: (homography N) . P5 =
(homography N2) . ((homography (N1 ~)) . P5)
by ANPROJ_9:13
.=
P5
by A14, A19, ANPROJ_9:15
;
homography N1 in EnsHomography3
by ANPROJ_9:def 1;
then reconsider h1 = homography N1 as Element of EnsHomography3 ;
h1 is_K-isometry
by A10;
then
h1 in EnsK-isometry
;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography N2 in EnsHomography3
by ANPROJ_9:def 1;
then reconsider h2 = homography N2 as Element of EnsHomography3 ;
h2 is_K-isometry
by A15;
then
h2 in EnsK-isometry
;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography (N1 ~) in EnsHomography3
by ANPROJ_9:def 1;
then reconsider h3 = homography (N1 ~) as Element of EnsHomography3 ;
A24:
hsg1 " = h3
by Th36;
set H = EnsK-isometry ;
set G = GroupHomography3 ;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1 " as Element of GroupHomography3 by A24, ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry ;
A25: h4 =
hg2 * hg3
by A24, GROUP_2:43
.=
h2 (*) h3
by A24, ANPROJ_9:def 3, ANPROJ_9:def 4
.=
homography N
by ANPROJ_9:18
;
h4 in the carrier of SubGroupK-isometry
;
then
h4 in EnsK-isometry
by Def05;
then consider h being Element of EnsHomography3 such that
A26:
h4 = h
and
A27:
h is_K-isometry
;
take
N
; ( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )
thus
(homography N) .: absolute = absolute
by A25, A26, A27; ( (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )
set NP = (homography N) . P;
set NQ = (homography N) . Q;
set NP1 = (homography N) . P1;
set NP2 = (homography N) . P2;
set NP3 = (homography N) . P3;
set NP4 = (homography N) . P4;
set NP5 = (homography N) . P5;
A28:
P,P1,P2 are_collinear
by A1, A3, A4, ANPROJ_8:57, HESSENBE:2;
( Q,P,P1 are_collinear & Q,P,P2 are_collinear )
by A3, A4, COLLSP:4;
then A29:
Q,P1,P2 are_collinear
by A1, ANPROJ_8:57, HESSENBE:2;
thus
( (homography N) . P = Q & (homography N) . Q = P )
ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 )proof
A30:
(homography N) . P <> (homography N) . Q
A32:
(
(homography N) . P,
(homography N) . Q,
(homography N) . P1 are_collinear &
(homography N) . P,
(homography N) . Q,
(homography N) . P2 are_collinear &
(homography N) . P,
(homography N) . P5,
(homography N) . P3 are_collinear &
(homography N) . Q,
(homography N) . P5,
(homography N) . P4 are_collinear )
by A3, A4, A5, A6, ANPROJ_8:102;
then A33:
(homography N) . P,
(homography N) . P1,
(homography N) . P2 are_collinear
by ANPROJ_8:57, A30, HESSENBE:2;
A34:
P1,
P2,
Q are_collinear
by A29, ANPROJ_8:57, HESSENBE:1;
P5,
P4,
Q are_collinear
by A6, ANPROJ_8:57, HESSENBE:1;
then A35:
(
Q in Line (
P1,
P2) &
Q in Line (
P5,
P4) )
by A34, COLLSP:11;
then A36:
Q in (Line (P1,P2)) /\ (Line (P5,P4))
by XBOOLE_0:def 4;
P1,
P2,
(homography N) . P are_collinear
by A33, A20, A21, ANPROJ_8:57, HESSENBE:1;
then A37:
(homography N) . P in Line (
P1,
P2)
by COLLSP:11;
P5,
P4,
(homography N) . P are_collinear
by A32, A22, A23, ANPROJ_8:57, HESSENBE:1;
then
(homography N) . P in Line (
P5,
P4)
by COLLSP:11;
then
(homography N) . P in (Line (P5,P4)) /\ (Line (P1,P2))
by A37, XBOOLE_0:def 4;
then A39:
{Q,((homography N) . P)} c= (Line (P1,P2)) /\ (Line (P5,P4))
by A36, ZFMISC_1:32;
P4 <> P5
then
(
Line (
P1,
P2) is
LINE of
real_projective_plane &
Line (
P5,
P4) is
LINE of
real_projective_plane )
by A2, COLLSP:def 7;
then A41:
(
Line (
P1,
P2)
= Line (
P5,
P4) or
Line (
P1,
P2)
misses Line (
P5,
P4) or ex
p being
Element of
real_projective_plane st
(Line (P1,P2)) /\ (Line (P5,P4)) = {p} )
by COLLSP:21;
Line (
P1,
P2)
<> Line (
P5,
P4)
then consider p being
Element of
real_projective_plane such that A42:
(Line (P1,P2)) /\ (Line (P5,P4)) = {p}
by A35, A41, XBOOLE_0:def 4;
(
Q = p &
(homography N) . P = p )
by A42, A39, ZFMISC_1:20;
hence
(
(homography N) . P = Q &
(homography N) . Q = P )
by A28, A20, A21, A2, COLLSP:8, BKMODEL1:69;
verum
end;
thus
ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 )
by A2, A3, A4, A20, A21; verum