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