let S be locally_directed OrderSortedSign; :: thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is order-sorted )
let U1, U2 be non-empty OSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is order-sorted )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies ( OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is order-sorted ) )
set mc = OSCng F;
set qa = QuotOSAlg U1,(OSCng F);
set qh = OSHomQuot F;
set S1 = the Sorts of U1;
assume A1:
( F is_homomorphism U1,U2 & F is order-sorted )
; :: thesis: ( OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is order-sorted )
for o being Element of the carrier' of S st Args o,(QuotOSAlg U1,(OSCng F)) <> {} holds
for x being Element of Args o,(QuotOSAlg U1,(OSCng F)) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) = (Den o,U2) . ((OSHomQuot F) # x)
proof
let o be
Element of the
carrier' of
S;
:: thesis: ( Args o,(QuotOSAlg U1,(OSCng F)) <> {} implies for x being Element of Args o,(QuotOSAlg U1,(OSCng F)) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) = (Den o,U2) . ((OSHomQuot F) # x) )
assume
Args o,
(QuotOSAlg U1,(OSCng F)) <> {}
;
:: thesis: for x being Element of Args o,(QuotOSAlg U1,(OSCng F)) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) = (Den o,U2) . ((OSHomQuot F) # x)
let x be
Element of
Args o,
(QuotOSAlg U1,(OSCng F));
:: thesis: ((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) = (Den o,U2) . ((OSHomQuot F) # x)
reconsider o1 =
o as
OperSymbol of
S ;
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
A2:
Den o,
(QuotOSAlg U1,(OSCng F)) =
(OSQuotCharact (OSCng F)) . o
by MSUALG_1:def 11
.=
OSQuotCharact (OSCng F),
o1
by Def21
;
Args o,
(QuotOSAlg U1,(OSCng F)) = (((OSClass (OSCng F)) # ) * the Arity of S) . o
by MSUALG_1:def 9;
then consider a being
Element of
Args o,
U1 such that A3:
x = (OSCng F) #_os a
by Th15;
A4:
(
dom (Den o,U1) = Args o,
U1 &
rng (Den o,U1) c= Result o,
U1 )
by FUNCT_2:def 1;
o in the
carrier' of
S
;
then
o in dom (the Sorts of U1 * the ResultSort of S)
by PARTFUN1:def 4;
then A5:
(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 A6:
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 A5, MSUALG_1:def 10;
A7:
(OSHomQuot F) . (the_result_sort_of o) = OSHomQuot F,
(the_result_sort_of o)
by Def27;
rng (Den o,U1) c= dom (OSQuotRes (OSCng F),o)
by A4, A5, A6, FUNCT_2:def 1;
then A8:
dom ((OSQuotRes (OSCng F),o) * (Den o,U1)) = dom (Den o,U1)
by RELAT_1:46;
A9:
(
dom ((OSHomQuot 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;
A10:
now let y be
set ;
:: thesis: ( y in dom (the_arity_of o) implies ((OSHomQuot F) # x) . y = (F # a) . y )assume A11:
y in dom (the_arity_of o)
;
:: thesis: ((OSHomQuot F) # x) . y = (F # a) . ythen reconsider n =
y as
Nat ;
A12:
(the_arity_of o) /. n = (the_arity_of o) . n
by A11, PARTFUN1:def 8;
(the_arity_of o) . n in rng (the_arity_of o)
by A11, FUNCT_1:def 5;
then reconsider s =
(the_arity_of o) . n as
SortSymbol of
S ;
consider an being
Element of the
Sorts of
U1 . s such that A13:
(
an = a . n &
x . n = OSClass (OSCng F),
an )
by A3, A11, A12, Def15;
((OSHomQuot F) # x) . n =
((OSHomQuot F) . s) . (x . n)
by A9, A11, A12, MSUALG_3:def 8
.=
(OSHomQuot F,s) . (OSClass (OSCng F),an)
by A13, Def27
.=
(F . s) . an
by A1, Def26
.=
(F # a) . n
by A9, A11, A12, A13, MSUALG_3:def 8
;
hence
((OSHomQuot 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 ((OSClass (OSCng F)) * (the_arity_of o)) = (((OSClass (OSCng F)) # ) * the Arity of S) . o
by MSAFREE:1;
then (Den o,(QuotOSAlg U1,(OSCng F))) . x =
((OSQuotRes (OSCng F),o) * (Den o,U1)) . a
by A2, A3, Def20
.=
(OSQuotRes (OSCng F),o) . da
by A4, A8, FUNCT_1:22
.=
OSClass (OSCng F),
da
by Def16
;
then ((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) =
(F . (the_result_sort_of o)) . ((Den o,U1) . a)
by A1, A7, Def26
.=
(Den o,U2) . (F # a)
by A1, MSUALG_3:def 9
;
hence
((OSHomQuot F) . (the_result_sort_of o)) . ((Den o,(QuotOSAlg U1,(OSCng F))) . x) = (Den o,U2) . ((OSHomQuot F) # x)
by A9, A10, FUNCT_1:9;
:: thesis: verum
end;
hence
OSHomQuot F is_homomorphism QuotOSAlg U1,(OSCng F),U2
by MSUALG_3:def 9; :: according to MSUALG_3:def 11 :: thesis: ( OSHomQuot F is "1-1" & OSHomQuot F is order-sorted )
for i being set st i in the carrier of S holds
(OSHomQuot F) . i is one-to-one
proof
let i be
set ;
:: thesis: ( i in the carrier of S implies (OSHomQuot F) . i is one-to-one )
set f =
(OSHomQuot F) . i;
assume
i in the
carrier of
S
;
:: thesis: (OSHomQuot F) . i is one-to-one
then reconsider s =
i as
SortSymbol of
S ;
A14:
(OSHomQuot F) . i = OSHomQuot F,
s
by Def27;
for
x1,
x2 being
set st
x1 in dom ((OSHomQuot F) . i) &
x2 in dom ((OSHomQuot F) . i) &
((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom ((OSHomQuot F) . i) & x2 in dom ((OSHomQuot F) . i) & ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 implies x1 = x2 )
assume A15:
(
x1 in dom ((OSHomQuot F) . i) &
x2 in dom ((OSHomQuot F) . i) &
((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 )
;
:: thesis: x1 = x2
then
(
x1 in (OSClass (OSCng F)) . s &
x2 in (OSClass (OSCng F)) . s )
by A14, FUNCT_2:def 1;
then A16:
(
x1 in OSClass (OSCng F),
s &
x2 in OSClass (OSCng F),
s )
by Def13;
then consider a1 being
set such that A17:
(
a1 in the
Sorts of
U1 . s &
x1 = Class (CompClass (OSCng F),(CComp s)),
a1 )
by Def12;
consider a2 being
set such that A18:
(
a2 in the
Sorts of
U1 . s &
x2 = Class (CompClass (OSCng F),(CComp s)),
a2 )
by A16, Def12;
reconsider a1 =
a1 as
Element of the
Sorts of
U1 . s by A17;
reconsider a2 =
a2 as
Element of the
Sorts of
U1 . s by A18;
A19:
(
x1 = OSClass (OSCng F),
a1 &
x2 = OSClass (OSCng F),
a2 )
by A17, A18;
(
(F . s) . a1 = ((OSHomQuot F) . i) . (OSClass (OSCng F),a1) &
(F . s) . a2 = ((OSHomQuot F) . i) . (OSClass (OSCng F),a2) )
by A1, A14, Def26;
then
[a1,a2] in MSCng F,
s
by A15, A17, A18, MSUALG_4:def 19;
then
[a1,a2] in (MSCng F) . s
by A1, MSUALG_4:def 20;
then
[a1,a2] in (OSCng F) . s
by A1, Def25;
hence
x1 = x2
by A19, Th13;
:: thesis: verum
end;
hence
(OSHomQuot F) . i is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
hence
OSHomQuot F is "1-1"
by MSUALG_3:1; :: thesis: OSHomQuot F is order-sorted
thus
OSHomQuot F is order-sorted
:: thesis: verumproof
let s1,
s2 be
Element of
S;
:: according to OSALG_3:def 1 :: thesis: ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) ) )
assume A20:
s1 <= s2
;
:: thesis: for b1 being set holds
( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) )
let a1 be
set ;
:: thesis: ( not a1 in dom ((OSHomQuot F) . s1) or ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 ) )
assume A21:
a1 in dom ((OSHomQuot F) . s1)
;
:: thesis: ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 )
reconsider sqa = the
Sorts of
(QuotOSAlg U1,(OSCng F)) as
OrderSortedSet of ;
reconsider S1O = the
Sorts of
U1 as
OrderSortedSet of
by OSALG_1:17;
A22:
S1O . s1 c= S1O . s2
by A20, OSALG_1:def 18;
A23:
(
dom ((OSHomQuot F) . s1) = the
Sorts of
(QuotOSAlg U1,(OSCng F)) . s1 &
dom ((OSHomQuot F) . s2) = the
Sorts of
(QuotOSAlg U1,(OSCng F)) . s2 )
by FUNCT_2:def 1;
sqa . s1 c= sqa . s2
by A20, OSALG_1:def 18;
hence
a1 in dom ((OSHomQuot F) . s2)
by A21, A23;
:: thesis: ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1
a1 in (OSClass (OSCng F)) . s1
by A21;
then
a1 in OSClass (OSCng F),
s1
by Def13;
then consider x being
set such that A24:
x in the
Sorts of
U1 . s1
and A25:
a1 = Class (CompClass (OSCng F),(CComp s1)),
x
by Def12;
reconsider x1 =
x as
Element of the
Sorts of
U1 . s1 by A24;
reconsider x2 =
x as
Element of the
Sorts of
U1 . s2 by A22, A24;
reconsider s3 =
s1,
s4 =
s2 as
Element of
S ;
x1 in dom (F . s3)
by A24, FUNCT_2:def 1;
then A26:
(
x1 in dom (F . s4) &
(F . s3) . x1 = (F . s4) . x1 )
by A1, A20, OSALG_3:def 1;
A27:
a1 = OSClass (OSCng F),
x2
by A20, A25, Th5;
thus ((OSHomQuot F) . s1) . a1 =
(OSHomQuot F,s1) . (OSClass (OSCng F),x1)
by A25, Def27
.=
(F . s2) . x1
by A1, A26, Def26
.=
(OSHomQuot F,s2) . (OSClass (OSCng F),x2)
by A1, Def26
.=
((OSHomQuot F) . s2) . a1
by A27, Def27
;
:: thesis: verum
end;