let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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); :: thesis: "/\" (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 B is empty ; :: thesis: "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
then reconsider B9 = B as empty Subset of (CongrLatt A) ;
for q being Element of (EqRelLatt the Sorts of A) st q in B9 holds
Top (EqRelLatt the Sorts of A) [= q ;
then A1: Top (EqRelLatt the Sorts of A) is_less_than B by LATTICE3:def 16;
for b being Element of (EqRelLatt the Sorts of A) st b is_less_than B holds
b [= Top (EqRelLatt the Sorts of A) by LATTICES:19;
then "/\" (B,(EqRelLatt the Sorts of A)) = Top (EqRelLatt the Sorts of A) by A1, LATTICE3:34
.= [| the Sorts of A, the Sorts of A|] by MSUALG_7:4 ;
hence "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A by MSUALG_5:18; :: thesis: verum
end;
suppose A2: not B is empty ; :: thesis: "/\" (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; :: thesis: 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); :: thesis: ( ( 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) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in d . (the_result_sort_of o)
A5: now :: thesis: for q being MSCongruence of A st q in B holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o)
let q be MSCongruence of A; :: thesis: ( q in B implies [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o) )
assume A6: q in B ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o)
now :: thesis: for n being Nat st n in dom x holds
[(x . n),(y . n)] in q . ((the_arity_of o) /. n)
let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in q . ((the_arity_of o) /. n) )
assume n in dom x ; :: thesis: [(x . n),(y . n)] in q . ((the_arity_of o) /. n)
then [(x . n),(y . n)] in d . ((the_arity_of o) /. n) by A4;
then A7: [(x . n),(y . n)] in m . ((the_arity_of o) /. n) by A2, MSUALG_7:10;
m c= q by A6, MSUALG_7:7;
then m . ((the_arity_of o) /. n) c= q . ((the_arity_of o) /. n) by PBOOLE:def 2;
hence [(x . n),(y . n)] in q . ((the_arity_of o) /. n) by A7; :: thesis: verum
end;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in q . (the_result_sort_of o) by MSUALG_4:def 4; :: thesis: verum
end;
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 :: thesis: for Y being set st Y in |:B1:| . (the_result_sort_of o) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in Y
let Y be set ; :: thesis: ( 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) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in Y
then 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; :: thesis: 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; :: thesis: verum
end;
hence "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A by MSUALG_4:def 4; :: thesis: verum
end;
end;