let R be non empty right_complementable right_unital well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over 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 over 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 Th32
.= v * (x * (- (1_ R))) by Def8
.= v * (- (x * (1_ R))) by VECTSP_1:8 ;
hence - (v * x) = v * (- x) ; :: thesis: w - (v * x) = w + (v * (- x))
thus w - (v * x) = w + (v * (- x)) by A1; :: thesis: verum