set g = canHom f;
set A = R / (ker f);
set B = Image f;
set I = ker f;
now for x, y being Element of (R / (ker f)) holds (canHom f) . (x + y) = ((canHom f) . x) + ((canHom f) . y)let x,
y be
Element of
(R / (ker f));
(canHom f) . (x + y) = ((canHom f) . x) + ((canHom f) . y)consider a being
Element of
R such that H1:
x = Class (
(EqRel (R,(ker f))),
a)
by RING_1:11;
consider b being
Element of
R such that H2:
y = Class (
(EqRel (R,(ker f))),
b)
by RING_1:11;
H3:
(canHom f) . x = f . a
by H1, ch;
H4:
(canHom f) . y = f . b
by H2, ch;
x + y = Class (
(EqRel (R,(ker f))),
(a + b))
by H1, H2, RING_1:13;
hence (canHom f) . (x + y) =
f . (a + b)
by ch
.=
(f . a) + (f . b)
by VECTSP_1:def 20
.=
((canHom f) . x) + ((canHom f) . y)
by H3, H4, T5
;
verum end;
hence
canHom f is additive
; ( canHom f is multiplicative & canHom f is unity-preserving )
now for x, y being Element of (R / (ker f)) holds (canHom f) . (x * y) = ((canHom f) . x) * ((canHom f) . y)let x,
y be
Element of
(R / (ker f));
(canHom f) . (x * y) = ((canHom f) . x) * ((canHom f) . y)consider a being
Element of
R such that H1:
x = Class (
(EqRel (R,(ker f))),
a)
by RING_1:11;
consider b being
Element of
R such that H2:
y = Class (
(EqRel (R,(ker f))),
b)
by RING_1:11;
H3:
(canHom f) . x = f . a
by H1, ch;
H4:
(canHom f) . y = f . b
by H2, ch;
x * y = Class (
(EqRel (R,(ker f))),
(a * b))
by H1, H2, RING_1:14;
hence (canHom f) . (x * y) =
f . (a * b)
by ch
.=
(f . a) * (f . b)
by GROUP_6:def 6
.=
((canHom f) . x) * ((canHom f) . y)
by H3, H4, T5
;
verum end;
hence
canHom f is multiplicative
; canHom f is unity-preserving
(canHom f) . (1. (R / (ker f))) =
(canHom f) . (Class ((EqRel (R,(ker f))),(1. R)))
by RING_1:15
.=
f . (1_ R)
by ch
.=
1_ S
by GROUP_1:def 13
.=
1. (Image f)
by defim
;
hence
canHom f is unity-preserving
; verum