let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of 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 of S; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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;
:: thesis: ( 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)) <> {}
;
:: thesis: 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));
:: thesis: ((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:
Den o,
(QuotMSAlg U1,(MSCng F)) =
(QuotCharact (MSCng F)) . o
by MSUALG_1:def 11
.=
QuotCharact (MSCng F),
o
by Def15
;
Args o,
(QuotMSAlg U1,(MSCng F)) = (((Class (MSCng F)) # ) * the Arity of S) . o
by MSUALG_1:def 9;
then consider a being
Element of
Args o,
U1 such that A3:
x = (MSCng F) # a
by Th2;
A4:
(
dom (Den o,U1) = Args o,
U1 &
rng (Den o,U1) c= Result o,
U1 )
by FUNCT_2:def 1;
A6:
o in the
carrier' of
S
;
o in dom (the Sorts of U1 * the ResultSort of S)
by A6, PARTFUN1:def 4;
then A8:
(the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . (the ResultSort of S . o)
by FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
then A9:
Result o,
U1 = the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 10;
reconsider da =
(Den o,U1) . a as
Element of the
Sorts of
U1 . (the_result_sort_of o) by A8, MSUALG_1:def 10;
A10:
(MSHomQuot F) . (the_result_sort_of o) = MSHomQuot F,
(the_result_sort_of o)
by Def22;
rng (Den o,U1) c= dom (QuotRes (MSCng F),o)
by A4, A8, A9, FUNCT_2:def 1;
then A11:
dom ((QuotRes (MSCng F),o) * (Den o,U1)) = dom (Den o,U1)
by RELAT_1:46;
A12:
(
dom ((MSHomQuot F) # x) = dom (the_arity_of o) &
dom (F # a) = dom (the_arity_of o) &
dom x = dom (the_arity_of o) &
dom a = dom (the_arity_of o) )
by MSUALG_3:6;
A13:
now let y be
set ;
:: thesis: ( y in dom (the_arity_of o) implies ((MSHomQuot F) # x) . y = (F # a) . y )assume A14:
y in dom (the_arity_of o)
;
:: thesis: ((MSHomQuot F) # x) . y = (F # a) . ythen reconsider n =
y as
Nat by ORDINAL1:def 13;
A15:
(the_arity_of o) /. n = (the_arity_of o) . n
by A14, PARTFUN1:def 8;
(the_arity_of o) . n in rng (the_arity_of o)
by A14, FUNCT_1:def 5;
then reconsider s =
(the_arity_of o) . n as
SortSymbol of
S ;
A16:
n in dom (the Sorts of U1 * (the_arity_of o))
by A14, PARTFUN1:def 4;
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 A16, FUNCT_1:22;
x . n = Class ((MSCng F) . s),
(a . n)
by A3, A14, A15, Def9;
then A17:
x . n = Class (MSCng F,s),
(a . n)
by A1, Def20;
((MSHomQuot F) # x) . n =
((MSHomQuot F) . s) . (x . n)
by A12, A14, A15, MSUALG_3:def 8
.=
(MSHomQuot F,s) . (x . n)
by Def22
.=
(F . s) . an
by A1, A17, Def21
.=
(F # a) . n
by A12, A14, A15, MSUALG_3:def 8
;
hence
((MSHomQuot F) # x) . y = (F # a) . y
;
:: thesis: verum end;
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 6;
then
product ((Class (MSCng F)) * (the_arity_of o)) = (((Class (MSCng F)) # ) * the Arity of S) . o
by MSAFREE:1;
then (Den o,(QuotMSAlg U1,(MSCng F))) . x =
((QuotRes (MSCng F),o) * (Den o,U1)) . a
by A2, A3, Def14
.=
(QuotRes (MSCng F),o) . da
by A4, A11, FUNCT_1:22
.=
Class (MSCng F),
da
by Def10
.=
Class (MSCng F,(the_result_sort_of o)),
da
by A1, Def20
;
then ((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, A10, Def21
.=
(Den o,U2) . (F # a)
by A1, MSUALG_3:def 9
;
hence
((MSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotMSAlg U1,(MSCng F))) . x) = (Den o,U2) . ((MSHomQuot F) # x)
by A12, A13, FUNCT_1:9;
:: thesis: verum
end;
hence
MSHomQuot F is_homomorphism QuotMSAlg U1,(MSCng F),U2
by MSUALG_3:def 9; :: according to MSUALG_3:def 11 :: thesis: 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 ;
:: thesis: ( 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
;
:: thesis: (MSHomQuot F) . i is one-to-one
then reconsider s =
i as
SortSymbol of
S ;
A18:
(MSHomQuot F) . i = MSHomQuot F,
s
by Def22;
for
x1,
x2 being
set 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
set ;
:: thesis: ( x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 implies x1 = x2 )
assume A19:
(
x1 in dom ((MSHomQuot F) . i) &
x2 in dom ((MSHomQuot F) . i) &
((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 )
;
:: thesis: x1 = x2
then A20:
(
x1 in (Class (MSCng F)) . s &
x2 in (Class (MSCng F)) . s )
by A18, FUNCT_2:def 1;
A21:
(MSCng F) . s = MSCng F,
s
by A1, Def20;
A22:
(
x1 in Class ((MSCng F) . s) &
x2 in Class ((MSCng F) . s) )
by A20, Def8;
then consider a1 being
set such that A23:
(
a1 in the
Sorts of
U1 . s &
x1 = Class ((MSCng F) . s),
a1 )
by EQREL_1:def 5;
consider a2 being
set such that A24:
(
a2 in the
Sorts of
U1 . s &
x2 = Class ((MSCng F) . s),
a2 )
by A22, EQREL_1:def 5;
reconsider a1 =
a1 as
Element of the
Sorts of
U1 . s by A23;
reconsider a2 =
a2 as
Element of the
Sorts of
U1 . s by A24;
(
((MSHomQuot F) . i) . x1 = (F . s) . a1 &
((MSHomQuot F) . i) . x2 = (F . s) . a2 )
by A1, A18, A21, A23, A24, Def21;
then
[a1,a2] in MSCng F,
s
by A19, Def19;
hence
x1 = x2
by A21, A23, A24, EQREL_1:44;
:: thesis: verum
end;
hence
(MSHomQuot F) . i is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
hence
MSHomQuot F is "1-1"
by MSUALG_3:1; :: thesis: verum