let R be comRing; for M1, M, N being LeftMod of R
for u being Homomorphism of R,M1,M holds
( tau (N,u) is additive & tau (N,u) is homogeneous )
let M1, M, N be LeftMod of R; for u being Homomorphism of R,M1,M holds
( tau (N,u) is additive & tau (N,u) is homogeneous )
let u be Homomorphism of R,M1,M; ( tau (N,u) is additive & tau (N,u) is homogeneous )
set F = tau (N,u);
A1:
for f, g being Element of (Hom (R,M,N)) holds (tau (N,u)) . (f + g) = ((tau (N,u)) . f) + ((tau (N,u)) . g)
proof
let f,
g be
Element of
(Hom (R,M,N));
(tau (N,u)) . (f + g) = ((tau (N,u)) . f) + ((tau (N,u)) . g)
reconsider h =
f + g as
Element of
(Hom (R,M,N)) ;
consider f1 being
Homomorphism of
R,
M,
N such that A2:
(
f = f1 &
(tau (N,u)) . f = f1 * u )
by Def23;
consider g1 being
Homomorphism of
R,
M,
N such that A3:
(
g = g1 &
(tau (N,u)) . g = g1 * u )
by Def23;
consider h1 being
Homomorphism of
R,
M,
N such that A4:
(
h1 = h &
(tau (N,u)) . h = h1 * u )
by Def23;
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
M1, the
carrier of
M)
by FUNCT_2:8;
reconsider f1u0 =
f1 * u,
g1u0 =
g1 * u as
Homomorphism of
R,
M1,
N by Th19;
(tau (N,u)) . (f + g) =
((ADD (M,N)) . (f0,g0)) * u0
by A2, A3, A4, Th21
.=
(ADD (M1,N)) . (
(f1 * u),
(g1 * u))
by Lm25
.=
(add_Hom (M1,N)) . (
f1u0,
g1u0)
by Th21
.=
((tau (N,u)) . f) + ((tau (N,u)) . g)
by A2, A3
;
hence
(tau (N,u)) . (f + g) = ((tau (N,u)) . f) + ((tau (N,u)) . g)
;
verum
end;
for f being Element of (Hom (R,M,N))
for a being Element of R holds (tau (N,u)) . (a * f) = a * ((tau (N,u)) . f)
proof
let f be
Element of
(Hom (R,M,N));
for a being Element of R holds (tau (N,u)) . (a * f) = a * ((tau (N,u)) . f)let a be
Element of
R;
(tau (N,u)) . (a * f) = a * ((tau (N,u)) . f)
consider f1 being
Homomorphism of
R,
M,
N such that A5:
(
f = f1 &
(tau (N,u)) . f = f1 * u )
by Def23;
reconsider af =
a * f as
Element of
(Hom (R,M,N)) ;
consider af1 being
Homomorphism of
R,
M,
N such that A6:
(
af = af1 &
(tau (N,u)) . af = af1 * u )
by Def23;
reconsider f0 =
f1,
af0 =
af1 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
M1, the
carrier of
M)
by FUNCT_2:8;
reconsider f1u0 =
f1 * u as
Homomorphism of
R,
M1,
N by Th19;
a * ((tau (N,u)) . f) =
(LMULT (M1,N)) . [a,f1u0]
by Th22, A5
.=
((LMULT (M,N)) . [a,f0]) * u0
by Lm27
.=
(tau (N,u)) . (a * f)
by A6, A5, Th22
;
hence
(tau (N,u)) . (a * f) = a * ((tau (N,u)) . f)
;
verum
end;
hence
( tau (N,u) is additive & tau (N,u) is homogeneous )
by A1; verum