let M, N be non empty multMagma ; for f being Function of M,N
for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )
let f be Function of M,N; for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )
let H be non empty multSubmagma of N; for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )
let R be compatible Equivalence_Relation of M; ( f is multiplicative & the carrier of H = rng f & R = equ_kernel f implies ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative ) )
assume A1:
f is multiplicative
; ( not the carrier of H = rng f or not R = equ_kernel f or ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative ) )
assume A2:
the carrier of H = rng f
; ( not R = equ_kernel f or ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative ) )
assume A3:
R = equ_kernel f
; ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )
set g = ((nat_hom R) ~) * f;
for x, y1, y2 being object st [x,y1] in ((nat_hom R) ~) * f & [x,y2] in ((nat_hom R) ~) * f holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in ((nat_hom R) ~) * f & [x,y2] in ((nat_hom R) ~) * f implies y1 = y2 )
assume
[x,y1] in ((nat_hom R) ~) * f
;
( not [x,y2] in ((nat_hom R) ~) * f or y1 = y2 )
then consider z1 being
object such that A4:
(
[x,z1] in (nat_hom R) ~ &
[z1,y1] in f )
by RELAT_1:def 8;
assume
[x,y2] in ((nat_hom R) ~) * f
;
y1 = y2
then consider z2 being
object such that A5:
(
[x,z2] in (nat_hom R) ~ &
[z2,y2] in f )
by RELAT_1:def 8;
A6:
(
[z1,x] in nat_hom R &
[z2,x] in nat_hom R )
by A4, A5, RELAT_1:def 7;
then
(
z1 in dom (nat_hom R) &
z2 in dom (nat_hom R) )
by XTUPLE_0:def 12;
then reconsider z1 =
z1,
z2 =
z2 as
Element of
M ;
A7:
(
x = (nat_hom R) . z1 &
x = (nat_hom R) . z2 )
by A6, FUNCT_1:1;
A8:
(
f . z1 = y1 &
f . z2 = y2 )
by A4, A5, FUNCT_1:1;
(
(nat_hom R) . z1 = Class (
R,
z1) &
(nat_hom R) . z2 = Class (
R,
z2) )
by Def6;
then
z2 in Class (
R,
z1)
by A7, EQREL_1:23;
then
[z1,z2] in equ_kernel f
by A3, EQREL_1:18;
hence
y1 = y2
by A8, Def8;
verum
end;
then reconsider g = ((nat_hom R) ~) * f as Function by FUNCT_1:def 1;
rng (nat_hom R) = the carrier of (M ./. R)
by FUNCT_2:def 3;
then A9:
dom ((nat_hom R) ~) = the carrier of (M ./. R)
by RELAT_1:20;
the carrier of M c= dom f
by FUNCT_2:def 1;
then
dom (nat_hom R) c= dom f
;
then
rng ((nat_hom R) ~) c= dom f
by RELAT_1:20;
then A10:
dom g = the carrier of (M ./. R)
by A9, RELAT_1:27;
dom f c= the carrier of M
;
then
dom f c= dom (nat_hom R)
by FUNCT_2:def 1;
then
dom f c= rng ((nat_hom R) ~)
by RELAT_1:20;
then A11:
rng g = the carrier of H
by A2, RELAT_1:28;
then reconsider g = g as Function of (M ./. R),H by A10, FUNCT_2:1;
take
g
; ( f = g * (nat_hom R) & g is bijective & g is multiplicative )
for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume A12:
x1 in dom g
;
( not x2 in dom g or not g . x1 = g . x2 or x1 = x2 )
assume A13:
x2 in dom g
;
( not g . x1 = g . x2 or x1 = x2 )
assume A14:
g . x1 = g . x2
;
x1 = x2
set y =
g . x1;
[x1,(g . x1)] in g
by A12, FUNCT_1:1;
then consider z1 being
object such that A15:
(
[x1,z1] in (nat_hom R) ~ &
[z1,(g . x1)] in f )
by RELAT_1:def 8;
[x2,(g . x1)] in g
by A14, A13, FUNCT_1:1;
then consider z2 being
object such that A16:
(
[x2,z2] in (nat_hom R) ~ &
[z2,(g . x1)] in f )
by RELAT_1:def 8;
A17:
(
[z1,x1] in nat_hom R &
[z2,x2] in nat_hom R )
by A15, A16, RELAT_1:def 7;
then
(
z1 in dom (nat_hom R) &
z2 in dom (nat_hom R) )
by XTUPLE_0:def 12;
then reconsider z1 =
z1,
z2 =
z2 as
Element of
M ;
(
z1 in dom f &
z2 in dom f &
f . z1 = g . x1 &
f . z2 = g . x1 )
by A15, A16, FUNCT_1:1;
then
[z1,z2] in equ_kernel f
by Def8;
then A18:
z2 in Class (
R,
z1)
by A3, EQREL_1:18;
A19:
(
(nat_hom R) . z1 = Class (
R,
z1) &
(nat_hom R) . z2 = Class (
R,
z2) )
by Def6;
(
x1 = (nat_hom R) . z1 &
x2 = (nat_hom R) . z2 )
by A17, FUNCT_1:1;
hence
x1 = x2
by A19, A18, EQREL_1:23;
verum
end;
then A20:
g is one-to-one
by FUNCT_1:def 4;
A21:
for x being object holds
( x in dom f iff ( x in dom (nat_hom R) & (nat_hom R) . x in dom g ) )
for x being object st x in dom f holds
f . x = g . ((nat_hom R) . x)
proof
let x be
object ;
( x in dom f implies f . x = g . ((nat_hom R) . x) )
assume A22:
x in dom f
;
f . x = g . ((nat_hom R) . x)
set y =
(nat_hom R) . x;
(nat_hom R) . x in dom g
by A22, A21;
then
[((nat_hom R) . x),(g . ((nat_hom R) . x))] in g
by FUNCT_1:1;
then consider z being
object such that A23:
(
[((nat_hom R) . x),z] in (nat_hom R) ~ &
[z,(g . ((nat_hom R) . x))] in f )
by RELAT_1:def 8;
[z,((nat_hom R) . x)] in nat_hom R
by A23, RELAT_1:def 7;
then A24:
(
z in dom (nat_hom R) &
(nat_hom R) . x = (nat_hom R) . z )
by FUNCT_1:1;
A25:
(
z in dom f &
g . ((nat_hom R) . x) = f . z )
by A23, FUNCT_1:1;
then reconsider z9 =
z,
x9 =
x as
Element of
M by A22;
(
(nat_hom R) . z9 = Class (
R,
z9) &
(nat_hom R) . x9 = Class (
R,
x9) )
by Def6;
then
z9 in Class (
R,
x9)
by A24, EQREL_1:23;
then
[x,z] in R
by EQREL_1:18;
hence
f . x = g . ((nat_hom R) . x)
by A25, A3, Def8;
verum
end;
hence
f = g * (nat_hom R)
by A21, FUNCT_1:10; ( g is bijective & g is multiplicative )
g is onto
by A11, FUNCT_2:def 3;
hence
g is bijective
by A20; g is multiplicative
for v, w being Element of (M ./. R) holds g . (v * w) = (g . v) * (g . w)
proof
let v,
w be
Element of
(M ./. R);
g . (v * w) = (g . v) * (g . w)
v * w in the
carrier of
(M ./. R)
;
then
v * w in dom g
by FUNCT_2:def 1;
then
[(v * w),(g . (v * w))] in g
by FUNCT_1:1;
then consider z being
object such that A26:
(
[(v * w),z] in (nat_hom R) ~ &
[z,(g . (v * w))] in f )
by RELAT_1:def 8;
[z,(v * w)] in nat_hom R
by A26, RELAT_1:def 7;
then A27:
(
z in dom (nat_hom R) &
(nat_hom R) . z = v * w )
by FUNCT_1:1;
A28:
f . z = g . (v * w)
by A26, FUNCT_1:1;
v in the
carrier of
(M ./. R)
;
then
v in dom g
by FUNCT_2:def 1;
then
[v,(g . v)] in g
by FUNCT_1:1;
then consider z1 being
object such that A29:
(
[v,z1] in (nat_hom R) ~ &
[z1,(g . v)] in f )
by RELAT_1:def 8;
[z1,v] in nat_hom R
by A29, RELAT_1:def 7;
then A30:
(
z1 in dom (nat_hom R) &
(nat_hom R) . z1 = v )
by FUNCT_1:1;
A31:
f . z1 = g . v
by A29, FUNCT_1:1;
w in the
carrier of
(M ./. R)
;
then
w in dom g
by FUNCT_2:def 1;
then
[w,(g . w)] in g
by FUNCT_1:1;
then consider z2 being
object such that A32:
(
[w,z2] in (nat_hom R) ~ &
[z2,(g . w)] in f )
by RELAT_1:def 8;
[z2,w] in nat_hom R
by A32, RELAT_1:def 7;
then A33:
(
z2 in dom (nat_hom R) &
(nat_hom R) . z2 = w )
by FUNCT_1:1;
A34:
f . z2 = g . w
by A32, FUNCT_1:1;
reconsider z1 =
z1,
z2 =
z2,
z =
z as
Element of
M by A30, A33, A27;
A35:
(nat_hom R) . z = (nat_hom R) . (z1 * z2)
by A30, A33, A27, GROUP_6:def 6;
(
(nat_hom R) . (z1 * z2) = Class (
R,
(z1 * z2)) &
(nat_hom R) . z = Class (
R,
z) )
by Def6;
then
z1 * z2 in Class (
R,
z)
by A35, EQREL_1:23;
then
[z,(z1 * z2)] in R
by EQREL_1:18;
then A36:
f . z =
f . (z1 * z2)
by A3, Def8
.=
(f . z1) * (f . z2)
by A1, GROUP_6:def 6
;
A37:
[(g . v),(g . w)] in [: the carrier of H, the carrier of H:]
by ZFMISC_1:def 2;
thus g . (v * w) =
the
multF of
N . [(g . v),(g . w)]
by A31, A34, A36, A28, BINOP_1:def 1
.=
( the multF of N | [: the carrier of H, the carrier of H:]) . [(g . v),(g . w)]
by A37, FUNCT_1:49
.=
( the multF of N | [: the carrier of H, the carrier of H:]) . (
(g . v),
(g . w))
by BINOP_1:def 1
.=
( the multF of N || the carrier of H) . (
(g . v),
(g . w))
by REALSET1:def 2
.=
(g . v) * (g . w)
by Def9
;
verum
end;
hence
g is multiplicative
by GROUP_6:def 6; verum