set H = EnsK-isometry ;
set G = GroupHomography3 ;
reconsider N = 1. (F_Real,3) as invertible Matrix of 3,F_Real ;
homography N in { (homography M) where M is invertible Matrix of 3,F_Real : verum } ;
then reconsider idG = homography (1. (F_Real,3)) as Element of GroupHomography3 by ANPROJ_9:def 1, ANPROJ_9:def 4;
A1: 1_ GroupHomography3 = idG

proof

for g being Element of GroupHomography3 holds
( idG * g = g & g * idG = g )

proof

let g be Element of GroupHomography3; :: thesis:
g in EnsHomography3 by ANPROJ_9:def 4;
then consider N being invertible Matrix of 3,F_Real such that
A2: g = homography N by ANPROJ_9:def 1;
( idG in EnsHomography3 & homography N in EnsHomography3 ) by ANPROJ_9:def 1;
then reconsider g1 = idG, g2 = homography N as Element of EnsHomography3 ;
thus idG * g = g :: thesis:

proof

idG * g = g1 (*) g2 by A2, ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography ((1. (F_Real,3)) * N) by ANPROJ_9:18
.= g by A2, MATRIX_3:18 ;
hence idG * g = g ; :: thesis:

end;

thus g * idG = g :: thesis:

proof

g * idG = g2 (*) g1 by A2, ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography (N * (1. (F_Real,3))) by ANPROJ_9:18
.= g by A2, MATRIX_3:19 ;
hence g * idG = g ; :: thesis:

end;

end;

hence 1_ GroupHomography3 = idG by GROUP_1:def 4; :: thesis:

end;

A3: for g1, g2 being Element of GroupHomography3 st g1 in EnsK-isometry & g2 in EnsK-isometry holds
g1 * g2 in EnsK-isometry

proof

let g1, g2 be Element of GroupHomography3; :: thesis:
assume that
A4: g1 in EnsK-isometry and
A5: g2 in EnsK-isometry ; :: thesis:
consider h1 being Element of EnsHomography3 such that
A5BIS: ( g1 = h1 & h1 is_K-isometry ) by A4;
consider h2 being Element of EnsHomography3 such that
A6: ( g2 = h2 & h2 is_K-isometry ) by A5;
reconsider g3 = g1 * g2 as Element of EnsHomography3 by ANPROJ_9:def 4;
consider N1, N2 being invertible Matrix of 3,F_Real such that
A7: h1 = homography N1 and
A8: h2 = homography N2 and
A9: h1 (*) h2 = homography (N1 * N2) by ANPROJ_9:def 2;
A10: ( dom (homography N1) = the carrier of (ProjectiveSpace (TOP-REAL 3)) & dom (homography N2) = the carrier of (ProjectiveSpace (TOP-REAL 3)) & dom (homography (N1 * N2)) = the carrier of (ProjectiveSpace (TOP-REAL 3)) ) by FUNCT_2:def 1;
A11: (homography (N1 * N2)) .: absolute c= absolute

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (homography (N1 * N2)) .: absolute ; :: thesis:
then consider y being object such that
A12: y in dom (homography (N1 * N2)) and
A13: y in absolute and
A14: (homography (N1 * N2)) . y = x by FUNCT_1:def 6;
reconsider y = y as Point of (ProjectiveSpace (TOP-REAL 3)) by A12;
dom (homography N2) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
then A15: (homography N2) . y in absolute by A13, A6, A8, FUNCT_1:108;
dom (homography N1) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
then (homography N1) . ((homography N2) . y) in (homography N1) .: absolute by A15, FUNCT_1:108;
hence x in absolute by A5BIS, A7, A14, ANPROJ_9:13; :: thesis:

end;

absolute c= (homography (N1 * N2)) .: absolute

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: x in absolute ; :: thesis:
then reconsider y = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider z being object such that
A17: z in dom (homography N1) and
A18: z in absolute and
A19: y = (homography N1) . z by A16, A5BIS, A7, FUNCT_1:def 6;
reconsider z = z as Point of (ProjectiveSpace (TOP-REAL 3)) by A17;
consider t being object such that
A20: t in dom (homography N2) and
A21: t in absolute and
A22: z = (homography N2) . t by A18, A6, A8, FUNCT_1:def 6;
reconsider t = t as Point of (ProjectiveSpace (TOP-REAL 3)) by A20;
y = (homography (N1 * N2)) . t by A22, A19, ANPROJ_9:13;
hence x in (homography (N1 * N2)) .: absolute by A10, A21, FUNCT_1:def 6; :: thesis:

end;

