let a, b, c be Real; :: thesis: for V being non trivial RealLinearSpace
for u, v, w being Element of V st a <> 0 & ((a * u) + (b * v)) + (c * w) = 0. V holds
u = (((- b) / a) * v) + (((- c) / a) * w)
let V be non trivial RealLinearSpace; :: thesis: for u, v, w being Element of V st a <> 0 & ((a * u) + (b * v)) + (c * w) = 0. V holds
u = (((- b) / a) * v) + (((- c) / a) * w)
let u, v, w be Element of V; :: thesis: ( a <> 0 & ((a * u) + (b * v)) + (c * w) = 0. V implies u = (((- b) / a) * v) + (((- c) / a) * w) )
assume that
A1: a <> 0 and
A2: ((a * u) + (b * v)) + (c * w) = 0. V ; :: thesis: u = (((- b) / a) * v) + (((- c) / a) * w)
(a * u) + ((b * v) + (c * w)) = 0. V by RLVECT_1:def 3, A2;
then A3: - ((b * v) + (c * w)) = a * u by RLVECT_1:6;
a * u = 1 * (- ((b * v) + (c * w))) by A3, RLVECT_1:def 8
.= (a * (1 / a)) * (- ((b * v) + (c * w))) by A1, XCMPLX_1:106
.= a * ((1 / a) * (- ((b * v) + (c * w)))) by RLVECT_1:def 7 ;
then u = (1 / a) * (- ((b * v) + (c * w))) by A1, RLVECT_1:36
.= (1 / a) * ((- 1) * ((b * v) + (c * w))) by RLVECT_1:16
.= (1 / a) * (((- 1) * (b * v)) + ((- 1) * (c * w))) by RLVECT_1:def 5
.= ((1 / a) * ((- 1) * (b * v))) + ((1 / a) * ((- 1) * (c * w))) by RLVECT_1:def 5
.= (((1 / a) * (- 1)) * (b * v)) + ((1 / a) * ((- 1) * (c * w))) by RLVECT_1:def 7
.= (((- (1 / a)) * b) * v) + ((1 / a) * ((- 1) * (c * w))) by RLVECT_1:def 7
.= ((((- 1) / a) * b) * v) + ((1 / a) * ((- 1) * (c * w))) by XCMPLX_1:187
.= ((((- 1) * b) / a) * v) + ((1 / a) * ((- 1) * (c * w))) by XCMPLX_1:74
.= (((- b) / a) * v) + (((1 / a) * (- 1)) * (c * w)) by RLVECT_1:def 7
.= (((- b) / a) * v) + (((- (1 / a)) * c) * w) by RLVECT_1:def 7
.= (((- b) / a) * v) + ((((- 1) / a) * c) * w) by XCMPLX_1:187
.= (((- b) / a) * v) + ((((- 1) * c) / a) * w) by XCMPLX_1:74
.= (((- b) / a) * v) + (((- c) / a) * w) ;
hence u = (((- b) / a) * v) + (((- c) / a) * w) ; :: thesis: verum