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 being Vector of V holds (- v) * x = - (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 being Vector of V holds (- v) * x = - (v * x)
let x be Scalar of R; :: thesis: for v being Vector of V holds (- v) * x = - (v * x)
let v be Vector of V; :: thesis: (- v) * x = - (v * x)
(- v) * x = (v * (- (1_ R))) * x by Th32
.= v * ((- (1_ R)) * x) by Def8
.= v * (- ((1_ R) * x)) by VECTSP_1:9
.= v * (- x) ;
hence (- v) * x = - (v * x) by Th33; :: thesis: verum