let V be RealLinearSpace; 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; ( 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
; 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
;
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)
;
verum end; suppose A7:
P <> Q
;
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;
verum end; end;