let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q holds
cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R)
let P, Q, R, S be Element of V; :: thesis: ( P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R) )
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q ; :: thesis: cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R)
set r1 = affine-ratio (R,P,Q);
set r2 = affine-ratio (S,P,Q);
set s1 = affine-ratio (S,Q,P);
set s2 = affine-ratio (R,Q,P);
per cases ( P = Q or P <> Q ) ;
suppose A6: P = Q ; :: thesis: cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R)
( R,P,P are_collinear & S,P,P are_collinear ) by Th05;
then ( affine-ratio (R,P,Q) = 1 & affine-ratio (S,P,Q) = 1 & affine-ratio (S,Q,P) = 1 & affine-ratio (R,Q,P) = 1 ) by A2, A3, A6, Th07;
hence cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R) ; :: thesis: verum
end;
suppose A7: P <> Q ; :: thesis: cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R)
P,Q,R are_collinear by A1;
then consider r9 being non zero non unit Real such that
A8: ( r9 = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r9 & affine-ratio (Q,P,R) = op1 (op2 (op1 r9)) & affine-ratio (Q,R,P) = op2 (op1 r9) & affine-ratio (R,P,Q) = op1 (op2 r9) & affine-ratio (R,Q,P) = op2 r9 ) by A2, A4, A7, Th28;
( P,Q,S are_collinear & P <> S & Q <> S ) by A1, A3, A5;
then ex s9 being non zero non unit Real st
( s9 = affine-ratio (P,Q,S) & affine-ratio (P,S,Q) = op1 s9 & affine-ratio (Q,P,S) = op1 (op2 (op1 s9)) & affine-ratio (Q,S,P) = op2 (op1 s9) & affine-ratio (S,P,Q) = op1 (op2 s9) & affine-ratio (S,Q,P) = op2 s9 ) by A7, Th28;
hence cross-ratio (P,Q,R,S) = cross-ratio (Q,P,S,R) by A8; :: thesis: verum
end;
end;