let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
let U1, U2 be non-empty MSAlgebra over S; for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
let F be ManySortedFunction of U1,U2; ( F is_homomorphism U1,U2 implies MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 )
set mc = MSCng F;
set qa = QuotMSAlg (U1,(MSCng F));
set qh = MSHomQuot F;
set S1 = the Sorts of U1;
assume A1:
F is_homomorphism U1,U2
; MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
for o being OperSymbol of S st Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} holds
for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
proof
let o be
OperSymbol of
S;
( Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} implies for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) )
assume
Args (
o,
(QuotMSAlg (U1,(MSCng F))))
<> {}
;
for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
let x be
Element of
Args (
o,
(QuotMSAlg (U1,(MSCng F))));
((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
A2:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
Args (
o,
(QuotMSAlg (U1,(MSCng F))))
= (((Class (MSCng F)) #) * the Arity of S) . o
by MSUALG_1:def 4;
then consider a being
Element of
Args (
o,
U1)
such that A3:
x = (MSCng F) # a
by Th2;
A4:
dom a = dom (the_arity_of o)
by MSUALG_3:6;
A5:
now for y being object st y in dom (the_arity_of o) holds
((MSHomQuot F) # x) . y = (F # a) . ylet y be
object ;
( y in dom (the_arity_of o) implies ((MSHomQuot F) # x) . y = (F # a) . y )assume A6:
y in dom (the_arity_of o)
;
((MSHomQuot F) # x) . y = (F # a) . ythen reconsider n =
y as
Nat by ORDINAL1:def 12;
(the_arity_of o) . n in rng (the_arity_of o)
by A6, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . n as
SortSymbol of
S ;
A7:
(the_arity_of o) /. n = (the_arity_of o) . n
by A6, PARTFUN1:def 6;
then
x . n = Class (
((MSCng F) . s),
(a . n))
by A3, A6, Def7;
then A8:
x . n = Class (
(MSCng (F,s)),
(a . n))
by A1, Def18;
A9:
n in dom ( the Sorts of U1 * (the_arity_of o))
by A6, PARTFUN1:def 2;
then
a . n in ( the Sorts of U1 * (the_arity_of o)) . n
by MSUALG_3:6;
then reconsider an =
a . n as
Element of the
Sorts of
U1 . s by A9, FUNCT_1:12;
((MSHomQuot F) # x) . n =
((MSHomQuot F) . s) . (x . n)
by A2, A6, A7, MSUALG_3:def 6
.=
(MSHomQuot (F,s)) . (x . n)
by Def20
.=
(F . s) . an
by A1, A8, Def19
.=
(F # a) . n
by A4, A6, A7, MSUALG_3:def 6
;
hence
((MSHomQuot F) # x) . y = (F # a) . y
;
verum end;
o in the
carrier' of
S
;
then
o in dom ( the Sorts of U1 * the ResultSort of S)
by PARTFUN1:def 2;
then A10:
( the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . ( the ResultSort of S . o)
by FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 2
;
then
(
rng (Den (o,U1)) c= Result (
o,
U1) &
Result (
o,
U1)
= the
Sorts of
U1 . (the_result_sort_of o) )
by MSUALG_1:def 5;
then
rng (Den (o,U1)) c= dom (QuotRes ((MSCng F),o))
by A10, FUNCT_2:def 1;
then A11:
(
dom (Den (o,U1)) = Args (
o,
U1) &
dom ((QuotRes ((MSCng F),o)) * (Den (o,U1))) = dom (Den (o,U1)) )
by FUNCT_2:def 1, RELAT_1:27;
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 1;
then A12:
product ((Class (MSCng F)) * (the_arity_of o)) = (((Class (MSCng F)) #) * the Arity of S) . o
by MSAFREE:1;
reconsider da =
(Den (o,U1)) . a as
Element of the
Sorts of
U1 . (the_result_sort_of o) by A10, MSUALG_1:def 5;
A13:
(MSHomQuot F) . (the_result_sort_of o) = MSHomQuot (
F,
(the_result_sort_of o))
by Def20;
Den (
o,
(QuotMSAlg (U1,(MSCng F)))) =
(QuotCharact (MSCng F)) . o
by MSUALG_1:def 6
.=
QuotCharact (
(MSCng F),
o)
by Def13
;
then (Den (o,(QuotMSAlg (U1,(MSCng F))))) . x =
((QuotRes ((MSCng F),o)) * (Den (o,U1))) . a
by A3, A12, Def12
.=
(QuotRes ((MSCng F),o)) . da
by A11, FUNCT_1:12
.=
Class (
(MSCng F),
da)
by Def8
.=
Class (
(MSCng (F,(the_result_sort_of o))),
da)
by A1, Def18
;
then A14:
((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) =
(F . (the_result_sort_of o)) . ((Den (o,U1)) . a)
by A1, A13, Def19
.=
(Den (o,U2)) . (F # a)
by A1
;
(
dom ((MSHomQuot F) # x) = dom (the_arity_of o) &
dom (F # a) = dom (the_arity_of o) )
by MSUALG_3:6;
hence
((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
by A5, A14, FUNCT_1:2;
verum
end;
hence
MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2
; MSUALG_3:def 9 MSHomQuot F is "1-1"
for i being set st i in the carrier of S holds
(MSHomQuot F) . i is one-to-one
proof
let i be
set ;
( i in the carrier of S implies (MSHomQuot F) . i is one-to-one )
set f =
(MSHomQuot F) . i;
assume
i in the
carrier of
S
;
(MSHomQuot F) . i is one-to-one
then reconsider s =
i as
SortSymbol of
S ;
A15:
(MSHomQuot F) . i = MSHomQuot (
F,
s)
by Def20;
for
x1,
x2 being
object st
x1 in dom ((MSHomQuot F) . i) &
x2 in dom ((MSHomQuot F) . i) &
((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 implies x1 = x2 )
assume that A16:
x1 in dom ((MSHomQuot F) . i)
and A17:
x2 in dom ((MSHomQuot F) . i)
and A18:
((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2
;
x1 = x2
x1 in (Class (MSCng F)) . s
by A15, A16, FUNCT_2:def 1;
then
x1 in Class ((MSCng F) . s)
by Def6;
then consider a1 being
object such that A19:
a1 in the
Sorts of
U1 . s
and A20:
x1 = Class (
((MSCng F) . s),
a1)
by EQREL_1:def 3;
x2 in (Class (MSCng F)) . s
by A15, A17, FUNCT_2:def 1;
then
x2 in Class ((MSCng F) . s)
by Def6;
then consider a2 being
object such that A21:
a2 in the
Sorts of
U1 . s
and A22:
x2 = Class (
((MSCng F) . s),
a2)
by EQREL_1:def 3;
reconsider a2 =
a2 as
Element of the
Sorts of
U1 . s by A21;
A23:
(MSCng F) . s = MSCng (
F,
s)
by A1, Def18;
then A24:
((MSHomQuot F) . i) . x2 = (F . s) . a2
by A1, A15, A22, Def19;
reconsider a1 =
a1 as
Element of the
Sorts of
U1 . s by A19;
((MSHomQuot F) . i) . x1 = (F . s) . a1
by A1, A15, A23, A20, Def19;
then
[a1,a2] in MSCng (
F,
s)
by A18, A24, Def17;
hence
x1 = x2
by A23, A20, A22, EQREL_1:35;
verum
end;
hence
(MSHomQuot F) . i is
one-to-one
by FUNCT_1:def 4;
verum
end;
hence
MSHomQuot F is "1-1"
by MSUALG_3:1; verum