let P be Element of BK_model ; :: thesis: for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N holds
(homography N) . P is Element of BK_model
let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds
(homography N) . P is Element of BK_model
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies (homography N) . P is Element of BK_model )
assume A1: h = homography N ; :: thesis: (homography N) . P is Element of BK_model
set hP = (homography N) . P;
assume A2: (homography N) . P is not Element of BK_model ; :: thesis: contradiction
(homography N) . P is not Element of absolute
proof
assume (homography N) . P is Element of absolute ; :: thesis: contradiction
then P is Element of absolute by A1, Th30;
hence contradiction by XBOOLE_0:3, BKMODEL2:1; :: thesis: verum
end;
then not (homography N) . P in BK_model \/ absolute by A2, XBOOLE_0:def 3;
then consider l being LINE of (IncProjSp_of real_projective_plane) such that
A3: (homography N) . P in l and
A4: l misses absolute by Th29;
reconsider L = (line_homography (N ~)) . l as LINE of real_projective_plane by INCPROJ:4;
reconsider L9 = L as LINE of (IncProjSp_of real_projective_plane) ;
consider P1, P2 being Element of absolute such that
P1 <> P2 and
A5: P1 in L9 and
P2 in L9 by A3, Th19, Th12;
A6: (homography N) . P1 is Element of absolute by A1, Th30;
(homography N) . P1 in (line_homography N) . L by A5, Th20;
then (homography N) . P1 in l by Th15;
hence contradiction by A6, A4, XBOOLE_0:def 4; :: thesis: verum