let R be non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr of R
for x being Scalar of R
for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr of R; :: thesis: for x being Scalar of R
for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
let x be Scalar of R; :: thesis: for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
let v, w be Vector of V; :: thesis: ( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )
A1: - (v * x) = (v * x) * (- (1_ R)) by Th90
.= v * (x * (- (1_ R))) by Def23
.= v * (- (x * (1_ R))) by VECTSP_1:8 ;
hence - (v * x) = v * (- x) by VECTSP_1:def 4; :: thesis: w - (v * x) = w + (v * (- x))
thus w - (v * x) = w + (v * (- x)) by A1, VECTSP_1:def 4; :: thesis: verum