let N be invertible Matrix of 3,F_Real; 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; ( h = homography N implies ( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry ) )
assume A1:
h = homography N
; ( 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; homography (N ~) is Element of SubGroupK-isometry
hence
homography (N ~) is Element of SubGroupK-isometry
; verum