:: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras
:: by Ewa Burakowska
::
:: Received April 25, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users

registration

let I be set ;
let X be ManySortedSet of I;
let Y be V8() ManySortedSet of I;

cluster X (\/) Y -> V8() ;

coherence
X (\/) Y is non-empty

proof end;

cluster Y (\/) X -> V8() ;

coherence
Y (\/) X is non-empty ;

end;

theorem Th1: :: MSUALG_2:1

for I being non empty set
for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X (/\) Y) * i) = (product (X * i)) /\ (product (Y * i))

proof end;

definition

let S be non empty ManySortedSign ;
let U0 be MSAlgebra over S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;

end;

definition

let S be non empty ManySortedSign ;
let IT be SortSymbol of S;

attr IT is with_const_op means :: MSUALG_2:def 1
ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT );

end;

:: deftheorem defines with_const_op MSUALG_2:def 1 :
for S being non empty ManySortedSign
for IT being SortSymbol of S holds
( IT is with_const_op iff ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT ) );

definition

let IT be non empty ManySortedSign ;

attr IT is all-with_const_op means :Def2: :: MSUALG_2:def 2
for s being SortSymbol of IT holds s is with_const_op ;

end;

:: deftheorem Def2 defines all-with_const_op MSUALG_2:def 2 :
for IT being non empty ManySortedSign holds
( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op );

registration

let A be non empty set ;
let B be set ;
let a be Function of B,(A *);
let r be Function of B,A;

cluster ManySortedSign(# A,B,a,r #) -> non empty ;

coherence
not ManySortedSign(# A,B,a,r #) is empty ;

end;

registration

cluster non empty non void V63() strict all-with_const_op for ManySortedSign ;

existence
ex b₁ being non empty ManySortedSign st
( not b₁ is void & b₁ is all-with_const_op & b₁ is strict )

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let s be SortSymbol of S;

func Constants (U0,s) -> Subset of ( the Sorts of U0 . s) means :Def3: :: MSUALG_2:def 3
ex A being non empty set st
( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) if the Sorts of U0 . s <> {}
otherwise it = {} ;

existence
( ( the Sorts of U0 . s <> {} implies ex b₁ being Subset of ( the Sorts of U0 . s) ex A being non empty set st
( A = the Sorts of U0 . s & b₁ = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) & ( not the Sorts of U0 . s <> {} implies ex b₁ being Subset of ( the Sorts of U0 . s) st b₁ = {} ) )

proof end;

correctness
consistency
for b₁ being Subset of ( the Sorts of U0 . s) holds verum;
uniqueness
for b₁, b₂ being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} & ex A being non empty set st
( A = the Sorts of U0 . s & b₁ = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) & ex A being non empty set st
( A = the Sorts of U0 . s & b₂ = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) implies b₁ = b₂ ) & ( not the Sorts of U0 . s <> {} & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );
;

end;

:: deftheorem Def3 defines Constants MSUALG_2:def 3 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for s being SortSymbol of S
for b₄ being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b₄ = Constants (U0,s) iff ex A being non empty set st
( A = the Sorts of U0 . s & b₄ = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b₄ = Constants (U0,s) iff b₄ = {} ) ) );

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

func Constants U0 -> MSSubset of U0 means :Def4: :: MSUALG_2:def 4
for s being SortSymbol of S holds it . s = Constants (U0,s);

existence
ex b₁ being MSSubset of U0 st
for s being SortSymbol of S holds b₁ . s = Constants (U0,s)

proof end;

