let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P <> S & R <> Q & S <> Q holds
cross-ratio (P,Q,R,S) = cross-ratio (R,S,P,Q)
let P, Q, R, S be Element of V; :: thesis: ( P,Q,R,S are_collinear & P <> S & R <> Q & S <> Q implies cross-ratio (P,Q,R,S) = cross-ratio (R,S,P,Q) )
assume that
A1: P,Q,R,S are_collinear and
A2: P <> S and
A3: R <> Q and
A4: S <> Q ; :: thesis: cross-ratio (P,Q,R,S) = cross-ratio (R,S,P,Q)
A5: ( R,P,Q are_collinear & P,R,S are_collinear & S,P,Q are_collinear & Q,R,S are_collinear ) by A1;
set r1 = affine-ratio (R,P,Q);
set r2 = affine-ratio (S,P,Q);
set s1 = affine-ratio (P,R,S);
set s2 = affine-ratio (Q,R,S);
A6: ( affine-ratio (S,P,Q) <> 0 & affine-ratio (Q,R,S) <> 0 ) by A2, A3, A4, A5, Th06;
A7: Q - S <> 0. V by A4, RLVECT_1:21;
A8: P - R = (affine-ratio (R,P,Q)) * (Q - R) by A5, A3, Def02;
A9: P - S = (affine-ratio (S,P,Q)) * (Q - S) by A5, A4, Def02;
R - Q = (affine-ratio (Q,R,S)) * (S - Q) by A5, A4, Def02;
then A10: Q - R = (affine-ratio (Q,R,S)) * (Q - S) by Lm02;
R - P = (affine-ratio (P,R,S)) * (S - P) by A5, A2, Def02;
then P - R = (affine-ratio (P,R,S)) * (P - S) by Lm02
.= ((affine-ratio (P,R,S)) * (affine-ratio (S,P,Q))) * (Q - S) by A9, RLVECT_1:def 7 ;
then ((affine-ratio (R,P,Q)) * (affine-ratio (Q,R,S))) * (Q - S) = ((affine-ratio (P,R,S)) * (affine-ratio (S,P,Q))) * (Q - S) by A8, A10, RLVECT_1:def 7;
hence cross-ratio (P,Q,R,S) = cross-ratio (R,S,P,Q) by A7, RLVECT_1:37, A6, XCMPLX_1:94; :: thesis: verum