let V be RealLinearSpace; :: thesis: for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
A - B = (affine-ratio (A,B,C)) * (A - C)
let A, B, C be Element of V; :: thesis: ( A <> C & A,B,C are_collinear implies A - B = (affine-ratio (A,B,C)) * (A - C) )
assume that
A1: A <> C and
A2: A,B,C are_collinear ; :: thesis: A - B = (affine-ratio (A,B,C)) * (A - C)
A - B = - (B - A) by RLVECT_1:33
.= - ((affine-ratio (A,B,C)) * (C - A)) by Def02, A1, A2
.= (- 1) * ((affine-ratio (A,B,C)) * (C - A)) by RLVECT_1:16
.= ((- 1) * (affine-ratio (A,B,C))) * (C - A) by RLVECT_1:def 7
.= (affine-ratio (A,B,C)) * ((- 1) * (C - A)) by RLVECT_1:def 7
.= (affine-ratio (A,B,C)) * (- (C - A)) by RLVECT_1:16
.= (affine-ratio (A,B,C)) * (A - C) by RLVECT_1:33 ;
hence A - B = (affine-ratio (A,B,C)) * (A - C) ; :: thesis: verum