set g = canHom I;
set B = R / I;
now for a, b being Element of R holds (canHom I) . (a + b) = ((canHom I) . a) + ((canHom I) . b)let a,
b be
Element of
R;
(canHom I) . (a + b) = ((canHom I) . a) + ((canHom I) . b)reconsider x =
Class (
(EqRel (R,I)),
a) as
Element of
(R / I) by RING_1:12;
reconsider y =
Class (
(EqRel (R,I)),
b) as
Element of
(R / I) by RING_1:12;
H1:
(canHom I) . a = Class (
(EqRel (R,I)),
a)
by defhomI;
H:
x + y = Class (
(EqRel (R,I)),
(a + b))
by RING_1:13;
thus (canHom I) . (a + b) =
x + y
by H, defhomI
.=
((canHom I) . a) + ((canHom I) . b)
by H1, defhomI
;
verum end;
hence
canHom I is additive
; ( canHom I is multiplicative & canHom I is unity-preserving )
now for a, b being Element of R holds (canHom I) . (a * b) = ((canHom I) . a) * ((canHom I) . b)let a,
b be
Element of
R;
(canHom I) . (a * b) = ((canHom I) . a) * ((canHom I) . b)reconsider x =
Class (
(EqRel (R,I)),
a) as
Element of
(R / I) by RING_1:12;
reconsider y =
Class (
(EqRel (R,I)),
b) as
Element of
(R / I) by RING_1:12;
H1:
(canHom I) . a = Class (
(EqRel (R,I)),
a)
by defhomI;
H:
x * y = Class (
(EqRel (R,I)),
(a * b))
by RING_1:14;
thus (canHom I) . (a * b) =
x * y
by H, defhomI
.=
((canHom I) . a) * ((canHom I) . b)
by H1, defhomI
;
verum end;
hence
canHom I is multiplicative
; canHom I is unity-preserving
(canHom I) . (1. R) =
Class ((EqRel (R,I)),(1. R))
by defhomI
.=
1. (R / I)
by RING_1:15
;
hence
canHom I is unity-preserving
; verum