let V be RealLinearSpace; :: thesis: for v1, v2, x, y being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
let v1, v2, x, y be VECTOR of V; :: thesis: for b1, b2, c1, c2 being Real st v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
let b1, b2, c1, c2 be Real; :: thesis: ( v1 = (b1 * x) + (b2 * y) & v2 = (c1 * x) + (c2 * y) implies ( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) ) )
assume that
A1: v1 = (b1 * x) + (b2 * y) and
A2: v2 = (c1 * x) + (c2 * y) ; :: thesis: ( v1 + v2 = ((b1 + c1) * x) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y) )
thus v1 + v2 = (((b1 * x) + (b2 * y)) + (c1 * x)) + (c2 * y) by A1, A2, RLVECT_1:def 3
.= (((b1 * x) + (c1 * x)) + (b2 * y)) + (c2 * y) by RLVECT_1:def 3
.= (((b1 + c1) * x) + (b2 * y)) + (c2 * y) by RLVECT_1:def 6
.= ((b1 + c1) * x) + ((b2 * y) + (c2 * y)) by RLVECT_1:def 3
.= ((b1 + c1) * x) + ((b2 + c2) * y) by RLVECT_1:def 6 ; :: thesis: v1 - v2 = ((b1 - c1) * x) + ((b2 - c2) * y)
thus v1 - v2 = ((b1 * x) + (b2 * y)) + ((- (c1 * x)) + (- (c2 * y))) by A1, A2, RLVECT_1:31
.= ((b1 * x) + (b2 * y)) + ((c1 * (- x)) + (- (c2 * y))) by RLVECT_1:25
.= ((b1 * x) + (b2 * y)) + ((c1 * (- x)) + (c2 * (- y))) by RLVECT_1:25
.= ((b1 * x) + (b2 * y)) + (((- c1) * x) + (c2 * (- y))) by RLVECT_1:24
.= ((b1 * x) + (b2 * y)) + (((- c1) * x) + ((- c2) * y)) by RLVECT_1:24
.= (((b1 * x) + (b2 * y)) + ((- c1) * x)) + ((- c2) * y) by RLVECT_1:def 3
.= (((b1 * x) + ((- c1) * x)) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def 3
.= (((b1 + (- c1)) * x) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def 6
.= ((b1 + (- c1)) * x) + ((b2 * y) + ((- c2) * y)) by RLVECT_1:def 3
.= ((b1 - c1) * x) + ((b2 + (- c2)) * y) by RLVECT_1:def 6
.= ((b1 - c1) * x) + ((b2 - c2) * y) ; :: thesis: verum