let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of F
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
let x be Element of F; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. 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 v being Element of V holds
( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
let v be Element of V; :: thesis: ( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )
v + ((0. F) * v) = ((1. F) * v) + ((0. F) * v) by Def16
.= ((1. F) + (0. F)) * v by Def14
.= (1. F) * v by RLVECT_1:4
.= v by Def16
.= v + (0. V) by RLVECT_1:4 ;
hence A1: (0. F) * v = 0. V by RLVECT_1:8; :: thesis: ( (- (1. F)) * v = - v & x * (0. V) = 0. V )
((- (1. F)) * v) + v = ((- (1. F)) * v) + ((1. F) * v) by Def16
.= ((1. F) + (- (1. F))) * v by Def14
.= 0. V by A1, RLVECT_1:def 10 ;
then ((- (1. F)) * v) + (v + (- v)) = (0. V) + (- v) by RLVECT_1:def 3;
then (0. V) + (- v) = ((- (1. F)) * v) + (0. V) by RLVECT_1:5
.= (- (1. F)) * v by RLVECT_1:4 ;
hence (- (1. F)) * v = - v by RLVECT_1:4; :: thesis: x * (0. V) = 0. V
x * (0. V) = (x * (0. F)) * v by A1, Def15
.= 0. V by A1 ;
hence x * (0. V) = 0. V ; :: thesis: verum