let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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) ( 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)) ; :: thesis: verum