let R be Ring; :: thesis: for M being AbGroup
for s being Function of R,(End_Ring M) st s is RingHomomorphism holds
AbGrLMod (M,s) is LeftMod of R
let M be AbGroup; :: thesis: for s being Function of R,(End_Ring M) st s is RingHomomorphism holds
AbGrLMod (M,s) is LeftMod of R
let s be Function of R,(End_Ring M); :: thesis: ( s is RingHomomorphism implies AbGrLMod (M,s) is LeftMod of R )
assume A1: s is RingHomomorphism ; :: thesis: AbGrLMod (M,s) is LeftMod of R
A2: AbGrLMod (M,s) is Abelian

proof

for x, y being Element of (AbGrLMod (M,s)) holds x + y = y + x

proof

let x, y be Element of (AbGrLMod (M,s)); :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of M ;
x + y = x1 + y1
.= y1 + x1
.= y + x ;
hence x + y = y + x ; :: thesis: verum

end;

hence AbGrLMod (M,s) is Abelian ; :: thesis: verum

end;

A3: AbGrLMod (M,s) is add-associative

proof

for x, y, z being Element of (AbGrLMod (M,s)) holds (x + y) + z = x + (y + z)

proof

let x, y, z be Element of (AbGrLMod (M,s)); :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of M ;
reconsider xy = x + y as Element of (AbGrLMod (M,s)) ;
reconsider xy1 = xy, yz1 = y + z as Element of M ;
reconsider yh = y1 + y1 as Element of M ;
(x + y) + z = (x1 + y1) + z1
.= x1 + (y1 + z1) by ALGSTR_1:7
.= x + (y + z) ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum

end;

hence AbGrLMod (M,s) is add-associative ; :: thesis: verum

end;

A4: AbGrLMod (M,s) is right_zeroed

proof

for x being Element of (AbGrLMod (M,s)) holds x + (0. (AbGrLMod (M,s))) = x

proof

let x be Element of (AbGrLMod (M,s)); :: thesis: x + (0. (AbGrLMod (M,s))) = x
reconsider x1 = x as Element of M ;
x + (0. (AbGrLMod (M,s))) = x1 + (0. M)
.= x by ALGSTR_1:7 ;
hence x + (0. (AbGrLMod (M,s))) = x ; :: thesis: verum

end;

hence AbGrLMod (M,s) is right_zeroed ; :: thesis: verum

end;

A5: AbGrLMod (M,s) is right_complementable

proof

for x being Element of (AbGrLMod (M,s)) holds x is right_complementable

proof

let x be Element of (AbGrLMod (M,s)); :: thesis: x is right_complementable
reconsider x1 = x as Element of M ;
consider y1 being Element of M such that
A6: x1 + y1 = 0. M by ALGSTR_1:7;
reconsider y = y1 as Element of (AbGrLMod (M,s)) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (AbGrLMod (M,s))
thus x + y = 0. (AbGrLMod (M,s)) by A6; :: thesis: verum

end;

hence AbGrLMod (M,s) is right_complementable ; :: thesis: verum

end;

AbGrLMod (M,s) is scalar-unital

proof

for x being Element of (AbGrLMod (M,s)) holds (1. R) * x = x

proof

let x be Element of (AbGrLMod (M,s)); :: thesis: (1. R) * x = x
reconsider x1 = x as Element of M ;
consider h being additive Function of the carrier of M, the carrier of M such that
A7: ( h = s . (1. R) & (1. R) * x = h . x ) by Def12;
s is unity-preserving by A1;
hence (1. R) * x = x by A7; :: thesis: verum

end;

hence AbGrLMod (M,s) is scalar-unital ; :: thesis: verum

end;

then ( AbGrLMod (M,s) is Abelian & AbGrLMod (M,s) is add-associative & AbGrLMod (M,s) is right_zeroed & AbGrLMod (M,s) is right_complementable & AbGrLMod (M,s) is vector-distributive & AbGrLMod (M,s) is scalar-distributive & AbGrLMod (M,s) is scalar-associative & AbGrLMod (M,s) is scalar-unital ) by A2, A3, A4, A5, A1, Lm12, Lm13, Lm14;
hence AbGrLMod (M,s) is LeftMod of R ; :: thesis: verum