let N, M be non empty multMagma ; for f being Function of M,N st f is multiplicative holds
ex r being Relators of M st equ_kernel f = equ_rel r
let f be Function of M,N; ( f is multiplicative implies ex r being Relators of M st equ_kernel f = equ_rel r )
assume A1:
f is multiplicative
; ex r being Relators of M st equ_kernel f = equ_rel r
set I = { [v,w] where v, w is Element of M : f . v = f . w } ;
set r = id { [v,w] where v, w is Element of M : f . v = f . w } ;
A2:
dom (id { [v,w] where v, w is Element of M : f . v = f . w } ) = { [v,w] where v, w is Element of M : f . v = f . w }
by FUNCT_1:17;
for y being set st y in rng (id { [v,w] where v, w is Element of M : f . v = f . w } ) holds
y in [: the carrier of M, the carrier of M:]
proof
let y be
set ;
( y in rng (id { [v,w] where v, w is Element of M : f . v = f . w } ) implies y in [: the carrier of M, the carrier of M:] )
assume
y in rng (id { [v,w] where v, w is Element of M : f . v = f . w } )
;
y in [: the carrier of M, the carrier of M:]
then consider x being
set such that A3:
(
x in dom (id { [v,w] where v, w is Element of M : f . v = f . w } ) &
y = (id { [v,w] where v, w is Element of M : f . v = f . w } ) . x )
by FUNCT_1:def 3;
y = x
by A3, FUNCT_1:17;
then
y in { [v,w] where v, w is Element of M : f . v = f . w }
by A3;
then consider v9,
w9 being
Element of
M such that A4:
(
y = [v9,w9] &
f . v9 = f . w9 )
;
thus
y in [: the carrier of M, the carrier of M:]
by A4, ZFMISC_1:def 2;
verum
end;
then
rng (id { [v,w] where v, w is Element of M : f . v = f . w } ) c= [: the carrier of M, the carrier of M:]
by TARSKI:def 3;
then reconsider r = id { [v,w] where v, w is Element of M : f . v = f . w } as Relators of M by FUNCT_2:2;
take
r
; equ_kernel f = equ_rel r
reconsider R = equ_kernel f as compatible Equivalence_Relation of M by A1, Th4;
A5:
for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w)
proof
let i be
set ;
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w)let v,
w be
Element of
M;
( i in dom r & r . i = [v,w] implies v in Class (R,w) )
assume A6:
(
i in dom r &
r . i = [v,w] )
;
v in Class (R,w)
then A7:
r . i = i
by A2, FUNCT_1:17;
consider v9,
w9 being
Element of
M such that A8:
(
i = [v9,w9] &
f . v9 = f . w9 )
by A2, A6;
[v,w] in equ_kernel f
by A8, Def8, A6, A7;
hence
v in Class (
R,
w)
by EQREL_1:19;
verum
end;
then A9:
equ_rel r c= R
by Th3;
for z being set st z in R holds
z in equ_rel r
proof
let z be
set ;
( z in R implies z in equ_rel r )
assume A10:
z in R
;
z in equ_rel r
then consider x,
y being
set such that A11:
(
x in the
carrier of
M &
y in the
carrier of
M &
z = [x,y] )
by ZFMISC_1:def 2;
A12:
f . x = f . y
by A10, A11, Def8;
reconsider x =
x,
y =
y as
Element of
M by A11;
set X9 =
{ R9 where R9 is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R9,w) } ;
A13:
R in { R9 where R9 is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R9,w) }
by A5;
for
Y being
set st
Y in { R9 where R9 is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R9,w) } holds
z in Y
proof
let Y be
set ;
( Y in { R9 where R9 is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R9,w) } implies z in Y )
assume
Y in { R9 where R9 is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R9,w) }
;
z in Y
then consider R9 being
compatible Equivalence_Relation of
M such that A14:
(
R9 = Y & ( for
i being
set for
v,
w being
Element of
M st
i in dom r &
r . i = [v,w] holds
v in Class (
R9,
w) ) )
;
set i =
[x,y];
A15:
[x,y] in { [v,w] where v, w is Element of M : f . v = f . w }
by A12;
then
r . [x,y] = [x,y]
by FUNCT_1:17;
then
x in Class (
R9,
y)
by A2, A15, A14;
hence
z in Y
by A11, A14, EQREL_1:19;
verum
end;
hence
z in equ_rel r
by A13, SETFAM_1:def 1;
verum
end;
then
R c= equ_rel r
by TARSKI:def 3;
hence
equ_kernel f = equ_rel r
by A9, XBOOLE_0:def 10; verum