let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F; :: thesis: for x being Element of F
for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let x be Element of F; :: thesis: for v, w being Element of V holds
( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
let v, w be Element of V; :: thesis: ( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )
A1: - (x * v) = (- (1. F)) * (x * v) by Th10
.= ((- (1. F)) * x) * v by Def15
.= (- ((1. F) * x)) * v by Th5 ;
hence - (x * v) = (- x) * v ; :: thesis: w - (x * v) = w + ((- x) * v)
thus w - (x * v) = w + ((- x) * v) by A1; :: thesis: verum