let N be invertible Matrix of 3,F_Real; for P, Q, R being Point of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear holds
(homography N) . ((homography N) . R) = R
let P, Q, R be Point of (ProjectiveSpace (TOP-REAL 3)); ( P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear implies (homography N) . ((homography N) . R) = R )
assume that
A1:
P <> Q
and
A2:
(homography N) . P = Q
and
A3:
(homography N) . Q = P
and
A4:
P,Q,R are_collinear
; (homography N) . ((homography N) . R) = R
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
consider u1, v1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A5:
( P = Dir u1 & not u1 is zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 & not v1 is zero & (homography N) . P = Dir v1 )
by ANPROJ_8:def 4;
consider u2, v2 being Element of (TOP-REAL 3), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that
A6:
( Q = Dir u2 & not u2 is zero & u2 = u2f & p2 = N * u2f & v2 = M2F p2 & not v2 is zero & (homography N) . Q = Dir v2 )
by ANPROJ_8:def 4;
reconsider u1fr = u1f, u2fr = u2f as FinSequence of REAL ;
( u1 in TOP-REAL 3 & u2 in TOP-REAL 3 )
;
then A7:
( u1 in REAL 3 & u2 in REAL 3 )
by EUCLID:22;
then A8:
( len u1 = 3 & len u2 = 3 )
by EUCLID_8:50;
consider u3 being Element of (TOP-REAL 3) such that
A9:
not u3 is zero
and
A10:
R = Dir u3
by ANPROJ_1:26;
reconsider uf3r = u3 as FinSequence of REAL by EUCLID:24;
A11:
( are_Prop v2,u1 & are_Prop v1,u2 )
by A2, A3, A5, A6, ANPROJ_1:22;
then consider l1 being Real such that
A12:
l1 <> 0
and
A13:
v2 = l1 * u1
by ANPROJ_1:1;
consider l2 being Real such that
A14:
l2 <> 0
and
A15:
v1 = l2 * u2
by A11, ANPROJ_1:1;
A16:
( width NR = 3 & len NR = 3 & len u2fr = 3 & len u1fr = 3 )
by A7, EUCLID_8:50, A5, A6, MATRIX_0:24;
A17:
( width NR = len u2fr & len u2fr > 0 & width NR = len u1fr & len u1fr > 0 )
by A8, A5, A6, MATRIX_0:24;
reconsider l = l1 * l2 as non zero Real by A12, A14;
A18: (NR * NR) * u1fr =
NR * (NR * u1fr)
by A16, MATRIXR2:59
.=
NR * (l2 * u2fr)
by A5, A6, A8, MATRIXR1:def 2, Th30, A15
.=
l2 * (NR * u2fr)
by A17, MATRIXR2:53
.=
l2 * (l1 * u1fr)
by A5, A6, A8, MATRIXR1:def 2, Th30, A13
.=
l * u1fr
by RVSUM_1:49
;
A19: (NR * NR) * u2fr =
NR * (NR * u2fr)
by A16, MATRIXR2:59
.=
NR * (l1 * u1fr)
by A5, A6, A8, MATRIXR1:def 2, Th30, A13
.=
l1 * (NR * u1fr)
by A17, MATRIXR2:53
.=
l1 * (l2 * u2fr)
by A5, A6, A8, MATRIXR1:def 2, Th30, A15
.=
l * u2fr
by RVSUM_1:49
;
|{u1,u2,u3}| = 0
by A4, A5, A6, A9, A10, Th01;
then consider a, b, c being Real such that
A20:
( ((a * u1) + (b * u2)) + (c * u3) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
by ANPROJ_8:42;
A21:
c <> 0
proof
assume A22:
c = 0
;
contradiction
reconsider bu2 =
b * u2 as
Element of
REAL 3
by EUCLID:22;
reconsider n = 3 as
Nat ;
u3 in TOP-REAL 3
;
then
u3 in REAL 3
by EUCLID:22;
then bu2 + (0 * u3) =
bu2 + (0* n)
by EUCLID_4:3
.=
bu2
by EUCLID_4:1
;
then
(a * u1) + (b * u2) = 0. (TOP-REAL 3)
by A20, A22, RVSUM_1:15;
then
are_Prop u1,
u2
by A20, A22, A5, A6, Th57;
hence
contradiction
by A1, A5, A6, ANPROJ_1:22;
verum
end;
A23:
((a * u1) + (b * u2)) + (c * u3) = ((c * u3) + (a * u1)) + (b * u2)
by RVSUM_1:15;
reconsider d = (- a) / c, e = (- b) / c as Real ;
A24:
u3 = (d * u1) + (e * u2)
by A23, A20, A21, ANPROJ_8:12;
reconsider u4fr = (d * u1) + (e * u2) as FinSequence of REAL ;
reconsider NRNR = NR * NR as Matrix of 3,REAL ;
u3 in TOP-REAL 3
;
then
u3 in REAL 3
by EUCLID:22;
then A25:
( len u4fr = width NR & width NR = len NR & len u4fr > 0 & len NR > 0 )
by A16, A24, EUCLID_8:50;
A26:
( len u1fr = 3 & len u2fr = 3 & width NR = 3 & len NR = 3 )
by A5, A6, A7, EUCLID_8:50, MATRIX_0:24;
( len (d * u1fr) = 3 & len (e * u2fr) = 3 )
by RVSUM_1:117, A5, A6, A8;
then A27:
( len (d * u1fr) = len (e * u2fr) & width NR = len (d * u1fr) & len (d * u1fr) > 0 & len NR > 0 )
by MATRIX_0:24;
( len (NR * u1fr) = 3 & len (NR * u2fr) = 3 )
by A26, MATRIXR1:61;
then A28:
( len (d * (NR * u1fr)) = 3 & len (e * (NR * u2fr)) = 3 & width NR = 3 & len NR = 3 )
by MATRIX_0:24, RVSUM_1:117;
A29:
( width NR = len (NR * u1fr) & len (NR * u1fr) > 0 )
by A26, MATRIXR1:61;
A30:
( width NR = len (NR * u2fr) & len (NR * u2fr) > 0 )
by A26, MATRIXR1:61;
A31: (NR * NR) * uf3r =
(NR * NR) * u4fr
by A23, A20, A21, ANPROJ_8:12
.=
NR * (NR * ((d * u1fr) + (e * u2fr)))
by A5, A6, A25, MATRIXR2:59
.=
NR * ((NR * (d * u1fr)) + (NR * (e * u2fr)))
by MATRIXR1:57, A27
.=
NR * ((d * (NR * u1fr)) + (NR * (e * u2fr)))
by MATRIXR1:59, A26
.=
NR * ((d * (NR * u1fr)) + (e * (NR * u2fr)))
by MATRIXR1:59, A26
.=
(NR * (d * (NR * u1fr))) + (NR * (e * (NR * u2fr)))
by MATRIXR1:57, A28
.=
(d * (NR * (NR * u1fr))) + (NR * (e * (NR * u2fr)))
by MATRIXR1:59, A29
.=
(d * (NR * (NR * u1fr))) + (e * (NR * (NR * u2fr)))
by MATRIXR1:59, A30
.=
(d * ((NR * NR) * u1fr)) + (e * (NR * (NR * u2fr)))
by A16, MATRIXR2:59
.=
(d * (l * u1fr)) + (e * ((NR * NR) * u2fr))
by A18, A16, MATRIXR2:59
.=
((d * l) * u1fr) + (e * (l * u2fr))
by A19, RVSUM_1:49
.=
((d * l) * u1fr) + ((e * l) * u2fr)
by RVSUM_1:49
.=
(l * (d * u1fr)) + ((l * e) * u2fr)
by RVSUM_1:49
.=
(l * (d * u1fr)) + (l * (e * u2fr))
by RVSUM_1:49
.=
l * ((d * u1) + (e * u2))
by A5, A6, RVSUM_1:51
.=
l * uf3r
by A23, A20, A21, ANPROJ_8:12
;
N = NR
by MATRIXR1:def 2;
then
(homography (N * N)) . R = R
by A31, A9, A10, Th33, ANPROJ_8:17;
hence
(homography N) . ((homography N) . R) = R
by ANPROJ_9:13; verum