uniqueness
for b₁, b₂ being MSSubset of U0 st ( for s being SortSymbol of S holds b₁ . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds b₂ . s = Constants (U0,s) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b₃ being MSSubset of U0 holds
( b₃ = Constants U0 iff for s being SortSymbol of S holds b₃ . s = Constants (U0,s) );

registration

let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let s be SortSymbol of S;

cluster Constants (U0,s) -> non empty ;

coherence
not Constants (U0,s) is empty

proof end;

end;

registration

let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

cluster Constants U0 -> V8() ;

coherence
Constants U0 is non-empty

proof end;

end;

::
:: Subalgebras of a Many Sorted Algebra.
::

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
let A be MSSubset of U0;

pred A is_closed_on o means :: MSUALG_2:def 5
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;

end;

:: deftheorem defines is_closed_on MSUALG_2:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S
for A being MSSubset of U0 holds
( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

attr A is opers_closed means :: MSUALG_2:def 6
for o being OperSymbol of S holds A is_closed_on o;

end;

:: deftheorem defines opers_closed MSUALG_2:def 6 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o );

theorem Th2: :: MSUALG_2:2

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
let A be MSSubset of U0;
assume A1: A is_closed_on o ;

func o /. A -> Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) equals :Def7: :: MSUALG_2:def 7
(Den (o,U0)) | (((A #) * the Arity of S) . o);

coherence
(Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

proof end;

end;

:: deftheorem Def7 defines /. MSUALG_2:def 7 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S
for A being MSSubset of U0 st A is_closed_on o holds
o /. A = (Den (o,U0)) | (((A #) * the Arity of S) . o);

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

func Opers (U0,A) -> ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S means :Def8: :: MSUALG_2:def 8
for o being OperSymbol of S holds it . o = o /. A;

existence
ex b₁ being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st
for o being OperSymbol of S holds b₁ . o = o /. A

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b₁ . o = o /. A ) & ( for o being OperSymbol of S holds b₂ . o = o /. A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Opers MSUALG_2:def 8 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b₄ being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds
( b₄ = Opers (U0,A) iff for o being OperSymbol of S holds b₄ . o = o /. A );

theorem Th3: :: MSUALG_2:3

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

proof end;

theorem Th4: :: MSUALG_2:4

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers (U0,B) = the Charact of U0

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

mode MSSubAlgebra of U0 -> MSAlgebra over S means :Def9: :: MSUALG_2:def 9
( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

existence
ex b₁ being MSAlgebra over S st
( the Sorts of b₁ is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b₁ holds
( B is opers_closed & the Charact of b₁ = Opers (U0,B) ) ) )

proof end;

end;

:: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def 9 :
for S being non empty non void ManySortedSign
for U0, b₃ being MSAlgebra over S holds
( b₃ is MSSubAlgebra of U0 iff ( the Sorts of b₃ is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b₃ holds
( B is opers_closed & the Charact of b₃ = Opers (U0,B) ) ) ) );

Lm1: for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0

proof end;

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

cluster strict for MSSubAlgebra of U0;

existence
ex b₁ being MSSubAlgebra of U0 st b₁ is strict

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

cluster MSAlgebra(# the Sorts of U0, the Charact of U0 #) -> non-empty ;

coherence
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is non-empty by MSUALG_1:def 3;

end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

cluster strict non-empty for MSSubAlgebra of U0;

existence
ex b₁ being MSSubAlgebra of U0 st
( b₁ is non-empty & b₁ is strict )

proof end;

end;

theorem :: MSUALG_2:5

for S being non empty non void ManySortedSign
for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds
U0 is MSSubAlgebra of U1

proof end;

theorem :: MSUALG_2:6

for S being non empty non void ManySortedSign
for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2

proof end;

theorem Th7: :: MSUALG_2:7

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

theorem Th8: :: MSUALG_2:8

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2

proof end;

theorem Th9: :: MSUALG_2:9

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

theorem Th10: :: MSUALG_2:10

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

proof end;

theorem :: MSUALG_2:11

for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10;

theorem :: MSUALG_2:12

for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()

proof end;

::
:: Many Sorted Subsets of a Many Sorted Algebra.
::

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

func SubSort A -> set means :Def10: :: MSUALG_2:def 10
for x being object holds
( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being object holds
( x in b₂ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines SubSort MSUALG_2:def 10 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b₄ being set holds
( b₄ = SubSort A iff for x being object holds
( x in b₄ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) );

Lm2: for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

proof end;

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

cluster SubSort A -> non empty ;

coherence
not SubSort A is empty by Lm2;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

func SubSort U0 -> set means :Def11: :: MSUALG_2:def 11
for x being object holds
( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) & ( for x being object holds
( x in b₂ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b₃ being set holds
( b₃ = SubSort U0 iff for x being object holds
( x in b₃ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) );

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

cluster SubSort U0 -> non empty ;

coherence
not SubSort U0 is empty

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let e be Element of SubSort U0;

func @ e -> MSSubset of U0 equals :: MSUALG_2:def 12
e;

coherence
e is MSSubset of U0 by Def11;

end;

:: deftheorem defines @ MSUALG_2:def 12 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for e being Element of SubSort U0 holds @ e = e;

theorem Th13: :: MSUALG_2:13

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )

proof end;

theorem Th14: :: MSUALG_2:14

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
let s be SortSymbol of S;

func SubSort (A,s) -> set means :Def13: :: MSUALG_2:def 13
for x being object holds
( x in it iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) & ( for x being object holds
( x in b₂ iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines SubSort MSUALG_2:def 13 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for s being SortSymbol of S
for b₅ being set holds
( b₅ = SubSort (A,s) iff for x being object holds
( x in b₅ iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) );

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
let s be SortSymbol of S;

cluster SubSort (A,s) -> non empty ;

coherence
not SubSort (A,s) is empty

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

func MSSubSort A -> MSSubset of U0 means :Def14: :: MSUALG_2:def 14
for s being SortSymbol of S holds it . s = meet (SubSort (A,s));

existence
ex b₁ being MSSubset of U0 st
for s being SortSymbol of S holds b₁ . s = meet (SubSort (A,s))

proof end;

uniqueness
for b₁, b₂ being MSSubset of U0 st ( for s being SortSymbol of S holds b₁ . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds b₂ . s = meet (SubSort (A,s)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines MSSubSort MSUALG_2:def 14 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, b₄ being MSSubset of U0 holds
( b₄ = MSSubSort A iff for s being SortSymbol of S holds b₄ . s = meet (SubSort (A,s)) );

theorem Th15: :: MSUALG_2:15

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds (Constants U0) (\/) A c= MSSubSort A

proof end;

theorem Th16: :: MSUALG_2:16

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 st (Constants U0) (\/) A is V8() holds
MSSubSort A is V8()

proof end;

theorem Th17: :: MSUALG_2:17

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

proof end;

theorem Th18: :: MSUALG_2:18

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o

proof end;

theorem Th19: :: MSUALG_2:19

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o

proof end;

theorem Th20: :: MSUALG_2:20

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )

proof end;

::
:: Operations on Subalgebras of a Many Sorted Algebra.
::

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;
assume A1: A is opers_closed ;

func U0 | A -> strict MSSubAlgebra of U0 equals :Def15: :: MSUALG_2:def 15
MSAlgebra(# A,(Opers (U0,A)) #);

coherence
MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0

proof end;

end;

:: deftheorem Def15 defines | MSUALG_2:def 15 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 st A is opers_closed holds
U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;

func U1 /\ U2 -> strict MSSubAlgebra of U0 means :Def16: :: MSUALG_2:def 16
( the Sorts of it = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

existence
ex b₁ being strict MSSubAlgebra of U0 st
( the Sorts of b₁ = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b₁ holds
( B is opers_closed & the Charact of b₁ = Opers (U0,B) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict MSSubAlgebra of U0 st the Sorts of b₁ = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b₁ holds
( B is opers_closed & the Charact of b₁ = Opers (U0,B) ) ) & the Sorts of b₂ = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b₂ holds
( B is opers_closed & the Charact of b₂ = Opers (U0,B) ) ) holds
b₁ = b₂ by Th9;

end;

:: deftheorem Def16 defines /\ MSUALG_2:def 16 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b₅ being strict MSSubAlgebra of U0 holds
( b₅ = U1 /\ U2 iff ( the Sorts of b₅ = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b₅ holds
( B is opers_closed & the Charact of b₅ = Opers (U0,B) ) ) ) );

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let A be MSSubset of U0;

func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17
( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
it is MSSubAlgebra of U1 ) );

existence
ex b₁ being strict MSSubAlgebra of U0 st
( A is MSSubset of b₁ & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b₁ is MSSubAlgebra of U1 ) )

proof end;

uniqueness
for b₁, b₂ being strict MSSubAlgebra of U0 st A is MSSubset of b₁ & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b₁ is MSSubAlgebra of U1 ) & A is MSSubset of b₂ & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b₂ is MSSubAlgebra of U1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines GenMSAlg MSUALG_2:def 17 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b₄ being strict MSSubAlgebra of U0 holds
( b₄ = GenMSAlg A iff ( A is MSSubset of b₄ & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b₄ is MSSubAlgebra of U1 ) ) );

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let A be V8() MSSubset of U0;

cluster GenMSAlg A -> strict non-empty ;

coherence
GenMSAlg A is non-empty

proof end;

end;

theorem Th21: :: MSUALG_2:21

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

proof end;

theorem Th22: :: MSUALG_2:22

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

proof end;

theorem Th23: :: MSUALG_2:23

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let U1, U2 be MSSubAlgebra of U0;

func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18
for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
it = GenMSAlg A;

existence
ex b₁ being strict MSSubAlgebra of U0 st
for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₁ = GenMSAlg A

proof end;

uniqueness
for b₁, b₂ being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₁ = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₂ = GenMSAlg A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines "\/" MSUALG_2:def 18 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b₅ being strict MSSubAlgebra of U0 holds
( b₅ = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₅ = GenMSAlg A );

theorem Th24: :: MSUALG_2:24

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenMSAlg A) "\/" U1 = GenMSAlg B

proof end;

theorem Th25: :: MSUALG_2:25

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B

proof end;

theorem Th26: :: MSUALG_2:26

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

proof end;

theorem Th27: :: MSUALG_2:27

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

proof end;

theorem Th28: :: MSUALG_2:28

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

::
:: The Lattice of SubAlgebras of a Many Sorted Algebra.
::

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

func MSSub U0 -> set means :Def19: :: MSUALG_2:def 19
for x being object holds
( x in it iff x is strict MSSubAlgebra of U0 );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff x is strict MSSubAlgebra of U0 )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is strict MSSubAlgebra of U0 ) ) & ( for x being object holds
( x in b₂ iff x is strict MSSubAlgebra of U0 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines MSSub MSUALG_2:def 19 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b₃ being set holds
( b₃ = MSSub U0 iff for x being object holds
( x in b₃ iff x is strict MSSubAlgebra of U0 ) );

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

cluster MSSub U0 -> non empty ;

coherence
not MSSub U0 is empty

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

func MSAlg_join U0 -> BinOp of (MSSub U0) means :Def20: :: MSUALG_2:def 20
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 "\/" U2;

existence
ex b₁ being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 "\/" U2

proof end;

uniqueness
for b₁, b₂ being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 "\/" U2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines MSAlg_join MSUALG_2:def 20 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for b₃ being BinOp of (MSSub U0) holds
( b₃ = MSAlg_join U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₃ . (x,y) = U1 "\/" U2 );

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

func MSAlg_meet U0 -> BinOp of (MSSub U0) means :Def21: :: MSUALG_2:def 21
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . (x,y) = U1 /\ U2;

existence
ex b₁ being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 /\ U2

proof end;

uniqueness
for b₁, b₂ being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₁ . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 /\ U2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines MSAlg_meet MSUALG_2:def 21 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for b₃ being BinOp of (MSSub U0) holds
( b₃ = MSAlg_meet U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₃ . (x,y) = U1 /\ U2 );

theorem Th29: :: MSUALG_2:29

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative

proof end;

theorem Th30: :: MSUALG_2:30

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative

proof end;

theorem Th31: :: MSUALG_2:31

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative

proof end;

theorem Th32: :: MSUALG_2:32

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 22
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

coherence
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice

proof end;

end;

:: deftheorem defines MSSubAlLattice MSUALG_2:def 22 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

theorem Th33: :: MSUALG_2:33

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded

proof end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;

cluster MSSubAlLattice U0 -> strict bounded ;

coherence
MSSubAlLattice U0 is bounded by Th33;

end;

theorem :: MSUALG_2:34

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)

proof end;

theorem Th35: :: MSUALG_2:35

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Top (MSSubAlLattice U0) = GenMSAlg B

proof end;

theorem :: MSUALG_2:36

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

proof end;

theorem :: MSUALG_2:37

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

theorem :: MSUALG_2:38

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2;

theorem :: MSUALG_2:39

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds SubSort A c= SubSort U0

proof end;