then (homography (N1 * N2)) .: absolute = absolute by A11;
then g3 is_K-isometry by A9, A5BIS, A6, ANPROJ_9:def 3, ANPROJ_9:def 4;
hence g1 * g2 in EnsK-isometry ; :: thesis:

end;

for g being Element of GroupHomography3 st g in EnsK-isometry holds
g " in EnsK-isometry

proof

let g be Element of GroupHomography3; :: thesis:
assume g in EnsK-isometry ; :: thesis:
then consider h being Element of EnsHomography3 such that
A23: ( g = h & h is_K-isometry ) ;
h in { (homography N) where N is invertible Matrix of 3,F_Real : verum } by ANPROJ_9:def 1;
then consider N being invertible Matrix of 3,F_Real such that
A24: h = homography N ;
reconsider h3 = g " as Element of EnsHomography3 by ANPROJ_9:def 4;
h3 in { (homography N) where N is invertible Matrix of 3,F_Real : verum } by ANPROJ_9:def 1;
then consider N3 being invertible Matrix of 3,F_Real such that
A25: h3 = homography N3 ;
A26: h (*) h3 = g * (g ") by A23, ANPROJ_9:def 3, ANPROJ_9:def 4
.= 1_ GroupHomography3 by GROUP_1:def 5 ;
A27: h3 (*) h = (g ") * g by A23, ANPROJ_9:def 3, ANPROJ_9:def 4
.= 1_ GroupHomography3 by GROUP_1:def 5 ;
A28: homography (N * N3) = homography (1. (F_Real,3)) by A26, A1, A25, A24, ANPROJ_9:18;
A29: homography (N3 * N) = homography (1. (F_Real,3)) by A27, A1, A25, A24, ANPROJ_9:18;
A30: for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography (N3 ~)) . P = (homography N) . P

proof

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
(homography N3) . ((homography N) . P) = (homography (N3 * N)) . P by ANPROJ_9:13
.= P by A29, ANPROJ_9:14 ;
hence (homography (N3 ~)) . P = (homography N) . P by ANPROJ_9:15; :: thesis:

end;

A31: for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography N3) . P = (homography (N ~)) . P

proof

let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
(homography N) . ((homography N3) . P) = (homography (N * N3)) . P by ANPROJ_9:13
.= P by A28, ANPROJ_9:14 ;
hence (homography N3) . P = (homography (N ~)) . P by ANPROJ_9:15; :: thesis:

end;

A32: ( dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) & dom (homography N3) = the carrier of (ProjectiveSpace (TOP-REAL 3)) ) by FUNCT_2:def 1;
(homography N3) .: absolute = absolute

proof

A33: (homography N3) .: absolute c= absolute

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (homography N3) .: absolute ; :: thesis:
then consider y being object such that
A34: y in dom (homography N3) and
A35: y in absolute and
A36: (homography N3) . y = x by FUNCT_1:def 6;
reconsider y = y as Point of (ProjectiveSpace (TOP-REAL 3)) by A34;
A37: y = (homography (N3 ~)) . x by A36, ANPROJ_9:15;
(homography N3) . y is Point of (ProjectiveSpace (TOP-REAL 3)) ;
then reconsider z = x as Point of (ProjectiveSpace (TOP-REAL 3)) by A36;
(homography N) . z in absolute by A37, A30, A35;
then consider t being object such that
A38: t in dom (homography N) and
A39: t in absolute and
A40: (homography N) . t = (homography N) . z by A23, A24, FUNCT_1:def 6;
reconsider t = t as Point of (ProjectiveSpace (TOP-REAL 3)) by A38;
t = (homography (N ~)) . ((homography N) . t) by ANPROJ_9:15
.= z by A40, ANPROJ_9:15 ;
hence x in absolute by A39; :: thesis:

end;

absolute c= (homography N3) .: absolute

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A41: x in absolute ; :: thesis:
then reconsider y = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider z being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A42: z in absolute and
A43: (homography N) . y = z by A32, FUNCT_1:108, A41, A23, A24;
reconsider z = z as Point of (ProjectiveSpace (TOP-REAL 3)) ;
y = (homography (N ~)) . ((homography N) . y) by ANPROJ_9:15
.= (homography N3) . z by A43, A31 ;
hence x in (homography N3) .: absolute by A42, A32, FUNCT_1:def 6; :: thesis:

end;

hence (homography N3) .: absolute = absolute by A33; :: thesis:

end;

then h3 is_K-isometry by A25;
hence g " in EnsK-isometry ; :: thesis:

end;

hence ex b₁ being strict Subgroup of GroupHomography3 st the carrier of b₁ = EnsK-isometry by ANPROJ_9:def 4, A3, GROUP_2:52; :: thesis: