let V be RealLinearSpace; 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; ( 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
; 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; verum