let V be RealLinearSpace; :: thesis: for A, B, P, Q being Element of V
for a, b being Real st A = ((1 - a) * P) + (a * Q) & B = ((1 - b) * P) + (b * Q) holds
A - B = (b - a) * (P - Q)
let A, B, P, Q be Element of V; :: thesis: for a, b being Real st A = ((1 - a) * P) + (a * Q) & B = ((1 - b) * P) + (b * Q) holds
A - B = (b - a) * (P - Q)
let a, b be Real; :: thesis: ( A = ((1 - a) * P) + (a * Q) & B = ((1 - b) * P) + (b * Q) implies A - B = (b - a) * (P - Q) )
assume that
A1: A = ((1 - a) * P) + (a * Q) and
A2: B = ((1 - b) * P) + (b * Q) ; :: thesis: A - B = (b - a) * (P - Q)
A - B = ((1 - a) * P) + ((a * Q) - (((1 - b) * P) + (b * Q))) by A1, A2, RLVECT_1:def 3
.= ((1 - a) * P) + (((a * Q) - (b * Q)) - ((1 - b) * P)) by RLVECT_1:27
.= ((1 - a) * P) + (((a - b) * Q) - ((1 - b) * P)) by RLVECT_1:35
.= (((1 - a) * P) + ((a - b) * Q)) + (- ((1 - b) * P)) by RLVECT_1:def 3
.= (((1 - a) * P) + ((a - b) * Q)) + ((- 1) * ((1 - b) * P)) by RLVECT_1:16
.= (((1 - a) * P) + ((a - b) * Q)) + (((- 1) * (1 - b)) * P) by RLVECT_1:def 7
.= ((1 - a) * P) + (((a - b) * Q) + ((b - 1) * P)) by RLVECT_1:def 3
.= ((1 - a) * P) + (((b - 1) * P) + ((a - b) * Q)) by RLVECT_1:def 2
.= (((1 - a) * P) + ((b - 1) * P)) + ((a - b) * Q) by RLVECT_1:def 3
.= (((1 - a) + (b - 1)) * P) + ((a - b) * Q) by RLVECT_1:def 6
.= ((b - a) * P) + (((- 1) * (b - a)) * Q)
.= ((b - a) * P) + ((- 1) * ((b - a) * Q)) by RLVECT_1:def 7
.= ((b - a) * P) - (((- 1) * (a - b)) * Q) by RLVECT_1:16 ;
hence A - B = (b - a) * (P - Q) by RLVECT_1:34; :: thesis: verum