let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A
let A be non-empty MSAlgebra over S; for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A
let X9 be Subset of (CongrLatt A); "\/" (X9,(EqRelLatt the Sorts of A)) is MSCongruence of A
set M = the Sorts of A;
set E = EqRelLatt the Sorts of A;
the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A)
by NAT_LAT:def 12;
then reconsider X = X9 as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1;
reconsider V = "\/" (X,(EqRelLatt the Sorts of A)) as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;
reconsider V = V as ManySortedRelation of A ;
reconsider V = V as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in V . s1 holds
[(t . a),(t . b)] in V . s2
proof
let s1,
s2 be
SortSymbol of
S;
for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in V . s1 holds
[(t . a),(t . b)] in V . s2let t be
Function;
( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in V . s1 holds
[(t . a),(t . b)] in V . s2 )
assume A1:
t is_e.translation_of A,
s1,
s2
;
for a, b being set st [a,b] in V . s1 holds
[(t . a),(t . b)] in V . s2
then reconsider t9 =
t as
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) by MSUALG_6:11;
let a,
b be
set ;
( [a,b] in V . s1 implies [(t . a),(t . b)] in V . s2 )
assume A2:
[a,b] in V . s1
;
[(t . a),(t . b)] in V . s2
then A3:
a in the
Sorts of
A . s1
by ZFMISC_1:87;
A4:
b in the
Sorts of
A . s1
by A2, ZFMISC_1:87;
then A5:
t9 . b in the
Sorts of
A . s2
by FUNCT_2:5;
[a,b] in "\/" (EqRelSet (X,s1))
by A2, Th17;
then consider f being
FinSequence such that A6:
1
<= len f
and A7:
a = f . 1
and A8:
b = f . (len f)
and A9:
for
i being
Nat st 1
<= i &
i < len f holds
[(f . i),(f . (i + 1))] in union (EqRelSet (X,s1))
by A3, A4, Th10;
A10:
ex
g being
FinSequence st
( 1
<= len g &
t . a = g . 1 &
t . b = g . (len g) & ( for
i being
Nat st 1
<= i &
i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) )
proof
deffunc H1(
set )
-> set =
t . (f . $1);
consider g being
FinSequence such that A11:
(
len g = len f & ( for
k being
Nat st
k in dom g holds
g . k = H1(
k) ) )
from FINSEQ_1:sch 2();
take
g
;
( 1 <= len g & t . a = g . 1 & t . b = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) )
thus
1
<= len g
by A6, A11;
( t . a = g . 1 & t . b = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) )
A12:
dom g = Seg (len f)
by A11, FINSEQ_1:def 3;
1
in Seg (len f)
by A6, FINSEQ_1:1;
hence
g . 1
= t . a
by A7, A11, A12;
( t . b = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet (X,s2)) ) )
len g in Seg (len f)
by A6, A11, FINSEQ_1:1;
hence
g . (len g) = t . b
by A8, A11, A12;
for i being Nat st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet (X,s2))
let j be
Nat;
( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in union (EqRelSet (X,s2)) )
assume that A13:
1
<= j
and A14:
j < len g
;
[(g . j),(g . (j + 1))] in union (EqRelSet (X,s2))
A15:
1
<= j + 1
by A13, NAT_1:13;
[(f . j),(f . (j + 1))] in union (EqRelSet (X,s1))
by A9, A11, A13, A14;
then consider Z being
set such that A16:
[(f . j),(f . (j + 1))] in Z
and A17:
Z in EqRelSet (
X,
s1)
by TARSKI:def 4;
consider Eq being
Equivalence_Relation of the
Sorts of
A such that A18:
Z = Eq . s1
and A19:
Eq in X
by A17, Def3;
reconsider Eq =
Eq as
ManySortedRelation of
A ;
reconsider Eq =
Eq as
MSEquivalence-like ManySortedRelation of
A by MSUALG_4:def 3;
Eq is
MSCongruence of
A
by A19, MSUALG_5:def 6;
then reconsider Eq =
Eq as
MSEquivalence-like compatible ManySortedRelation of
A by MSUALG_6:27;
ex
W being
set st
(
[(t . (f . j)),(t . (f . (j + 1)))] in W &
W in EqRelSet (
X,
s2) )
then A20:
[(t . (f . j)),(t . (f . (j + 1)))] in union (EqRelSet (X,s2))
by TARSKI:def 4;
j + 1
<= len f
by A11, A14, NAT_1:13;
then A21:
j + 1
in Seg (len f)
by A15, FINSEQ_1:1;
j in Seg (len f)
by A11, A13, A14, FINSEQ_1:1;
then
g . j = t . (f . j)
by A11, A12;
hence
[(g . j),(g . (j + 1))] in union (EqRelSet (X,s2))
by A11, A12, A20, A21;
verum
end;
t9 . a in the
Sorts of
A . s2
by A3, FUNCT_2:5;
then
[(t . a),(t . b)] in "\/" (EqRelSet (X,s2))
by A5, A10, Th10;
hence
[(t . a),(t . b)] in V . s2
by Th17;
verum
end;
then reconsider V = V as MSEquivalence-like invariant ManySortedRelation of A by MSUALG_6:def 8;
V is compatible
;
hence
"\/" (X9,(EqRelLatt the Sorts of A)) is MSCongruence of A
by MSUALG_6:27; verum