let V be RealLinearSpace; :: thesis: for P, Q, R being Element of V st P,Q,R are_collinear & P <> R & Q <> R & P <> Q holds
affine-ratio (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1)
let P, Q, R be Element of V; :: thesis: ( P,Q,R are_collinear & P <> R & Q <> R & P <> Q implies affine-ratio (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) )
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: Q <> R and
A4: P <> Q ; :: thesis: affine-ratio (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1)
set r = affine-ratio (P,Q,R);
set s = affine-ratio (Q,P,R);
A5: Q - P = (affine-ratio (P,Q,R)) * (R - P) by A1, A2, Def02;
Q,P,R are_collinear by A1;
then P - Q = (affine-ratio (Q,P,R)) * (R - Q) by A3, Def02;
then (affine-ratio (P,Q,R)) * (R - P) = - ((affine-ratio (Q,P,R)) * ((R + (0. V)) - Q)) by A5, RLVECT_1:33
.= - ((affine-ratio (Q,P,R)) * ((R + ((- P) + P)) - Q)) by RLVECT_1:5
.= - ((affine-ratio (Q,P,R)) * (((R - P) + P) - Q)) by RLVECT_1:def 3
.= - ((affine-ratio (Q,P,R)) * ((R - P) + (P - Q))) by RLVECT_1:def 3
.= (- 1) * ((affine-ratio (Q,P,R)) * ((R - P) + (P - Q))) by RLVECT_1:16
.= ((- 1) * (affine-ratio (Q,P,R))) * ((R - P) + (P - Q)) by RLVECT_1:def 7
.= ((- (affine-ratio (Q,P,R))) * (R - P)) + ((- (affine-ratio (Q,P,R))) * (P - Q)) by RLVECT_1:def 5 ;
then A6: ((affine-ratio (P,Q,R)) * (R - P)) + ((affine-ratio (Q,P,R)) * (R - P)) = ((- (affine-ratio (Q,P,R))) * (R - P)) + (((- (affine-ratio (Q,P,R))) * (P - Q)) + ((affine-ratio (Q,P,R)) * (R - P))) by RLVECT_1:def 3
.= ((- (affine-ratio (Q,P,R))) * (R - P)) + (((affine-ratio (Q,P,R)) * (R - P)) + ((- (affine-ratio (Q,P,R))) * (P - Q))) by RLVECT_1:def 2
.= (((- (affine-ratio (Q,P,R))) * (R - P)) + ((affine-ratio (Q,P,R)) * (R - P))) + ((- (affine-ratio (Q,P,R))) * (P - Q)) by RLVECT_1:def 3
.= (((- (affine-ratio (Q,P,R))) + (affine-ratio (Q,P,R))) * (R - P)) + ((- (affine-ratio (Q,P,R))) * (P - Q)) by RLVECT_1:def 6
.= (0. V) + ((- (affine-ratio (Q,P,R))) * (P - Q)) by RLVECT_1:10
.= (- (affine-ratio (Q,P,R))) * (P - Q) ;
Q,P,R are_collinear by A1;
then A7: affine-ratio (Q,P,R) <> 0 by A3, A4, Th06;
then reconsider s9 = 1 / (affine-ratio (Q,P,R)) as non zero Real ;
A8: s9 * (affine-ratio (Q,P,R)) = 1 by A7, XCMPLX_1:106;
A9: (affine-ratio (P,Q,R)) - 1 <> 0 by A1, A2, A3, Th07;
((affine-ratio (P,Q,R)) + (affine-ratio (Q,P,R))) * (R - P) = (- (affine-ratio (Q,P,R))) * (P - Q) by A6, RLVECT_1:def 6
.= (affine-ratio (Q,P,R)) * (- (P - Q)) by RLVECT_1:24
.= (affine-ratio (Q,P,R)) * (Q - P) by RLVECT_1:33 ;
then (s9 * ((affine-ratio (P,Q,R)) + (affine-ratio (Q,P,R)))) * (R - P) = s9 * ((affine-ratio (Q,P,R)) * (Q - P)) by RLVECT_1:def 7
.= (s9 * (affine-ratio (Q,P,R))) * (Q - P) by RLVECT_1:def 7
.= 1 * (Q - P) by A7, XCMPLX_1:106
.= Q - P by RLVECT_1:def 8 ;
then (affine-ratio (Q,P,R)) * (affine-ratio (P,Q,R)) = (affine-ratio (Q,P,R)) * ((1 / (affine-ratio (Q,P,R))) * ((affine-ratio (P,Q,R)) + (affine-ratio (Q,P,R)))) by A1, Def02, A2;
then (affine-ratio (P,Q,R)) * (affine-ratio (Q,P,R)) = ((affine-ratio (Q,P,R)) * (1 / (affine-ratio (Q,P,R)))) * ((affine-ratio (P,Q,R)) + (affine-ratio (Q,P,R))) ;
then (affine-ratio (P,Q,R)) * (affine-ratio (Q,P,R)) = (affine-ratio (P,Q,R)) + (affine-ratio (Q,P,R)) by A8;
then ((affine-ratio (Q,P,R)) * ((affine-ratio (P,Q,R)) - 1)) / ((affine-ratio (P,Q,R)) - 1) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) ;
then (affine-ratio (Q,P,R)) * (((affine-ratio (P,Q,R)) - 1) / ((affine-ratio (P,Q,R)) - 1)) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) ;
then (affine-ratio (Q,P,R)) * 1 = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) by A9, XCMPLX_1:60;
hence affine-ratio (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1) ; :: thesis: verum