set G = GroupHomography3 ;
homography (1. (F_Real,3)) in GroupHomography3
by ANPROJ_9:def 1, ANPROJ_9:def 4;
then reconsider e = homography (1. (F_Real,3)) as Element of GroupHomography3 ;
now for h being Element of GroupHomography3 holds
( h * e = h & e * h = h )let h be
Element of
GroupHomography3;
( h * e = h & e * h = h )
h in EnsHomography3
by ANPROJ_9:def 4;
then consider N being
invertible Matrix of 3,
F_Real such that A1:
h = homography N
by ANPROJ_9:def 1;
(
h in EnsHomography3 &
e in EnsHomography3 )
by A1, ANPROJ_9:def 1;
then reconsider h1 =
h,
h2 =
e as
Element of
EnsHomography3 ;
thus h * e =
h1 (*) h2
by ANPROJ_9:def 3, ANPROJ_9:def 4
.=
homography (N * (1. (F_Real,3)))
by A1, ANPROJ_9:18
.=
h
by A1, MATRIX_3:19
;
e * h = hthus e * h =
h2 (*) h1
by ANPROJ_9:def 3, ANPROJ_9:def 4
.=
homography ((1. (F_Real,3)) * N)
by A1, ANPROJ_9:18
.=
h
by A1, MATRIX_3:18
;
verum end;
hence
homography (1. (F_Real,3)) = 1_ GroupHomography3
by GROUP_1:4; homography (1. (F_Real,3)) = 1_ SubGroupK-isometry
hence
homography (1. (F_Real,3)) = 1_ SubGroupK-isometry
by GROUP_2:44; verum