let M be AbGroup; End_Ring M is associative
for f, g, h being Element of (End_Ring M) holds (f * g) * h = f * (g * h)
proof
let f,
g,
h be
Element of
(End_Ring M);
(f * g) * h = f * (g * h)
f in set_End M
;
then consider f1 being
Function of the
carrier of
M, the
carrier of
M such that A1:
(
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 A2:
(
g1 = g &
g1 is
Endomorphism of
M )
;
h in set_End M
;
then consider h1 being
Function of the
carrier of
M, the
carrier of
M such that A3:
(
h1 = h &
h1 is
Endomorphism of
M )
;
f * g in set_End M
;
then consider fg1 being
Function of the
carrier of
M, the
carrier of
M such that A4:
(
fg1 = f * g &
fg1 is
Endomorphism of
M )
;
g * h in set_End M
;
then consider gh1 being
Function of the
carrier of
M, the
carrier of
M such that A5:
(
gh1 = g * h &
gh1 is
Endomorphism of
M )
;
A6:
f * g = (FuncComp M) . (
f1,
g1)
by A1, A2, Th6;
A7:
g * h = (FuncComp M) . (
g1,
h1)
by A2, A3, Th6;
reconsider f1 =
f1,
g1 =
g1,
h1 =
h1,
fg1 =
fg1,
gh1 =
gh1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
A8:
for
x being
Element of
M holds
((FuncComp M) . (fg1,h1)) . x = ((FuncComp M) . (f1,gh1)) . x
proof
let x be
Element of the
carrier of
M;
((FuncComp M) . (fg1,h1)) . x = ((FuncComp M) . (f1,gh1)) . x
A9:
g1 . (h1 . x) =
(g1 * h1) . x
by FUNCT_2:15
.=
gh1 . x
by A5, A7, Def4
;
((FuncComp M) . (fg1,h1)) . x =
(fg1 * h1) . x
by Def4
.=
((FuncComp M) . (f1,g1)) . (h1 . x)
by A4, A6, FUNCT_2:15
.=
(f1 * g1) . (h1 . x)
by Def4
.=
f1 . (gh1 . x)
by A9, FUNCT_2:15
.=
(f1 * gh1) . x
by FUNCT_2:15
.=
((FuncComp M) . (f1,gh1)) . x
by Def4
;
hence
((FuncComp M) . (fg1,h1)) . x = ((FuncComp M) . (f1,gh1)) . x
;
verum
end;
reconsider F =
(FuncComp M) . (
fg1,
h1) as
Function of the
carrier of
M, the
carrier of
M ;
reconsider G =
(FuncComp M) . (
f1,
gh1) as
Function of the
carrier of
M, the
carrier of
M ;
(f * g) * h =
F
by A3, A4, Th6
.=
G
by A8
.=
f * (g * h)
by A1, A5, Th6
;
hence
(f * g) * h = f * (g * h)
;
verum
end;
hence
End_Ring M is associative
; verum