let R be comRing; for M, N, N1 being LeftMod of R
for u being Homomorphism of R,N,N1 holds
( phi (M,u) is additive & phi (M,u) is homogeneous )
let M, N, N1 be LeftMod of R; for u being Homomorphism of R,N,N1 holds
( phi (M,u) is additive & phi (M,u) is homogeneous )
let u be Homomorphism of R,N,N1; ( phi (M,u) is additive & phi (M,u) is homogeneous )
set F = phi (M,u);
A1:
( u is additive & u is homogeneous )
by Def10;
A2:
for f, g being Element of (Hom (R,M,N)) holds (phi (M,u)) . (f + g) = ((phi (M,u)) . f) + ((phi (M,u)) . g)
proof
let f,
g be
Element of
(Hom (R,M,N));
(phi (M,u)) . (f + g) = ((phi (M,u)) . f) + ((phi (M,u)) . g)
reconsider h =
f + g as
Element of
(Hom (R,M,N)) ;
consider f1 being
Homomorphism of
R,
M,
N such that A3:
(
f = f1 &
(phi (M,u)) . f = u * f1 )
by Def24;
consider g1 being
Homomorphism of
R,
M,
N such that A4:
(
g = g1 &
(phi (M,u)) . g = u * g1 )
by Def24;
consider h1 being
Homomorphism of
R,
M,
N such that A5:
(
h1 = h &
(phi (M,u)) . h = u * h1 )
by Def24;
A6:
h1 = (ADD (M,N)) . (
f1,
g1)
by A3, A4, A5, Th21;
reconsider f0 =
f1,
g0 =
g1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
N)
by FUNCT_2:8;
reconsider u0 =
u as
Element of
Funcs ( the
carrier of
N, the
carrier of
N1)
by FUNCT_2:8;
reconsider uf10 =
u * f1,
ug10 =
u * g1 as
Homomorphism of
R,
M,
N1 by Th19;
(phi (M,u)) . (f + g) =
(ADD (M,N1)) . (
(u0 * f0),
(u * g0))
by Lm26, A1, A6, A5
.=
(add_Hom (M,N1)) . (
uf10,
ug10)
by Th21
.=
((phi (M,u)) . f) + ((phi (M,u)) . g)
by A3, A4
;
hence
(phi (M,u)) . (f + g) = ((phi (M,u)) . f) + ((phi (M,u)) . g)
;
verum
end;
for f being Element of (Hom (R,M,N))
for a being Element of R holds (phi (M,u)) . (a * f) = a * ((phi (M,u)) . f)
proof
let f be
Element of
(Hom (R,M,N));
for a being Element of R holds (phi (M,u)) . (a * f) = a * ((phi (M,u)) . f)let a be
Element of
R;
(phi (M,u)) . (a * f) = a * ((phi (M,u)) . f)
consider f1 being
Homomorphism of
R,
M,
N such that A7:
(
f = f1 &
(phi (M,u)) . f = u * f1 )
by Def24;
reconsider af =
a * f as
Element of
(Hom (R,M,N)) ;
consider af1 being
Homomorphism of
R,
M,
N such that A8:
(
af = af1 &
(phi (M,u)) . af = u * af1 )
by Def24;
reconsider f0 =
f1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
N)
by FUNCT_2:8;
reconsider u0 =
u as
Element of
Funcs ( the
carrier of
N, the
carrier of
N1)
by FUNCT_2:8;
reconsider uf10 =
u * f1 as
Homomorphism of
R,
M,
N1 by Th19;
a * ((phi (M,u)) . f) =
(LMULT (M,N1)) . [a,uf10]
by A7, Th22
.=
u0 * ((LMULT (M,N)) . [a,f0])
by Lm28, A1
.=
(phi (M,u)) . (a * f)
by A8, A7, Th22
;
hence
(phi (M,u)) . (a * f) = a * ((phi (M,u)) . f)
;
verum
end;
hence
( phi (M,u) is additive & phi (M,u) is homogeneous )
by A2; verum