let h be Element of EnsHomography3 ; :: thesis: ( h = homography (1. (F_Real,3)) implies h is_K-isometry )
assume A1: h = homography (1. (F_Real,3)) ; :: thesis: h is_K-isometry
reconsider N = 1. (F_Real,3) as invertible Matrix of 3,F_Real ;
h is_K-isometry
proof
A2: (homography N) .: absolute c= absolute
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (homography N) .: absolute or x in absolute )
assume x in (homography N) .: absolute ; :: thesis: x in absolute
then ex y being object st
( y in dom (homography N) & y in absolute & (homography N) . y = x ) by FUNCT_1:def 6;
hence x in absolute by ANPROJ_9:14; :: thesis: verum
end;
absolute c= (homography N) .: absolute
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in absolute or x in (homography N) .: absolute )
assume A3: x in absolute ; :: thesis: x in (homography N) .: absolute
then reconsider y = x as Point of (ProjectiveSpace (TOP-REAL 3)) ;
A4: y = (homography N) . y by ANPROJ_9:14;
dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence x in (homography N) .: absolute by A4, A3, FUNCT_1:108; :: thesis: verum
end;
then absolute = (homography N) .: absolute by A2;
hence h is_K-isometry by A1; :: thesis: verum
end;
hence h is_K-isometry ; :: thesis: verum