let V be RealLinearSpace; :: thesis: for u, v, w being Element of V
for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
let u, v, w be Element of V; :: thesis: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
let a, b, c be Real; :: thesis: ( ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 implies u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) )
assume that
A1: ((a * u) + (b * v)) + (c * w) = 0. V and
A2: a <> 0 ; :: thesis: u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
((a * u) + (b * v)) + (c * w) = (a * u) + ((b * v) + (c * w)) by RLVECT_1:def 3;
then a * u = - ((b * v) + (c * w)) by A1, RLVECT_1:6
.= (- (b * v)) + (- (c * w)) by RLVECT_1:31
.= (b * (- v)) + (- (c * w)) by RLVECT_1:25
.= (b * (- v)) + (c * (- w)) by RLVECT_1:25
.= ((- b) * v) + (c * (- w)) by RLVECT_1:24
.= ((- b) * v) + ((- c) * w) by RLVECT_1:24 ;
hence u = (a ") * (((- b) * v) + ((- c) * w)) by A2, ANALOAF:5
.= ((a ") * ((- b) * v)) + ((a ") * ((- c) * w)) by RLVECT_1:def 5
.= (((a ") * (- b)) * v) + ((a ") * ((- c) * w)) by RLVECT_1:def 7
.= ((- ((a ") * b)) * v) + (((a ") * (- c)) * w) by RLVECT_1:def 7
.= ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) ;
:: thesis: verum