let g be Form of V,W; :: thesis: ( g = - f iff g = (- (1. INT.Ring)) * f )
thus ( g = - f implies g = (- (1. INT.Ring)) * f ) :: thesis: ( g = (- (1. INT.Ring)) * f implies g = - f )
proof
assume A1: g = - f ; :: thesis: g = (- (1. INT.Ring)) * f
now :: thesis: for v being Vector of V
for w being Vector of W holds g . (v,w) = ((- (1. INT.Ring)) * f) . (v,w)
let v be Vector of V; :: thesis: for w being Vector of W holds g . (v,w) = ((- (1. INT.Ring)) * f) . (v,w)
let w be Vector of W; :: thesis: g . (v,w) = ((- (1. INT.Ring)) * f) . (v,w)
thus g . (v,w) = - (f . (v,w)) by A1, BLDef4
.= (- (1. INT.Ring)) * (f . (v,w))
.= ((- (1. INT.Ring)) * f) . (v,w) by BLDef3 ; :: thesis: verum
end;
hence g = (- (1. INT.Ring)) * f ; :: thesis: verum
end;
assume A2: g = (- (1. INT.Ring)) * f ; :: thesis: g = - f
now :: thesis: for v being Vector of V
for w being Vector of W holds g . (v,w) = (- f) . (v,w)
let v be Vector of V; :: thesis: for w being Vector of W holds g . (v,w) = (- f) . (v,w)
let w be Vector of W; :: thesis: g . (v,w) = (- f) . (v,w)
thus g . (v,w) = (- (1. INT.Ring)) * (f . (v,w)) by A2, BLDef3
.= - (f . (v,w))
.= (- f) . (v,w) by BLDef4 ; :: thesis: verum
end;
hence g = - f ; :: thesis: verum