let S be locally_directed OrderSortedSign; for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
let U1 be non-empty OSAlgebra of S; for R being OSCongruence of U1 holds
( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
let R be OSCongruence of U1; ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )
set F = OSNat_Hom (U1,R);
set QA = QuotOSAlg (U1,R);
set S1 = the Sorts of U1;
for o being Element of the carrier' of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
proof
let o be
Element of the
carrier' of
S;
( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) )
assume
Args (
o,
U1)
<> {}
;
for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
let x be
Element of
Args (
o,
U1);
((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 1;
then A1:
(((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o))
by MSAFREE:1;
A2:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
A3:
for
a being
object st
a in dom (the_arity_of o) holds
((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a
proof
let a be
object ;
( a in dom (the_arity_of o) implies ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a )
assume A4:
a in dom (the_arity_of o)
;
((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a
then reconsider n =
a as
Nat ;
set Fo =
OSNat_Hom (
U1,
R,
((the_arity_of o) /. n));
set s =
(the_arity_of o) /. n;
A5:
ex
z being
Element of the
Sorts of
U1 . ((the_arity_of o) /. n) st
(
z = x . n &
(R #_os x) . n = OSClass (
R,
z) )
by A4, Def13;
A6:
n in dom ( the Sorts of U1 * (the_arity_of o))
by A4, PARTFUN1:def 2;
then ( the Sorts of U1 * (the_arity_of o)) . n =
the
Sorts of
U1 . ((the_arity_of o) . n)
by FUNCT_1:12
.=
the
Sorts of
U1 . ((the_arity_of o) /. n)
by A4, PARTFUN1:def 6
;
then reconsider xn =
x . n as
Element of the
Sorts of
U1 . ((the_arity_of o) /. n) by A6, MSUALG_3:6;
thus ((OSNat_Hom (U1,R)) # x) . a =
((OSNat_Hom (U1,R)) . ((the_arity_of o) /. n)) . (x . n)
by A2, A4, MSUALG_3:def 6
.=
(OSNat_Hom (U1,R,((the_arity_of o) /. n))) . xn
by Def22
.=
(R #_os x) . a
by A5, Def21
;
verum
end;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then
rng the
ResultSort of
S c= dom the
Sorts of
U1
;
then
(
dom the
ResultSort of
S = the
carrier' of
S &
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S )
by FUNCT_2:def 1, RELAT_1:27;
then A7:
( 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 reconsider dx =
(Den (o,U1)) . x as
Element of the
Sorts of
U1 . (the_result_sort_of o) by MSUALG_1:def 5;
(
rng (Den (o,U1)) c= Result (
o,
U1) &
Result (
o,
U1)
= the
Sorts of
U1 . (the_result_sort_of o) )
by A7, MSUALG_1:def 5;
then
rng (Den (o,U1)) c= dom (OSQuotRes (R,o))
by A7, FUNCT_2:def 1;
then A8:
(
dom (Den (o,U1)) = Args (
o,
U1) &
dom ((OSQuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) )
by FUNCT_2:def 1, RELAT_1:27;
dom (OSClass R) = the
carrier of
S
by PARTFUN1:def 2;
then
(
dom (R #_os x) = dom ((OSClass R) * (the_arity_of o)) &
rng (the_arity_of o) c= dom (OSClass R) )
by CARD_3:9;
then
(
dom ((OSNat_Hom (U1,R)) # x) = dom (the_arity_of o) &
dom (R #_os x) = dom (the_arity_of o) )
by MSUALG_3:6, RELAT_1:27;
then A9:
(OSNat_Hom (U1,R)) # x = R #_os x
by A3, FUNCT_1:2;
Den (
o,
(QuotOSAlg (U1,R))) =
(OSQuotCharact R) . o
by MSUALG_1:def 6
.=
OSQuotCharact (
R,
o)
by Def19
;
then (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) =
((OSQuotRes (R,o)) * (Den (o,U1))) . x
by A1, A9, Def18
.=
(OSQuotRes (R,o)) . dx
by A8, FUNCT_1:12
.=
OSClass (
R,
dx)
by Def14
.=
(OSNat_Hom (U1,R,(the_result_sort_of o))) . dx
by Def21
.=
((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x)
by Def22
;
hence
((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x)
;
verum
end;
hence
OSNat_Hom (U1,R) is_homomorphism U1, QuotOSAlg (U1,R)
; MSUALG_3:def 8 ( OSNat_Hom (U1,R) is "onto" & OSNat_Hom (U1,R) is order-sorted )
for i being set st i in the carrier of S holds
rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i
proof
let i be
set ;
( i in the carrier of S implies rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i )
assume
i in the
carrier of
S
;
rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i
then reconsider s =
i as
Element of
S ;
reconsider f =
(OSNat_Hom (U1,R)) . i as
Function of
( the Sorts of U1 . s),
( the Sorts of (QuotOSAlg (U1,R)) . s) by PBOOLE:def 15;
A10:
dom f = the
Sorts of
U1 . s
by FUNCT_2:def 1;
A11:
the
Sorts of
(QuotOSAlg (U1,R)) . s = OSClass (
R,
s)
by Def11;
for
x being
object st
x in the
Sorts of
(QuotOSAlg (U1,R)) . i holds
x in rng f
proof
let x be
object ;
( x in the Sorts of (QuotOSAlg (U1,R)) . i implies x in rng f )
A12:
f = OSNat_Hom (
U1,
R,
s)
by Def22;
assume
x in the
Sorts of
(QuotOSAlg (U1,R)) . i
;
x in rng f
then consider a1 being
set such that A13:
a1 in the
Sorts of
U1 . s
and A14:
x = Class (
(CompClass (R,(CComp s))),
a1)
by A11, Def10;
reconsider a2 =
a1 as
Element of the
Sorts of
U1 . s by A13;
(
OSClass (
R,
a2)
= x &
f . a1 in rng f )
by A10, A13, A14, FUNCT_1:def 3;
hence
x in rng f
by A12, Def21;
verum
end;
then
the
Sorts of
(QuotOSAlg (U1,R)) . i c= rng f
;
hence
rng ((OSNat_Hom (U1,R)) . i) = the
Sorts of
(QuotOSAlg (U1,R)) . i
;
verum
end;
hence
OSNat_Hom (U1,R) is "onto"
; OSNat_Hom (U1,R) is order-sorted
thus
OSNat_Hom (U1,R) is order-sorted
verumproof
reconsider S2 = the
Sorts of
U1 as
OrderSortedSet of
S by OSALG_1:17;
let s1,
s2 be
Element of
S;
OSALG_3:def 1 ( not s1 <= s2 or for b1 being set holds
( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) ) )
assume A15:
s1 <= s2
;
for b1 being set holds
( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) )
A16:
S2 . s1 c= S2 . s2
by A15, OSALG_1:def 16;
let a1 be
set ;
( not a1 in dom ((OSNat_Hom (U1,R)) . s1) or ( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 ) )
assume A17:
a1 in dom ((OSNat_Hom (U1,R)) . s1)
;
( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 )
A18:
a1 in the
Sorts of
U1 . s1
by A17;
then reconsider b2 =
a1 as
Element of the
Sorts of
U1 . s2 by A16;
dom ((OSNat_Hom (U1,R)) . s2) = the
Sorts of
U1 . s2
by FUNCT_2:def 1;
hence
a1 in dom ((OSNat_Hom (U1,R)) . s2)
by A16, A18;
((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1
reconsider b1 =
a1 as
Element of the
Sorts of
U1 . s1 by A17;
thus ((OSNat_Hom (U1,R)) . s1) . a1 =
(OSNat_Hom (U1,R,s1)) . b1
by Def22
.=
OSClass (
R,
b1)
by Def21
.=
OSClass (
R,
b2)
by A15, Th4
.=
(OSNat_Hom (U1,R,s2)) . b2
by Def21
.=
((OSNat_Hom (U1,R)) . s2) . a1
by Def22
;
verum
end;