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