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 * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
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 * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
let x be Scalar of R; :: thesis: for v being Vector of V holds
( v * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
let v be Vector of V; :: thesis: ( v * (0. R) = 0. V & v * (- (1_ R)) = - v & (0. V) * x = 0. V )
v + (v * (0. R)) = (v * (1_ R)) + (v * (0. R)) by Def8
.= v * ((1_ R) + (0. R)) by Def8
.= v * (1_ R) by RLVECT_1:4
.= v by Def8
.= v + (0. V) by RLVECT_1:4 ;
hence A1: v * (0. R) = 0. V by RLVECT_1:8; :: thesis: ( v * (- (1_ R)) = - v & (0. V) * x = 0. V )
(v * (- (1_ R))) + v = (v * (- (1_ R))) + (v * (1_ R)) by Def8
.= v * ((- (1_ R)) + (1_ R)) by Def8
.= 0. V by A1, RLVECT_1:5 ;
then (v * (- (1_ R))) + (v + (- v)) = (0. V) + (- v) by RLVECT_1:def 3;
then (0. V) + (- v) = (v * (- (1_ R))) + (0. V) by RLVECT_1:5
.= v * (- (1_ R)) by RLVECT_1:4 ;
hence v * (- (1_ R)) = - v by RLVECT_1:4; :: thesis: (0. V) * x = 0. V
(0. V) * x = v * ((0. R) * x) by A1, Def8
.= 0. V by A1 ;
hence (0. V) * x = 0. V ; :: thesis: verum