let p1, q1, r1, p2, q2, r2 be Element of absolute ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum