let V be RealLinearSpace; :: thesis: for P, Q, R being Element of V
for a being non zero Real st P,Q,R are_collinear & P <> R holds
affine-ratio (P,Q,R) = affine-ratio ((a * P),(a * Q),(a * R))
let P, Q, R be Element of V; :: thesis: for a being non zero Real st P,Q,R are_collinear & P <> R holds
affine-ratio (P,Q,R) = affine-ratio ((a * P),(a * Q),(a * R))
let a be non zero Real; :: thesis: ( P,Q,R are_collinear & P <> R implies affine-ratio (P,Q,R) = affine-ratio ((a * P),(a * Q),(a * R)) )
assume A1: ( P,Q,R are_collinear & P <> R ) ; :: thesis: affine-ratio (P,Q,R) = affine-ratio ((a * P),(a * Q),(a * R))
reconsider aP = a * P, aQ = a * Q, aR = a * R as Element of V ;
now :: thesis: ( aP <> aR & aP,aQ,aR are_collinear )
thus aP <> aR by A1, RLVECT_1:36; :: thesis: aP,aQ,aR are_collinear
Q in Line (P,R) by A1, RLTOPSP1:80;
then Q in { (((1 - l) * P) + (l * R)) where l is Real : verum } by RLTOPSP1:def 14;
then consider l being Real such that
A2: Q = ((1 - l) * P) + (l * R) ;
reconsider aL = Line (aP,aR) as line of V ;
H1: ( aP in aL & aR in aL ) by RLTOPSP1:72;
aQ = (a * ((1 - l) * P)) + (a * (l * R)) by A2, RLVECT_1:def 5
.= ((a * (1 - l)) * P) + (a * (l * R)) by RLVECT_1:def 7
.= ((a * (1 - l)) * P) + ((a * l) * R) by RLVECT_1:def 7
.= ((1 - l) * (a * P)) + ((a * l) * R) by RLVECT_1:def 7
.= ((1 - l) * aP) + (l * aR) by RLVECT_1:def 7 ;
then aQ in { (((1 - l) * aP) + (l * aR)) where l is Real : verum } ;
then aQ in aL by RLTOPSP1:def 14;
hence aP,aQ,aR are_collinear by H1; :: thesis: verum
end;
then aQ - aP = (affine-ratio (aP,aQ,aR)) * (aR - aP) by Def02;
then a * (Q - P) = (affine-ratio (aP,aQ,aR)) * (aR - aP) by RLVECT_1:34;
then a * (Q - P) = (affine-ratio (aP,aQ,aR)) * (a * (R - P)) by RLVECT_1:34;
then a * (Q - P) = ((affine-ratio (aP,aQ,aR)) * a) * (R - P) by RLVECT_1:def 7;
then a * (Q - P) = a * ((affine-ratio (aP,aQ,aR)) * (R - P)) by RLVECT_1:def 7;
then Q - P = (affine-ratio (aP,aQ,aR)) * (R - P) by RLVECT_1:36;
hence affine-ratio (P,Q,R) = affine-ratio ((a * P),(a * Q),(a * R)) by A1, Def02; :: thesis: verum