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

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

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

then
not (homography N) . P in BK_model \/ absolute
by A2, XBOOLE_0:def 3;
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 P is Element of absolute by A1, Th30;

hence contradiction by XBOOLE_0:3, BKMODEL2:1; :: thesis: verum

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