let N be invertible Matrix of 3,F_Real; :: thesis: for h being Element of SubGroupK-isometry st h = homography N holds
( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry )
let h be Element of SubGroupK-isometry; :: thesis: ( h = homography N implies ( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry ) )
assume A1: h = homography N ; :: thesis: ( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry )
then h in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = h as Element of EnsHomography3 ;
homography (N ~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography (N ~) as Element of EnsHomography3 ;
set G = GroupHomography3 ;
reconsider h1g = h1, h2g = h2 as Element of GroupHomography3 by ANPROJ_9:def 4;
A2: N is_reverse_of N ~ by MATRIX_6:def 4;
A3: h1g * h2g = h1 (*) h2 by ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography (N * (N ~)) by A1, ANPROJ_9:18
.= 1_ GroupHomography3 by A2, MATRIX_6:def 2, Th34 ;
h2g * h1g = h2 (*) h1 by ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography ((N ~) * N) by A1, ANPROJ_9:18
.= 1_ GroupHomography3 by A2, MATRIX_6:def 2, Th34 ;
then h2g = h1g " by A3, GROUP_1:5;
hence h " = homography (N ~) by GROUP_2:48; :: thesis: homography (N ~) is Element of SubGroupK-isometry
hence homography (N ~) is Element of SubGroupK-isometry ; :: thesis: verum