let R be comRing; for M being LeftMod of R holds LModlmult ((AbGr M),(canHom M)) = the lmult of M
let M be LeftMod of R; LModlmult ((AbGr M),(canHom M)) = the lmult of M
set F = LModlmult ((AbGr M),(canHom M));
for z being object st z in [: the carrier of R, the carrier of M:] holds
(LModlmult ((AbGr M),(canHom M))) . z = the lmult of M . z
proof
let z be
object ;
( z in [: the carrier of R, the carrier of M:] implies (LModlmult ((AbGr M),(canHom M))) . z = the lmult of M . z )
assume A1:
z in [: the carrier of R, the carrier of M:]
;
(LModlmult ((AbGr M),(canHom M))) . z = the lmult of M . z
consider x,
y being
object such that A2:
(
x in the
carrier of
R &
y in the
carrier of
M &
z = [x,y] )
by A1, ZFMISC_1:def 2;
reconsider y0 =
y as
Element of
M by A2;
reconsider y1 =
y as
Element of
(AbGr M) by A2;
reconsider x0 =
x as
Element of
R by A2;
consider h being
Endomorphism of
(AbGr M) such that A3:
(
h = (canHom M) . x0 &
(LModlmult ((AbGr M),(canHom M))) . (
x0,
y0)
= h . y0 )
by Def12;
consider f being
Endomorphism of
R,
M such that A4:
(
f = (curry the lmult of M) . x0 &
(canHom M) . x0 = AbGr f )
by Def27;
reconsider y2 =
y1 as
Element of the
carrier of
M ;
A5:
(AbGr f) . y1 = f . y2
by Def26;
(LModlmult ((AbGr M),(canHom M))) . (
x0,
y0)
= the
lmult of
M . (
x0,
y0)
by A4, A5, A3, LOPBAN_8:7;
hence
(LModlmult ((AbGr M),(canHom M))) . z = the
lmult of
M . z
by A2;
verum
end;
hence
LModlmult ((AbGr M),(canHom M)) = the lmult of M
; verum