let P be Point of real_projective_plane; :: thesis: for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N holds
( P is Element of absolute iff (homography N) . P is Element of absolute )
let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds
( P is Element of absolute iff (homography N) . P is Element of absolute )
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies ( P is Element of absolute iff (homography N) . P is Element of absolute ) )
assume A1: h = homography N ; :: thesis: ( P is Element of absolute iff (homography N) . P is Element of absolute )
h is Element of EnsK-isometry by BKMODEL2:def 8;
then A2: (homography N) .: absolute = absolute by A1, BKMODEL2:44;
homography (N ~) is Element of SubGroupK-isometry by A1, BKMODEL2:47;
then homography (N ~) is Element of EnsK-isometry by BKMODEL2:def 8;
then A3: (homography (N ~)) .: absolute = absolute by BKMODEL2:44;
set hP = (homography N) . P;
hereby :: thesis: ( (homography N) . P is Element of absolute implies P is Element of absolute )
assume A4: P is Element of absolute ; :: thesis: (homography N) . P is Element of absolute
dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence (homography N) . P is Element of absolute by A2, A4, FUNCT_1:108; :: thesis: verum
end;
assume A5: (homography N) . P is Element of absolute ; :: thesis: P is Element of absolute
A6: dom (homography (N ~)) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
(homography (N ~)) . ((homography N) . P) in (homography (N ~)) .: absolute by A6, A5, FUNCT_1:108;
hence P is Element of absolute by A3, ANPROJ_9:15; :: thesis: verum