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