let p1, q1, r1, p2, q2, r2 be Element of absolute ; ( p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct implies ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 ) )
assume that
A1:
p1,q1,r1 are_mutually_distinct
and
A2:
p2,q2,r2 are_mutually_distinct
; ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 )
consider t being Element of real_projective_plane such that
A3:
(tangent p1) /\ (tangent q1) = {t}
by A1, Th25;
t in (tangent p1) /\ (tangent q1)
by A3, TARSKI:def 1;
then consider N1 being invertible Matrix of 3,F_Real such that
A5:
( (homography N1) .: absolute = absolute & (homography N1) . Dir101 = p1 & (homography N1) . Dirm101 = q1 & (homography N1) . Dir011 = r1 & (homography N1) . Dir010 = t )
by A1, Th37;
consider u being Element of real_projective_plane such that
A6:
(tangent q2) /\ (tangent p2) = {u}
by A2, Th25;
u in (tangent p2) /\ (tangent q2)
by A6, TARSKI:def 1;
then consider N2 being invertible Matrix of 3,F_Real such that
A7:
( (homography N2) .: absolute = absolute & (homography N2) . Dir101 = p2 & (homography N2) . Dirm101 = q2 & (homography N2) . Dir011 = r2 & (homography N2) . Dir010 = u )
by A2, 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 A5, A7, ANPROJ_9:15
;
A21: (homography N) . q1 =
(homography N2) . ((homography (N1 ~)) . q1)
by ANPROJ_9:13
.=
q2
by A5, A7, ANPROJ_9:15
;
A22: (homography N) . r1 =
(homography N2) . ((homography (N1 ~)) . r1)
by ANPROJ_9:13
.=
r2
by A5, A7, 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 A5;
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 A7;
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
ex h being Element of EnsHomography3 st
( h4 = h & h is_K-isometry )
;
hence
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 )
by A20, A21, A22, A25; verum