let a, b, c be Real; :: thesis: for u, v, w being Element of (TOP-REAL 3) st a <> 0 & (a + b) + c = 0 & ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) holds
u in Line (v,w)
let u, v, w be Element of (TOP-REAL 3); :: thesis: ( a <> 0 & (a + b) + c = 0 & ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) implies u in Line (v,w) )
assume that
A1: a <> 0 and
A2: (a + b) + c = 0 and
A3: ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) ; :: thesis: u in Line (v,w)
A4: u = (((- b) / a) * v) + (((- c) / a) * w) by A1, A3, ANPROJ_8:12;
reconsider r = (- c) / a as Real ;
1 - r = (a / a) + (c / a) by A1, XCMPLX_1:60
.= (a + c) / a
.= (- b) / a by A2 ;
then u in { (((1 - r) * v) + (r * w)) where r is Real : verum } by A4;
hence u in Line (v,w) by RLTOPSP1:def 14; :: thesis: verum