let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
let A be non-empty MSAlgebra over S; for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
set M = the Sorts of A;
set E = EqRelLatt the Sorts of A;
set C = CongrLatt A;
let B be Subset of (CongrLatt A); "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
set d9 = "/\" (B,(EqRelLatt the Sorts of A));
reconsider d = "/\" (B,(EqRelLatt the Sorts of A)) as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;
reconsider d = d as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A)
by NAT_LAT:def 12;
then reconsider B1 = B as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1;
reconsider B1 = B1 as SubsetFamily of [| the Sorts of A, the Sorts of A|] by MSUALG_7:5;
per cases
( B is empty or not B is empty )
;
suppose A2:
not
B is
empty
;
"/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
for
o being
OperSymbol of
S for
x,
y being
Element of
Args (
o,
A) st ( for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o)
proof
reconsider B19 =
B1 as non
empty SubsetFamily of
[| the Sorts of A, the Sorts of A|] by A2;
reconsider m =
meet |:B1:| as
Equivalence_Relation of the
Sorts of
A by A2, MSUALG_7:8;
let o be
OperSymbol of
S;
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o)let x,
y be
Element of
Args (
o,
A);
( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o) )
A3:
|:B19:| is
V2()
;
assume A4:
for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in d . ((the_arity_of o) /. n)
;
[((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o)
A8:
|:B1:| . (the_result_sort_of o) = { (x1 . (the_result_sort_of o)) where x1 is Element of Bool [| the Sorts of A, the Sorts of A|] : x1 in B }
by A2, CLOSURE2:14;
now for Y being set st Y in |:B1:| . (the_result_sort_of o) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in Ylet Y be
set ;
( Y in |:B1:| . (the_result_sort_of o) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in Y )assume
Y in |:B1:| . (the_result_sort_of o)
;
[((Den (o,A)) . x),((Den (o,A)) . y)] in Ythen consider z being
Element of
Bool [| the Sorts of A, the Sorts of A|] such that A9:
Y = z . (the_result_sort_of o)
and A10:
z in B
by A8;
reconsider z9 =
z as
MSCongruence of
A by A10, MSUALG_5:def 6;
[((Den (o,A)) . x),((Den (o,A)) . y)] in z9 . (the_result_sort_of o)
by A5, A10;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in Y
by A9;
verum end;
then
( ex
Q being
Subset-Family of
([| the Sorts of A, the Sorts of A|] . (the_result_sort_of o)) st
(
Q = |:B1:| . (the_result_sort_of o) &
m . (the_result_sort_of o) = Intersect Q ) &
[((Den (o,A)) . x),((Den (o,A)) . y)] in meet (|:B1:| . (the_result_sort_of o)) )
by A3, MSSUBFAM:def 1, SETFAM_1:def 1;
then
[((Den (o,A)) . x),((Den (o,A)) . y)] in m . (the_result_sort_of o)
by A3, SETFAM_1:def 9;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o)
by A2, MSUALG_7:10;
verum
end; hence
"/\" (
B,
(EqRelLatt the Sorts of A)) is
MSCongruence of
A
by MSUALG_4:def 4;
verum end; end;