let M, N 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 } ;
for y being object 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
object ;
( 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
object such that A2:
(
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 A2, FUNCT_1:17;
then
y in { [v,w] where v, w is Element of M : f . v = f . w }
by A2;
then consider v9,
w9 being
Element of
M such that A3:
(
y = [v9,w9] &
f . v9 = f . w9 )
;
thus
y in [: the carrier of M, the carrier of M:]
by A3, 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:]
;
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;
A4:
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 A5:
(
i in dom r &
r . i = [v,w] )
;
v in Class (R,w)
then A6:
r . i = i
by FUNCT_1:17;
consider v9,
w9 being
Element of
M such that A7:
(
i = [v9,w9] &
f . v9 = f . w9 )
by A5;
[v,w] in equ_kernel f
by A7, Def8, A5, A6;
hence
v in Class (
R,
w)
by EQREL_1:19;
verum
end;
then A8:
equ_rel r c= R
by Th3;
for z being object st z in R holds
z in equ_rel r
proof
let z be
object ;
( z in R implies z in equ_rel r )
assume A9:
z in R
;
z in equ_rel r
then consider x,
y being
object such that A10:
(
x in the
carrier of
M &
y in the
carrier of
M &
z = [x,y] )
by ZFMISC_1:def 2;
A11:
f . x = f . y
by A9, A10, Def8;
reconsider x =
x,
y =
y as
Element of
M by A10;
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) } ;
A12:
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 A4;
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 A13:
(
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];
A14:
[x,y] in { [v,w] where v, w is Element of M : f . v = f . w }
by A11;
then
r . [x,y] = [x,y]
by FUNCT_1:17;
then
x in Class (
R9,
y)
by A14, A13;
hence
z in Y
by A10, A13, EQREL_1:19;
verum
end;
hence
z in equ_rel r
by A12, SETFAM_1:def 1;
verum
end;
then
R c= equ_rel r
;
hence
equ_kernel f = equ_rel r
by A8, XBOOLE_0:def 10; verum