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 (P,R,Q) = 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 (P,R,Q) = 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 (P,R,Q) = 1 / (affine-ratio (P,Q,R))
set r = affine-ratio (P,Q,R);
set s = affine-ratio (P,R,Q);
P,R,Q are_collinear by A1;
then R - P = (affine-ratio (P,R,Q)) * (Q - P) by A3, Def02
.= (affine-ratio (P,R,Q)) * ((affine-ratio (P,Q,R)) * (R - P)) by A1, A2, Def02
.= ((affine-ratio (P,R,Q)) * (affine-ratio (P,Q,R))) * (R - P) by RLVECT_1:def 7 ;
then 1 * (R - P) = ((affine-ratio (P,R,Q)) * (affine-ratio (P,Q,R))) * (R - P) by RLVECT_1:def 8;
hence affine-ratio (P,R,Q) = 1 / (affine-ratio (P,Q,R)) by A2, Th08, XCMPLX_1:73; :: thesis: verum