let p, q, r, s be Element of absolute ; :: thesis: ( p,q,r are_mutually_distinct & q,p,s are_mutually_distinct implies ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) ) )
assume that
A1: p,q,r are_mutually_distinct and
A2: q,p,s are_mutually_distinct ; :: thesis: ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) )
consider t being Element of real_projective_plane such that
A3: (tangent p) /\ (tangent q) = {t} by A1, Th25;
A4: t in (tangent p) /\ (tangent q) 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 = p & (homography N1) . Dirm101 = q & (homography N1) . Dir011 = r & (homography N1) . Dir010 = t ) by A1, Th37;
consider N2 being invertible Matrix of 3,F_Real such that
A7: ( (homography N2) .: absolute = absolute & (homography N2) . Dir101 = q & (homography N2) . Dirm101 = p & (homography N2) . Dir011 = s & (homography N2) . Dir010 = t ) by A2, A4, Th37;
reconsider N = N2 * (N1 ~) as invertible Matrix of 3,F_Real ;
A20: (homography N) . p = (homography N2) . ((homography (N1 ~)) . p) by ANPROJ_9:13
.= q by A5, A7, ANPROJ_9:15 ;
A21: (homography N) . q = (homography N2) . ((homography (N1 ~)) . q) by ANPROJ_9:13
.= p by A5, A7, ANPROJ_9:15 ;
A22: (homography N) . r = (homography N2) . ((homography (N1 ~)) . r) by ANPROJ_9:13
.= s by A5, A7, ANPROJ_9:15 ;
A23: (homography N) . t = (homography N2) . ((homography (N1 ~)) . t) by ANPROJ_9:13
.= t 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 consider h being Element of EnsHomography3 such that
A26: h4 = h and
A27: h is_K-isometry ;
take N ; :: thesis: ( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) )
thus (homography N) .: absolute = absolute by A25, A26, A27; :: thesis: ( (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) )
thus ( (homography N) . p = q & (homography N) . q = p & (homography N) . r = s ) by A20, A21, A22; :: thesis: for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t
thus for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t :: thesis: verum

proof

let v be Element of real_projective_plane; :: thesis: ( v in (tangent p) /\ (tangent q) implies (homography N) . v = v )
assume v in (tangent p) /\ (tangent q) ; :: thesis: (homography N) . v = v
then v = t by A3, TARSKI:def 1;
hence (homography N) . v = v by A23; :: thesis: verum

end;