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