let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of S; :: thesis: for X being Subset of (CongrLatt A) holds "\/" X,(EqRelLatt the Sorts of A) is MSCongruence of A
let X' be Subset of (CongrLatt A); :: thesis: "\/" X',(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 16;
then reconsider X = X' 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 5;
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;
:: thesis: 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;
:: thesis: ( 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
;
:: thesis: for a, b being set st [a,b] in V . s1 holds
[(t . a),(t . b)] in V . s2
let a,
b be
set ;
:: thesis: ( [a,b] in V . s1 implies [(t . a),(t . b)] in V . s2 )
assume A2:
[a,b] in V . s1
;
:: thesis: [(t . a),(t . b)] in V . s2
then A3:
[a,b] in "\/" (EqRelSet X,s1)
by Th17;
A4:
(
a in the
Sorts of
A . s1 &
b in the
Sorts of
A . s1 )
by A2, ZFMISC_1:106;
then consider f being
FinSequence such that A5:
( 1
<= len f &
a = f . 1 &
b = f . (len f) & ( for
i being
Element of
NAT st 1
<= i &
i < len f holds
[(f . i),(f . (i + 1))] in union (EqRelSet X,s1) ) )
by A3, Th10;
reconsider t' =
t as
Function of
(the Sorts of A . s1),
(the Sorts of A . s2) by A1, MSUALG_6:11;
A6:
(
t' . a in the
Sorts of
A . s2 &
t' . b in the
Sorts of
A . s2 )
by A4, FUNCT_2:7;
ex
g being
FinSequence st
( 1
<= len g &
t . a = g . 1 &
t . b = g . (len g) & ( for
i being
Element of
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 A7:
(
len g = len f & ( for
k being
Nat st
k in dom g holds
g . k = H1(
k) ) )
from FINSEQ_1:sch 2();
A8:
dom g = Seg (len f)
by A7, FINSEQ_1:def 3;
take
g
;
:: thesis: ( 1 <= len g & t . a = g . 1 & t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet X,s2) ) )
thus
1
<= len g
by A5, A7;
:: thesis: ( t . a = g . 1 & t . b = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet X,s2) ) )
1
in Seg (len f)
by A5, FINSEQ_1:3;
hence
g . 1
= t . a
by A5, A7, A8;
:: thesis: ( t . b = g . (len g) & ( for i being Element of 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 A5, A7, FINSEQ_1:3;
hence
g . (len g) = t . b
by A5, A7, A8;
:: thesis: for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in union (EqRelSet X,s2)
let j be
Element of
NAT ;
:: thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in union (EqRelSet X,s2) )
assume A9:
( 1
<= j &
j < len g )
;
:: thesis: [(g . j),(g . (j + 1))] in union (EqRelSet X,s2)
then
[(f . j),(f . (j + 1))] in union (EqRelSet X,s1)
by A5, A7;
then consider Z being
set such that A10:
(
[(f . j),(f . (j + 1))] in Z &
Z in EqRelSet X,
s1 )
by TARSKI:def 4;
consider Eq being
Equivalence_Relation of the
Sorts of
A such that A11:
(
Z = Eq . s1 &
Eq in X )
by A10, Def3;
reconsider Eq =
Eq as
ManySortedRelation of
A ;
reconsider Eq =
Eq as
MSEquivalence-like ManySortedRelation of
A by MSUALG_4:def 5;
Eq is
MSCongruence of
A
by A11, 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 A12:
[(t . (f . j)),(t . (f . (j + 1)))] in union (EqRelSet X,s2)
by TARSKI:def 4;
j in Seg (len f)
by A7, A9, FINSEQ_1:3;
then A13:
g . j = t . (f . j)
by A7, A8;
( 1
<= j + 1 &
j + 1
<= len f )
by A7, A9, NAT_1:13;
then
j + 1
in Seg (len f)
by FINSEQ_1:3;
hence
[(g . j),(g . (j + 1))] in union (EqRelSet X,s2)
by A7, A12, A13, A8;
:: thesis: verum
end;
then
[(t . a),(t . b)] in "\/" (EqRelSet X,s2)
by A6, Th10;
hence
[(t . a),(t . b)] in V . s2
by Th17;
:: thesis: verum
end;
then reconsider V = V as MSEquivalence-like invariant ManySortedRelation of A by MSUALG_6:def 8;
V is compatible
;
hence
"\/" X',(EqRelLatt the Sorts of A) is MSCongruence of A
by MSUALG_6:27; :: thesis: verum