let r be Real; :: thesis: for V being RealLinearSpace
for v, u, w being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
let V be RealLinearSpace; :: thesis: for v, u, w being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
let v, u, w be VECTOR of V; :: thesis: ( r <> 1 & (r * u) + ((1 - r) * w) = v implies w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) )
assume that
A1: r <> 1 and
A2: (r * u) + ((1 - r) * w) = v ; :: thesis: w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
A3: (1 - r) * w = v - (r * u) by A2, RLVECT_4:1;
A4: 1 - r <> 1 - 1 by A1;
then A5: (1 / (1 - r)) * (1 - r) = 1 by XCMPLX_1:106;
A6: (1 / (1 - r)) * (r * u) = ((1 / (1 - r)) * r) * u by RLVECT_1:def 7
.= ((1 - (1 - r)) / (1 - r)) * u by XCMPLX_1:99
.= ((1 / (1 - r)) - ((1 - r) / (1 - r))) * u by XCMPLX_1:120
.= ((1 / (1 - r)) - 1) * u by A4, XCMPLX_1:60 ;
thus w = 1 * w by RLVECT_1:def 8
.= (1 / (1 - r)) * ((1 - r) * w) by A5, RLVECT_1:def 7
.= ((1 / (1 - r)) * v) - ((1 / (1 - r)) * (r * u)) by A3, RLVECT_1:34
.= ((1 / (1 - r)) * v) + (- (((1 / (1 - r)) - 1) * u)) by A6, RLVECT_1:def 11
.= ((1 / (1 - r)) * v) + (((1 / (1 - r)) - 1) * (- u)) by RLVECT_1:25
.= ((1 / (1 - r)) * v) + ((- ((1 / (1 - r)) - 1)) * u) by RLVECT_1:24
.= ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) ; :: thesis: verum