let P, Q be Element of BK_model ; ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P )
per cases
( P = Q or P <> Q )
;
suppose
P <> Q
;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P )then consider N being
invertible Matrix of 3,
F_Real such that A2:
(homography N) .: absolute = absolute
and A3:
(homography N) . P = Q
and A4:
(homography N) . Q = P
and
ex
P1,
P2 being
Element of
absolute st
(
P1 <> P2 &
P,
Q,
P1 are_collinear &
P,
Q,
P2 are_collinear &
(homography N) . P1 = P2 &
(homography N) . P2 = P1 )
by Th45;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum }
;
then reconsider h =
homography N as
Element of
EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry
by A2;
then
h in EnsK-isometry
;
then reconsider h =
h as
Element of
SubGroupK-isometry by Def05;
take
h
;
ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P )thus
ex
N being
invertible Matrix of 3,
F_Real st
(
h = homography N &
(homography N) . P = Q &
(homography N) . Q = P )
by A3, A4;
verum end; end;