let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V st P,Q,R,S are_collinear & R <> Q & S <> Q & R <> S & cross-ratio (P,Q,R,S) = 1 holds
P = Q
let P, Q, R, S be Element of V; :: thesis: ( P,Q,R,S are_collinear & R <> Q & S <> Q & R <> S & cross-ratio (P,Q,R,S) = 1 implies P = Q )
assume that
A1: P,Q,R,S are_collinear and
A2: R <> Q and
A3: S <> Q and
A4: R <> S and
A5: cross-ratio (P,Q,R,S) = 1 ; :: thesis: P = Q
A6: affine-ratio (R,P,Q) = affine-ratio (S,P,Q) by A5, XCMPLX_1:58;
set r = affine-ratio (R,P,Q);
A7: ( R,P,Q are_collinear & S,P,Q are_collinear ) by A1;
then (P + (0. V)) - R = (affine-ratio (R,P,Q)) * ((Q + (0. V)) - R) by A2, Def02;
then (P + ((- S) + S)) - R = (affine-ratio (R,P,Q)) * ((Q + (0. V)) - R) by RLVECT_1:5
.= (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 ;
then ((P - S) + S) - R = (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
.= (P - S) + ((affine-ratio (R,P,Q)) * (S - R)) by A7, A6, A3, Def02 ;
then (- (P - S)) + ((P - S) + (S - R)) = (- (P - S)) + ((P - S) + ((affine-ratio (R,P,Q)) * (S - R))) by RLVECT_1:def 3;
then ((- (P - S)) + (P - S)) + (S - R) = (- (P - S)) + ((P - S) + ((affine-ratio (R,P,Q)) * (S - R))) by RLVECT_1:def 3
.= ((- (P - S)) + (P - S)) + ((affine-ratio (R,P,Q)) * (S - R)) by RLVECT_1:def 3 ;
then (affine-ratio (R,P,Q)) * (S - R) = S - R by RLVECT_1:8
.= 1 * (S - R) by RLVECT_1:def 8 ;
then affine-ratio (R,P,Q) = 1 by A4, Th08;
hence P = Q by A2, Th07, A7; :: thesis: verum