let V be RealLinearSpace; for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S))
let P, Q, R, S be Element of V; ( P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S)) )
assume that
A1:
P,Q,R,S are_collinear
and
A2:
P,Q,R,S are_mutually_distinct
; cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S))
A3:
( P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q )
by A2, ZFMISC_1:def 6;
set r1 = affine-ratio (R,P,Q);
set r2 = affine-ratio (S,P,Q);
set s1 = affine-ratio (Q,P,R);
set s2 = affine-ratio (S,P,R);
set r = affine-ratio (P,Q,R);
A4:
P,Q,R are_collinear
by A1;
then A5:
( affine-ratio (R,P,Q) = 1 / (1 - (affine-ratio (P,Q,R))) & affine-ratio (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) )
by A3, Th10, Th13;
P,Q,R are_collinear
by A1;
then A6:
(affine-ratio (P,Q,R)) - 1 <> 0
by A3, Th07;
A7:
1 - (affine-ratio (Q,P,R)) = affine-ratio (R,P,Q)
proof
1
- (affine-ratio (Q,P,R)) =
1
- ((affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1))
by A4, A3, Th10
.=
(((affine-ratio (P,Q,R)) - 1) / ((affine-ratio (P,Q,R)) - 1)) - ((affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1))
by A6, XCMPLX_1:60
.=
(- 1) / ((affine-ratio (P,Q,R)) - 1)
.=
1
/ (- ((affine-ratio (P,Q,R)) - 1))
by XCMPLX_1:192
;
hence
1
- (affine-ratio (Q,P,R)) = affine-ratio (
R,
P,
Q)
by A5;
verum
end;
( R <> Q & R,P,Q are_collinear )
by A1, A2, ZFMISC_1:def 6;
then A8:
(affine-ratio (S,P,Q)) * (P - R) = (affine-ratio (S,P,Q)) * ((affine-ratio (R,P,Q)) * (Q - R))
by Def02;
A9:
( S <> Q & S,P,Q are_collinear )
by A1, A2, ZFMISC_1:def 6;
A10:
( S <> R & S,P,R are_collinear )
by A1, A2, ZFMISC_1:def 6;
then A11:
P - S = (affine-ratio (S,P,R)) * (R - S)
by Def02;
S,P,Q are_collinear
by A1;
then A12:
affine-ratio (S,P,Q) <> 0
by A3, Th06;
S,P,R are_collinear
by A1;
then A13:
affine-ratio (S,P,R) <> 0
by A3, Th06;
P - R =
(P + (0. V)) - R
.=
(P + ((- S) + S)) - R
by RLVECT_1:5
.=
((P - S) + S) - R
by RLVECT_1:def 3
.=
(P - S) + (S - R)
by RLVECT_1:def 3
.=
((affine-ratio (S,P,R)) * (R - S)) + (S - R)
by A10, Def02
.=
((affine-ratio (S,P,R)) * (R - S)) + (- (R - S))
by RLVECT_1:33
.=
((affine-ratio (S,P,R)) * (R - S)) + ((- 1) * (R - S))
by RLVECT_1:16
.=
((affine-ratio (S,P,R)) - 1) * (R - S)
by RLVECT_1:def 6
;
then A14:
(affine-ratio (S,P,Q)) * (P - R) = ((affine-ratio (S,P,Q)) * ((affine-ratio (S,P,R)) - 1)) * (R - S)
by RLVECT_1:def 7;
(affine-ratio (R,P,Q)) * (Q - R) =
(affine-ratio (R,P,Q)) * ((Q + (0. V)) - R)
.=
(affine-ratio (R,P,Q)) * ((Q + ((- S) + S)) - R)
by RLVECT_1:5
.=
(affine-ratio (R,P,Q)) * (((Q - S) + S) - R)
by RLVECT_1:def 3
.=
(affine-ratio (R,P,Q)) * ((Q - S) + (S - R))
by RLVECT_1:def 3
.=
((affine-ratio (R,P,Q)) * (Q - S)) + ((affine-ratio (R,P,Q)) * (S - R))
by RLVECT_1:def 5
.=
((affine-ratio (R,P,Q)) * (Q - S)) + ((affine-ratio (R,P,Q)) * (- (R - S)))
by RLVECT_1:33
.=
((affine-ratio (R,P,Q)) * (Q - S)) + ((affine-ratio (R,P,Q)) * ((- 1) * (R - S)))
by RLVECT_1:16
.=
((affine-ratio (R,P,Q)) * (Q - S)) + (((affine-ratio (R,P,Q)) * (- 1)) * (R - S))
by RLVECT_1:def 7
.=
((affine-ratio (R,P,Q)) * (Q - S)) + ((- (affine-ratio (R,P,Q))) * (R - S))
;
then (affine-ratio (S,P,Q)) * ((affine-ratio (R,P,Q)) * (Q - R)) =
((affine-ratio (S,P,Q)) * ((affine-ratio (R,P,Q)) * (Q - S))) + ((affine-ratio (S,P,Q)) * ((- (affine-ratio (R,P,Q))) * (R - S)))
by RLVECT_1:def 5
.=
(((affine-ratio (S,P,Q)) * (affine-ratio (R,P,Q))) * (Q - S)) + ((affine-ratio (S,P,Q)) * ((- (affine-ratio (R,P,Q))) * (R - S)))
by RLVECT_1:def 7
.=
((affine-ratio (R,P,Q)) * ((affine-ratio (S,P,Q)) * (Q - S))) + ((affine-ratio (S,P,Q)) * ((- (affine-ratio (R,P,Q))) * (R - S)))
by RLVECT_1:def 7
.=
((affine-ratio (R,P,Q)) * ((affine-ratio (S,P,R)) * (R - S))) + ((affine-ratio (S,P,Q)) * ((- (affine-ratio (R,P,Q))) * (R - S)))
by A9, Def02, A11
.=
(((affine-ratio (R,P,Q)) * (affine-ratio (S,P,R))) * (R - S)) + ((affine-ratio (S,P,Q)) * ((- (affine-ratio (R,P,Q))) * (R - S)))
by RLVECT_1:def 7
.=
(((affine-ratio (R,P,Q)) * (affine-ratio (S,P,R))) * (R - S)) + (((affine-ratio (S,P,Q)) * (- (affine-ratio (R,P,Q)))) * (R - S))
by RLVECT_1:def 7
.=
(((affine-ratio (R,P,Q)) * (affine-ratio (S,P,R))) + ((affine-ratio (S,P,Q)) * (- (affine-ratio (R,P,Q))))) * (R - S)
by RLVECT_1:def 6
;
then
(affine-ratio (S,P,Q)) * ((affine-ratio (S,P,R)) - 1) = ((affine-ratio (R,P,Q)) * (affine-ratio (S,P,R))) + ((affine-ratio (S,P,Q)) * (- (affine-ratio (R,P,Q))))
by A14, A8, A3, Th08;
then
((affine-ratio (R,P,Q)) * (affine-ratio (S,P,Q))) - (affine-ratio (S,P,Q)) = ((affine-ratio (R,P,Q)) * (affine-ratio (S,P,R))) - ((affine-ratio (S,P,Q)) * (affine-ratio (S,P,R)))
;
then
(- (affine-ratio (Q,P,R))) * (affine-ratio (S,P,Q)) = ((affine-ratio (R,P,Q)) - (affine-ratio (S,P,Q))) * (affine-ratio (S,P,R))
by A7;
then
(affine-ratio (Q,P,R)) * (affine-ratio (S,P,Q)) = ((affine-ratio (S,P,Q)) - (affine-ratio (R,P,Q))) * (affine-ratio (S,P,R))
;
then (affine-ratio (Q,P,R)) / (affine-ratio (S,P,R)) =
((affine-ratio (S,P,Q)) - (affine-ratio (R,P,Q))) / (affine-ratio (S,P,Q))
by A12, A13, XCMPLX_1:94
.=
((affine-ratio (S,P,Q)) / (affine-ratio (S,P,Q))) - ((affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q)))
.=
1 - ((affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q)))
by A12, XCMPLX_1:60
;
hence
cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S))
; verum