let M be AbGroup; End_Ring M is distributive
A1:
for f, g, v being Element of (End_Ring M) holds v * (f + g) = (v * f) + (v * g)
proof
let f,
g,
v be
Element of
(End_Ring M);
v * (f + g) = (v * f) + (v * g)
f in set_End M
;
then consider f1 being
Function of the
carrier of
M, the
carrier of
M such that A2:
(
f1 = f &
f1 is
Endomorphism of
M )
;
g in set_End M
;
then consider g1 being
Function of the
carrier of
M, the
carrier of
M such that A3:
(
g1 = g &
g1 is
Endomorphism of
M )
;
v in set_End M
;
then consider v1 being
Function of the
carrier of
M, the
carrier of
M such that A4:
(
v1 = v &
v1 is
Endomorphism of
M )
;
reconsider fg1 =
(ADD (M,M)) . (
f1,
g1) as
Endomorphism of
M by A2, A3, Th3;
A5:
f + g = (ADD (M,M)) . (
f1,
g1)
by A2, A3, Th3;
v * f in set_End M
;
then consider vf1 being
Function of the
carrier of
M, the
carrier of
M such that A6:
(
vf1 = v * f &
vf1 is
Endomorphism of
M )
;
v * g in set_End M
;
then consider vg1 being
Function of the
carrier of
M, the
carrier of
M such that A7:
(
vg1 = v * g &
vg1 is
Endomorphism of
M )
;
A8:
vf1 = (FuncComp M) . (
v1,
f1)
by A2, A4, A6, Th6;
A9:
vg1 = (FuncComp M) . (
v1,
g1)
by A3, A4, A7, Th6;
reconsider f1 =
f1,
g1 =
g1,
v1 =
v1,
vf1 =
vf1,
vg1 =
vg1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
A10:
for
x being
Element of
M holds
((FuncComp M) . (v1,fg1)) . x = ((ADD (M,M)) . (vf1,vg1)) . x
proof
let x be
Element of the
carrier of
M;
((FuncComp M) . (v1,fg1)) . x = ((ADD (M,M)) . (vf1,vg1)) . x
A11:
((ADD (M,M)) . (f1,g1)) . x = (f1 . x) + (g1 . x)
by Th1;
A12:
(
(v1 * f1) . x = v1 . (f1 . x) &
(v1 * g1) . x = v1 . (g1 . x) )
by FUNCT_2:15;
A13:
(
((FuncComp M) . (v1,f1)) . x = (v1 * f1) . x &
((FuncComp M) . (v1,g1)) . x = (v1 * g1) . x )
by Def4;
fg1 in Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
then ((FuncComp M) . (v1,fg1)) . x =
(v1 * fg1) . x
by Def4
.=
v1 . ((f1 . x) + (g1 . x))
by A11, FUNCT_2:15
.=
(vf1 . x) + (vg1 . x)
by A8, A9, A13, A12, A4, VECTSP_1:def 20
.=
((ADD (M,M)) . (vf1,vg1)) . x
by Th1
;
hence
((FuncComp M) . (v1,fg1)) . x = ((ADD (M,M)) . (vf1,vg1)) . x
;
verum
end;
reconsider F =
(FuncComp M) . (
v1,
fg1) as
Function of the
carrier of
M, the
carrier of
M by A4, Th6;
reconsider G =
(ADD (M,M)) . (
vf1,
vg1) as
Function of the
carrier of
M, the
carrier of
M ;
v * (f + g) =
F
by A4, A5, Th6
.=
G
by A10
.=
(v * f) + (v * g)
by A6, A7, Th3
;
hence
v * (f + g) = (v * f) + (v * g)
;
verum
end;
for f, g, v being Element of (End_Ring M) holds (f + g) * v = (f * v) + (g * v)
proof
let f,
g,
v be
Element of
(End_Ring M);
(f + g) * v = (f * v) + (g * v)
f in set_End M
;
then consider f1 being
Function of the
carrier of
M, the
carrier of
M such that A14:
(
f1 = f &
f1 is
Endomorphism of
M )
;
g in set_End M
;
then consider g1 being
Function of the
carrier of
M, the
carrier of
M such that A15:
(
g1 = g &
g1 is
Endomorphism of
M )
;
v in set_End M
;
then consider v1 being
Function of the
carrier of
M, the
carrier of
M such that A16:
(
v1 = v &
v1 is
Endomorphism of
M )
;
A17:
f + g = (ADD (M,M)) . (
f1,
g1)
by A14, A15, Th3;
reconsider fg1 =
(ADD (M,M)) . (
f1,
g1) as
Endomorphism of
M by A14, A15, Th3;
f * v in set_End M
;
then consider fv1 being
Function of the
carrier of
M, the
carrier of
M such that A18:
(
fv1 = f * v &
fv1 is
Endomorphism of
M )
;
g * v in set_End M
;
then consider gv1 being
Function of the
carrier of
M, the
carrier of
M such that A19:
(
gv1 = g * v &
gv1 is
Endomorphism of
M )
;
reconsider f1 =
f1,
g1 =
g1,
v1 =
v1,
fv1 =
fv1,
gv1 =
gv1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
A20:
fv1 = (FuncComp M) . (
f1,
v1)
by A14, A16, A18, Th6;
A21:
gv1 = (FuncComp M) . (
g1,
v1)
by A15, A16, A19, Th6;
A22:
for
x being
Element of
M holds
((FuncComp M) . (fg1,v1)) . x = ((ADD (M,M)) . (fv1,gv1)) . x
proof
let x be
Element of
M;
((FuncComp M) . (fg1,v1)) . x = ((ADD (M,M)) . (fv1,gv1)) . x
A23:
(
(f1 * v1) . x = f1 . (v1 . x) &
(g1 * v1) . x = g1 . (v1 . x) )
by FUNCT_2:15;
A24:
(
((FuncComp M) . (f1,v1)) . x = (f1 * v1) . x &
((FuncComp M) . (g1,v1)) . x = (g1 * v1) . x )
by Def4;
fg1 in Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
then ((FuncComp M) . (fg1,v1)) . x =
(fg1 * v1) . x
by Def4
.=
((ADD (M,M)) . (f1,g1)) . (v1 . x)
by FUNCT_2:15
.=
(fv1 . x) + (gv1 . x)
by A20, A21, A24, A23, Th1
.=
((ADD (M,M)) . (fv1,gv1)) . x
by Th1
;
hence
((FuncComp M) . (fg1,v1)) . x = ((ADD (M,M)) . (fv1,gv1)) . x
;
verum
end;
reconsider F =
(FuncComp M) . (
fg1,
v1) as
Function of the
carrier of
M, the
carrier of
M by A16, Th6;
reconsider G =
(ADD (M,M)) . (
fv1,
gv1) as
Function of the
carrier of
M, the
carrier of
M ;
(f + g) * v =
F
by A16, A17, Th6
.=
G
by A22
.=
(f * v) + (g * v)
by A18, A19, Th3
;
hence
(f + g) * v = (f * v) + (g * v)
;
verum
end;
hence
End_Ring M is distributive
by A1; verum