:: MSUALG_2 semantic presentation
begin
registration
let I be set ;
let X be ManySortedSet of I;
let Y be V8() ManySortedSet of I;
clusterX \/ Y -> V8() ;
coherence
X \/ Y is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (X \/ Y) . i is empty )
assume A1: i in I ; ::_thesis: not (X \/ Y) . i is empty
then (X \/ Y) . i = (X . i) \/ (Y . i) by PBOOLE:def_4;
hence not (X \/ Y) . i is empty by A1; ::_thesis: verum
end;
clusterY \/ 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
let I be non empty set ; ::_thesis: for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))
let X, Y be ManySortedSet of I; ::_thesis: for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))
let i be Element of I * ; ::_thesis: product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))
A1: rng i c= I by FINSEQ_1:def_4;
dom X = I by PARTFUN1:def_2;
then A2: dom (X * i) = dom i by A1, RELAT_1:27;
dom (X /\ Y) = I by PARTFUN1:def_2;
then A3: dom ((X /\ Y) * i) = dom i by A1, RELAT_1:27;
dom Y = I by PARTFUN1:def_2;
then A4: dom (Y * i) = dom i by A1, RELAT_1:27;
thus product ((X /\ Y) * i) c= (product (X * i)) /\ (product (Y * i)) :: according to XBOOLE_0:def_10 ::_thesis: (product (X * i)) /\ (product (Y * i)) c= product ((X /\ Y) * i)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ((X /\ Y) * i) or x in (product (X * i)) /\ (product (Y * i)) )
assume x in product ((X /\ Y) * i) ; ::_thesis: x in (product (X * i)) /\ (product (Y * i))
then consider g being Function such that
A5: ( x = g & dom g = dom ((X /\ Y) * i) ) and
A6: for y being set st y in dom ((X /\ Y) * i) holds
g . y in ((X /\ Y) * i) . y by CARD_3:def_5;
for y being set st y in dom (Y * i) holds
g . y in (Y * i) . y
proof
let y be set ; ::_thesis: ( y in dom (Y * i) implies g . y in (Y * i) . y )
assume A7: y in dom (Y * i) ; ::_thesis: g . y in (Y * i) . y
then g . y in ((X /\ Y) * i) . y by A4, A3, A6;
then A8: g . y in (X /\ Y) . (i . y) by A4, A3, A7, FUNCT_1:12;
i . y in rng i by A4, A7, FUNCT_1:def_3;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A8, PBOOLE:def_5;
then g . y in Y . (i . y) by XBOOLE_0:def_4;
hence g . y in (Y * i) . y by A7, FUNCT_1:12; ::_thesis: verum
end;
then A9: x in product (Y * i) by A4, A3, A5, CARD_3:def_5;
for y being set st y in dom (X * i) holds
g . y in (X * i) . y
proof
let y be set ; ::_thesis: ( y in dom (X * i) implies g . y in (X * i) . y )
assume A10: y in dom (X * i) ; ::_thesis: g . y in (X * i) . y
then g . y in ((X /\ Y) * i) . y by A2, A3, A6;
then A11: g . y in (X /\ Y) . (i . y) by A2, A3, A10, FUNCT_1:12;
i . y in rng i by A2, A10, FUNCT_1:def_3;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A1, A11, PBOOLE:def_5;
then g . y in X . (i . y) by XBOOLE_0:def_4;
hence g . y in (X * i) . y by A10, FUNCT_1:12; ::_thesis: verum
end;
then x in product (X * i) by A2, A3, A5, CARD_3:def_5;
hence x in (product (X * i)) /\ (product (Y * i)) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (product (X * i)) /\ (product (Y * i)) or x in product ((X /\ Y) * i) )
assume A12: x in (product (X * i)) /\ (product (Y * i)) ; ::_thesis: x in product ((X /\ Y) * i)
then x in product (X * i) by XBOOLE_0:def_4;
then consider g being Function such that
A13: x = g and
A14: dom g = dom (X * i) and
A15: for y being set st y in dom (X * i) holds
g . y in (X * i) . y by CARD_3:def_5;
x in product (Y * i) by A12, XBOOLE_0:def_4;
then A16: ex h being Function st
( x = h & dom h = dom (Y * i) & ( for y being set st y in dom (Y * i) holds
h . y in (Y * i) . y ) ) by CARD_3:def_5;
for y being set st y in dom ((X /\ Y) * i) holds
g . y in ((X /\ Y) * i) . y
proof
let y be set ; ::_thesis: ( y in dom ((X /\ Y) * i) implies g . y in ((X /\ Y) * i) . y )
assume A17: y in dom ((X /\ Y) * i) ; ::_thesis: g . y in ((X /\ Y) * i) . y
then A18: i . y in rng i by A3, FUNCT_1:def_3;
g . y in (X * i) . y by A2, A3, A15, A17;
then A19: g . y in X . (i . y) by A2, A3, A17, FUNCT_1:12;
g . y in (Y * i) . y by A4, A3, A13, A16, A17;
then g . y in Y . (i . y) by A4, A3, A17, FUNCT_1:12;
then g . y in (X . (i . y)) /\ (Y . (i . y)) by A19, XBOOLE_0:def_4;
then g . y in (X /\ Y) . (i . y) by A1, A18, PBOOLE:def_5;
hence g . y in ((X /\ Y) * i) . y by A17, FUNCT_1:12; ::_thesis: verum
end;
hence x in product ((X /\ Y) * i) by A2, A3, A13, A14, CARD_3:def_5; ::_thesis: verum
end;
begin
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;
attrIT is with_const_op means :Def1: :: MSUALG_2:def 1
ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT );
end;
:: deftheorem Def1 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 ;
attrIT 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 V60() strict all-with_const_op for ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is all-with_const_op & b1 is strict )
proof
set x = the set ;
set C = { the set };
consider a being Function such that
A1: dom a = { the set } and
A2: rng a = {(<*> { the set })} by FUNCT_1:5;
rng a c= { the set } *
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng a or y in { the set } * )
assume y in rng a ; ::_thesis: y in { the set } *
then y = <*> { the set } by A2, TARSKI:def_1;
hence y in { the set } * by FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider a = a as Function of { the set },({ the set } *) by A1, FUNCT_2:def_1, RELSET_1:4;
consider r being Function such that
A3: dom r = { the set } and
A4: rng r = { the set } by FUNCT_1:5;
reconsider r = r as Function of { the set },{ the set } by A3, A4, FUNCT_2:def_1, RELSET_1:4;
set M = ManySortedSign(# { the set },{ the set },a,r #);
take ManySortedSign(# { the set },{ the set },a,r #) ; ::_thesis: ( not ManySortedSign(# { the set },{ the set },a,r #) is void & ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict )
thus not ManySortedSign(# { the set },{ the set },a,r #) is void ; ::_thesis: ( ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict )
for s being SortSymbol of ManySortedSign(# { the set },{ the set },a,r #) holds s is with_const_op
proof
reconsider o = the set as OperSymbol of ManySortedSign(# { the set },{ the set },a,r #) by TARSKI:def_1;
let s be SortSymbol of ManySortedSign(# { the set },{ the set },a,r #); ::_thesis: s is with_const_op
take o ; :: according to MSUALG_2:def_1 ::_thesis: ( the Arity of ManySortedSign(# { the set },{ the set },a,r #) . o = {} & the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s )
a . o in rng a by A1, FUNCT_1:def_3;
hence the Arity of ManySortedSign(# { the set },{ the set },a,r #) . o = {} by A2, TARSKI:def_1; ::_thesis: the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s
( s = the set & r . o in rng r ) by A3, FUNCT_1:def_3, TARSKI:def_1;
hence the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s by A4, TARSKI:def_1; ::_thesis: verum
end;
hence ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op by Def2; ::_thesis: ManySortedSign(# { the set },{ the set },a,r #) is strict
thus ManySortedSign(# { the set },{ the set },a,r #) is strict ; ::_thesis: verum
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 b1 being Subset of ( the Sorts of U0 . s) ex A being non empty set st
( A = the Sorts of U0 . s & b1 = { 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 b1 being Subset of ( the Sorts of U0 . s) st b1 = {} ) )
proof
hereby ::_thesis: ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {} )
assume the Sorts of U0 . s <> {} ; ::_thesis: ex E being Subset of ( the Sorts of U0 . s) ex A being non empty set st
( A = the Sorts of U0 . s & E = { 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)) ) } )
then reconsider A = the Sorts of U0 . s as non empty set ;
set E = { 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)) ) } ;
{ 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)) ) } c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { 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)) ) } or x in A )
assume x in { 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)) ) } ; ::_thesis: x in A
then ex w being Element of the Sorts of U0 . s st
( w = x & ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & w in rng (Den (o,U0)) ) ) ;
hence x in A ; ::_thesis: verum
end;
then reconsider E = { 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)) ) } as Subset of ( the Sorts of U0 . s) ;
take E = E; ::_thesis: ex A being non empty set st
( A = the Sorts of U0 . s & E = { 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)) ) } )
take A = A; ::_thesis: ( A = the Sorts of U0 . s & E = { 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)) ) } )
thus ( A = the Sorts of U0 . s & E = { 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)) ) } ) ; ::_thesis: verum
end;
assume the Sorts of U0 . s = {} ; ::_thesis: ex b1 being Subset of ( the Sorts of U0 . s) st b1 = {}
take {} ( the Sorts of U0 . s) ; ::_thesis: {} ( the Sorts of U0 . s) = {}
thus {} ( the Sorts of U0 . s) = {} ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of ( the Sorts of U0 . s) holds verum;
uniqueness
for b1, b2 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 & b1 = { 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 & b2 = { 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 b1 = b2 ) & ( not the Sorts of U0 . s <> {} & b1 = {} & b2 = {} implies b1 = b2 ) );
;
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 b4 being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff ex A being non empty set st
( A = the Sorts of U0 . s & b4 = { 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 ( b4 = Constants (U0,s) iff b4 = {} ) ) );
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 b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = Constants (U0,s)
proof
deffunc H1( SortSymbol of S) -> Subset of ( the Sorts of U0 . $1) = Constants (U0,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being SortSymbol of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
f c= the Sorts of U0
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or f . s c= the Sorts of U0 . s )
assume s in the carrier of S ; ::_thesis: f . s c= the Sorts of U0 . s
then reconsider s1 = s as SortSymbol of S ;
f . s1 = Constants (U0,s1) by A1;
hence f . s c= the Sorts of U0 . s ; ::_thesis: verum
end;
then reconsider f = f as MSSubset of U0 by PBOOLE:def_18;
take f ; ::_thesis: for s being SortSymbol of S holds f . s = Constants (U0,s)
thus for s being SortSymbol of S holds f . s = Constants (U0,s) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds b2 . s = Constants (U0,s) ) holds
b1 = b2
proof
let W1, W2 be MSSubset of U0; ::_thesis: ( ( for s being SortSymbol of S holds W1 . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds W2 . s = Constants (U0,s) ) implies W1 = W2 )
assume that
A2: for s being SortSymbol of S holds W1 . s = Constants (U0,s) and
A3: for s being SortSymbol of S holds W2 . s = Constants (U0,s) ; ::_thesis: W1 = W2
for s being set st s in the carrier of S holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S implies W1 . s = W2 . s )
assume s in the carrier of S ; ::_thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S ;
W1 . t = Constants (U0,t) by A2;
hence W1 . s = W2 . s by A3; ::_thesis: verum
end;
hence W1 = W2 by PBOOLE:3; ::_thesis: verum
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 b3 being MSSubset of U0 holds
( b3 = Constants U0 iff for s being SortSymbol of S holds b3 . 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
( dom {} = {} & rng {} = {} ) ;
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
s is with_const_op by Def2;
then consider o being OperSymbol of S such that
A1: the Arity of S . o = {} and
A2: the ResultSort of S . o = s by Def1;
A3: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then ( dom ( the Sorts of U0 #) = the carrier of S * & the Arity of S . o in rng the Arity of S ) by FUNCT_1:def_3, PARTFUN1:def_2;
then A4: o in dom (( the Sorts of U0 #) * the Arity of S) by A3, FUNCT_1:11;
Args (o,U0) = (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of U0 #) . ( the Arity of S . o) by A4, FUNCT_1:12
.= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1
.= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5
.= product ( the Sorts of U0 * a) by A1, MSUALG_1:def_1
.= {{}} by CARD_3:10 ;
then A5: {} in Args (o,U0) by TARSKI:def_1;
set f = Den (o,U0);
A6: rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def_19;
dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1;
then A7: (Den (o,U0)) . {} in rng (Den (o,U0)) by A5, FUNCT_1:def_3;
A8: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then ( dom the Sorts of U0 = the carrier of S & the ResultSort of S . o in rng the ResultSort of S ) by FUNCT_1:def_3, PARTFUN1:def_2;
then A9: o in dom ( the Sorts of U0 * the ResultSort of S) by A8, FUNCT_1:11;
Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U0 . s by A2, A9, FUNCT_1:12 ;
then reconsider a = (Den (o,U0)) . {} as Element of the Sorts of U0 . s by A6, A7;
ex A being non empty set st
( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3;
then a in Constants (U0,s) by A1, A2, A7;
hence not Constants (U0,s) is empty ; ::_thesis: verum
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
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
not_(Constants_U0)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S implies not (Constants U0) . i is empty )
assume i in the carrier of S ; ::_thesis: not (Constants U0) . i is empty
then reconsider s = i as SortSymbol of S ;
(Constants U0) . s = Constants (U0,s) by Def4;
hence not (Constants U0) . i is empty ; ::_thesis: verum
end;
hence Constants U0 is non-empty by PBOOLE:def_13; ::_thesis: verum
end;
end;
begin
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;
predA is_closed_on o means :Def5: :: MSUALG_2:def 5
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;
end;
:: deftheorem Def5 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;
attrA is opers_closed means :Def6: :: MSUALG_2:def 6
for o being OperSymbol of S holds A is_closed_on o;
end;
:: deftheorem Def6 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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: 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
let B0, B1 be MSSubset of U0; ::_thesis: ( B0 c= B1 implies ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o )
reconsider a = the Arity of S . o as Element of the carrier of S * ;
A1: rng a c= the carrier of S by FINSEQ_1:def_4;
A2: dom B0 = the carrier of S by PARTFUN1:def_2;
then A3: dom (B0 * a) = dom a by A1, RELAT_1:27;
assume A4: B0 c= B1 ; ::_thesis: ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o
A5: for x being set st x in dom (B0 * a) holds
(B0 * a) . x c= (B1 * a) . x
proof
let x be set ; ::_thesis: ( x in dom (B0 * a) implies (B0 * a) . x c= (B1 * a) . x )
assume A6: x in dom (B0 * a) ; ::_thesis: (B0 * a) . x c= (B1 * a) . x
then a . x in rng a by A3, FUNCT_1:def_3;
then B0 . (a . x) c= B1 . (a . x) by A4, A1, PBOOLE:def_2;
then (B0 * a) . x c= B1 . (a . x) by A3, A6, FUNCT_1:13;
hence (B0 * a) . x c= (B1 * a) . x by A3, A6, FUNCT_1:13; ::_thesis: verum
end;
A7: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then dom ((B0 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
then ((B0 #) * the Arity of S) . o = (B0 #) . a by A7, FUNCT_1:12;
then A8: ((B0 #) * the Arity of S) . o = product (B0 * a) by FINSEQ_2:def_5;
dom ((B1 #) * the Arity of S) = dom the Arity of S by A7, PARTFUN1:def_2;
then ((B1 #) * the Arity of S) . o = (B1 #) . a by A7, FUNCT_1:12;
then A9: ((B1 #) * the Arity of S) . o = product (B1 * a) by FINSEQ_2:def_5;
dom B1 = the carrier of S by PARTFUN1:def_2;
then dom (B1 * a) = dom a by A1, RELAT_1:27;
hence ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by A8, A9, A2, A1, A5, CARD_3:27, RELAT_1:27; ::_thesis: verum
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 ;
funco /. 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
set f = (Den (o,U0)) | (((A #) * the Arity of S) . o);
set B = the Sorts of U0;
A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
percases ( (A * the ResultSort of S) . o = {} or (A * the ResultSort of S) . o <> {} ) ;
supposeA3: (A * the ResultSort of S) . o = {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def5;
then A4: (Den (o,U0)) | (((A #) * the Arity of S) . o) = {} by A3;
now__::_thesis:_(Den_(o,U0))_|_(((A_#)_*_the_Arity_of_S)_._o)_is_Function_of_(((A_#)_*_the_Arity_of_S)_._o),((A_*_the_ResultSort_of_S)_._o)
percases ( ((A #) * the Arity of S) . o = {} or ((A #) * the Arity of S) . o <> {} ) ;
suppose ((A #) * the Arity of S) . o = {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A4, RELSET_1:12; ::_thesis: verum
end;
suppose ((A #) * the Arity of S) . o <> {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
thus (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A3, A4, FUNCT_2:def_1, RELSET_1:12; ::_thesis: verum
end;
end;
end;
hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) ; ::_thesis: verum
end;
supposeA5: (A * the ResultSort of S) . o <> {} ; ::_thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)
reconsider B0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
A6: A c= B0 by PBOOLE:def_18;
A7: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def5;
A c= the Sorts of U0 by PBOOLE:def_18;
then A . ( the ResultSort of S . o) c= the Sorts of U0 . ( the ResultSort of S . o) by PBOOLE:def_2;
then the Sorts of U0 . ( the ResultSort of S . o) <> {} by A2, A5, FUNCT_1:13;
then ( the Sorts of U0 * the ResultSort of S) . o <> {} by A2, FUNCT_1:13;
then Result (o,U0) <> {} by MSUALG_1:def_5;
then dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1
.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4 ;
then dom ((Den (o,U0)) | (((A #) * the Arity of S) . o)) = ((( the Sorts of U0 #) * the Arity of S) . o) /\ (((A #) * the Arity of S) . o) by RELAT_1:61
.= ((A #) * the Arity of S) . o by A6, Th2, XBOOLE_1:28 ;
hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A7, FUNCT_2:2; ::_thesis: verum
end;
end;
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 b1 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = o /. A
proof
set B = (A #) * the Arity of S;
set C = A * the ResultSort of S;
defpred S1[ set , set ] means for o being OperSymbol of S st o = $1 holds
$2 = o /. A;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider o = x as OperSymbol of S ;
take o /. A ; ::_thesis: S1[x,o /. A]
thus S1[x,o /. A] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then reconsider o = x as OperSymbol of S by A2;
f . o = o /. A by A2;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
for x being set st x in the carrier' of S holds
f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) )
assume x in the carrier' of S ; ::_thesis: f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)
then reconsider o = x as OperSymbol of S ;
f . o = o /. A by A2;
hence f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S by PBOOLE:def_15;
take f ; ::_thesis: for o being OperSymbol of S holds f . o = o /. A
let o be OperSymbol of S; ::_thesis: f . o = o /. A
thus f . o = o /. A by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = o /. A ) & ( for o being OperSymbol of S holds b2 . o = o /. A ) holds
b1 = b2
proof
let f1, f2 be ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f1 . o = o /. A ) & ( for o being OperSymbol of S holds f2 . o = o /. A ) implies f1 = f2 )
assume that
A3: for o being OperSymbol of S holds f1 . o = o /. A and
A4: for o being OperSymbol of S holds f2 . o = o /. A ; ::_thesis: f1 = f2
for x being set st x in the carrier' of S holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies f1 . x = f2 . x )
assume x in the carrier' of S ; ::_thesis: f1 . x = f2 . x
then reconsider o1 = x as OperSymbol of S ;
f1 . o1 = o1 /. A by A3;
hence f1 . x = f2 . x by A4; ::_thesis: verum
end;
hence f1 = f2 by PBOOLE:3; ::_thesis: verum
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 b4 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds
( b4 = Opers (U0,A) iff for o being OperSymbol of S holds b4 . 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
let S be non empty non void ManySortedSign ; ::_thesis: 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) ) )
let U0 be MSAlgebra over S; ::_thesis: 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) ) )
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) ) )
assume A1: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )
thus A2: B is opers_closed ::_thesis: for o being OperSymbol of S holds o /. B = Den (o,U0)
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o
Result (o,U0) = (B * the ResultSort of S) . o by A1, MSUALG_1:def_5;
hence rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by RELAT_1:def_19; :: according to MSUALG_2:def_5 ::_thesis: verum
end;
let o be OperSymbol of S; ::_thesis: o /. B = Den (o,U0)
B is_closed_on o by A2, Def6;
then A3: o /. B = (Den (o,U0)) | (((B #) * the Arity of S) . o) by Def7;
percases ( (B * the ResultSort of S) . o = {} or (B * the ResultSort of S) . o <> {} ) ;
suppose (B * the ResultSort of S) . o = {} ; ::_thesis: o /. B = Den (o,U0)
then Result (o,U0) = {} by A1, MSUALG_1:def_5;
then Den (o,U0) = {} ;
hence o /. B = Den (o,U0) by A3; ::_thesis: verum
end;
suppose (B * the ResultSort of S) . o <> {} ; ::_thesis: o /. B = Den (o,U0)
then Result (o,U0) <> {} by A1, MSUALG_1:def_5;
then A4: dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1;
Args (o,U0) = ((B #) * the Arity of S) . o by A1, MSUALG_1:def_4;
hence o /. B = Den (o,U0) by A3, A4, RELAT_1:68; ::_thesis: verum
end;
end;
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers (U0,B) = the Charact of U0
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Opers (U0,B) = the Charact of U0 )
set f1 = the Charact of U0;
set f2 = Opers (U0,B);
assume A1: B = the Sorts of U0 ; ::_thesis: Opers (U0,B) = the Charact of U0
for x being set st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U0,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U0,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U0,B)) . x
then reconsider o1 = x as OperSymbol of S ;
( the Charact of U0 . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6;
hence the Charact of U0 . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum
end;
hence Opers (U0,B) = the Charact of U0 by PBOOLE:3; ::_thesis: verum
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 b1 being MSAlgebra over S st
( the Sorts of b1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) )
proof
take U1 = U0; ::_thesis: ( the Sorts of U1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) )
thus the Sorts of U1 is MSSubset of U0 by PBOOLE:def_18; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) )
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) )
set f1 = the Charact of U1;
set f2 = Opers (U0,B);
assume A1: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
hence B is opers_closed by Th3; ::_thesis: the Charact of U1 = Opers (U0,B)
for x being set st x in the carrier' of S holds
the Charact of U1 . x = (Opers (U0,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U0,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U0,B)) . x
then reconsider o1 = x as OperSymbol of S ;
( the Charact of U1 . o1 = Den (o1,U1) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6;
hence the Charact of U1 . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum
end;
hence the Charact of U1 = Opers (U0,B) by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def_9_:_
for S being non empty non void ManySortedSign
for U0, b3 being MSAlgebra over S holds
( b3 is MSSubAlgebra of U0 iff ( the Sorts of b3 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b3 holds
( B is opers_closed & the Charact of b3 = 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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0
let U0 be MSAlgebra over S; ::_thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0
reconsider A = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSAlgebra over S ;
now__::_thesis:_(_the_Sorts_of_A_is_MSSubset_of_U0_&_(_for_B_being_MSSubset_of_U0_st_B_=_the_Sorts_of_A_holds_
(_B_is_opers_closed_&_the_Charact_of_A_=_Opers_(U0,B)_)_)_)
thus the Sorts of A is MSSubset of U0 by PBOOLE:def_18; ::_thesis: for B being MSSubset of U0 st B = the Sorts of A holds
( B is opers_closed & the Charact of A = Opers (U0,B) )
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of A implies ( B is opers_closed & the Charact of A = Opers (U0,B) ) )
set f1 = the Charact of A;
set f2 = Opers (U0,B);
assume A1: B = the Sorts of A ; ::_thesis: ( B is opers_closed & the Charact of A = Opers (U0,B) )
hence B is opers_closed by Th3; ::_thesis: the Charact of A = Opers (U0,B)
for x being set st x in the carrier' of S holds
the Charact of A . x = (Opers (U0,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of A . x = (Opers (U0,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of A . x = (Opers (U0,B)) . x
then reconsider o1 = x as Element of the carrier' of S ;
( the Charact of A . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def_6;
hence the Charact of A . x = (Opers (U0,B)) . x by A1, Th3; ::_thesis: verum
end;
hence the Charact of A = Opers (U0,B) by PBOOLE:3; ::_thesis: verum
end;
hence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Def9; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
cluster strict for MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st b1 is strict
proof
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;
hence ex b1 being MSSubAlgebra of U0 st b1 is strict ; ::_thesis: verum
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 b1 being MSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict )
proof
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;
hence ex b1 being MSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict ) ; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0, U1 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) implies U0 is MSSubAlgebra of U1 )
assume A1: MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ; ::_thesis: U0 is MSSubAlgebra of U1
hence the Sorts of U0 is MSSubset of U1 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U1 st B = the Sorts of U0 holds
( B is opers_closed & the Charact of U0 = Opers (U1,B) )
let B be MSSubset of U1; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U1,B) ) )
set f1 = the Charact of U0;
set f2 = Opers (U1,B);
assume A2: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & the Charact of U0 = Opers (U1,B) )
thus B is opers_closed ::_thesis: the Charact of U0 = Opers (U1,B)
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o
(Den (o,U1)) | (((B #) * the Arity of S) . o) c= Den (o,U1) by RELAT_1:59;
then ( rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= rng (Den (o,U1)) & rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = (B * the ResultSort of S) . o ) by A1, A2, RELAT_1:11, RELAT_1:def_19, MSUALG_1:def_5;
hence rng ((Den (o,U1)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by XBOOLE_1:1; :: according to MSUALG_2:def_5 ::_thesis: verum
end;
for x being set st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U1,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U1,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U1,B)) . x
then reconsider o1 = x as OperSymbol of S ;
thus the Charact of U0 . x = (Opers (U1,B)) . x by A1, A2, Th4; ::_thesis: verum
end;
hence the Charact of U0 = Opers (U1,B) by PBOOLE:3; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0, U1, U2 be MSAlgebra over S; ::_thesis: ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 )
assume that
A1: U0 is MSSubAlgebra of U1 and
A2: U1 is MSSubAlgebra of U2 ; ::_thesis: U0 is MSSubAlgebra of U2
reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def9;
A3: B0 is opers_closed by A1, Def9;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A2, Def9;
A4: B1 is opers_closed by A2, Def9;
reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def_18;
A5: the Charact of U1 = Opers (U2,B1) by A2, Def9;
the Sorts of U0 is MSSubset of U1 by A1, Def9;
then A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U2 by A2, Def9;
then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_18;
then the Sorts of U0 c= the Sorts of U2 by A6, PBOOLE:13;
hence the Sorts of U0 is MSSubset of U2 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U2 st B = the Sorts of U0 holds
( B is opers_closed & the Charact of U0 = Opers (U2,B) )
let B be MSSubset of U2; ::_thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U2,B) ) )
set O = the Charact of U0;
set P = Opers (U2,B);
A7: the Charact of U0 = Opers (U1,B0) by A1, Def9;
assume A8: B = the Sorts of U0 ; ::_thesis: ( B is opers_closed & the Charact of U0 = Opers (U2,B) )
A9: for o being OperSymbol of S holds B is_closed_on o
proof
let o be OperSymbol of S; ::_thesis: B is_closed_on o
A10: B0 is_closed_on o by A3, Def6;
A11: B1 is_closed_on o by A4, Def6;
A12: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def_6
.= o /. B1 by Def8
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A11, Def7 ;
A13: ((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o by A6, Th2;
Den (o,U0) = (Opers (U1,B0)) . o by A7, MSUALG_1:def_6
.= o /. B0 by Def8
.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A10, A12, Def7
.= (Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o)) by RELAT_1:71
.= (Den (o,U2)) | (((B0 #) * the Arity of S) . o) by A13, XBOOLE_1:28 ;
then rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= Result (o,U0) by RELAT_1:def_19;
then rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5;
hence B is_closed_on o by A8, Def5; ::_thesis: verum
end;
hence B is opers_closed by Def6; ::_thesis: the Charact of U0 = Opers (U2,B)
for x being set st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U2,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U2,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U0 . x = (Opers (U2,B)) . x
then reconsider o = x as OperSymbol of S ;
A14: B0 is_closed_on o by A3, Def6;
A15: B1 is_closed_on o by A4, Def6;
A16: Den (o,U1) = (Opers (U2,B1)) . o by A5, MSUALG_1:def_6
.= o /. B1 by Def8
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A15, Def7 ;
thus the Charact of U0 . x = o /. B0 by A7, Def8
.= ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o) by A14, A16, Def7
.= (Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o)) by RELAT_1:71
.= (Den (o,U2)) | (((B #) * the Arity of S) . o) by A6, A8, Th2, XBOOLE_1:28
.= o /. B by A9, Def7
.= (Opers (U2,B)) . x by Def8 ; ::_thesis: verum
end;
hence the Charact of U0 = Opers (U2,B) by PBOOLE:3; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U1, U2 be MSAlgebra over S; ::_thesis: ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
assume that
A1: U1 is MSSubAlgebra of U2 and
A2: U2 is MSSubAlgebra of U1 ; ::_thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
the Sorts of U2 is MSSubset of U1 by A2, Def9;
then A3: the Sorts of U2 c= the Sorts of U1 by PBOOLE:def_18;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def9;
A4: the Charact of U1 = Opers (U2,B1) by A1, Def9;
reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2, Def9;
A5: the Charact of U2 = Opers (U1,B2) by A2, Def9;
the Sorts of U1 is MSSubset of U2 by A1, Def9;
then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_18;
then A6: the Sorts of U1 = the Sorts of U2 by A3, PBOOLE:146;
set O = the Charact of U1;
set P = Opers (U1,B2);
A7: B1 is opers_closed by A1, Def9;
for x being set st x in the carrier' of S holds
the Charact of U1 . x = (Opers (U1,B2)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U1,B2)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U1,B2)) . x
then reconsider o = x as OperSymbol of S ;
A8: Args (o,U2) = ((B2 #) * the Arity of S) . o by MSUALG_1:def_4;
A9: B1 is_closed_on o by A7, Def6;
thus the Charact of U1 . x = o /. B1 by A4, Def8
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A9, Def7
.= Den (o,U2) by A6, A8, RELSET_1:19
.= (Opers (U1,B2)) . x by A5, MSUALG_1:def_6 ; ::_thesis: verum
end;
hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A6, A5, PBOOLE:3; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2
let U1, U2 be MSSubAlgebra of U0; ::_thesis: ( the Sorts of U1 c= the Sorts of U2 implies U1 is MSSubAlgebra of U2 )
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by Def9;
assume A1: the Sorts of U1 c= the Sorts of U2 ; ::_thesis: U1 is MSSubAlgebra of U2
hence the Sorts of U1 is MSSubset of U2 by PBOOLE:def_18; :: according to MSUALG_2:def_9 ::_thesis: for B being MSSubset of U2 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U2,B) )
let B be MSSubset of U2; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U2,B) ) )
A2: B1 is opers_closed by Def9;
set O = the Charact of U1;
set P = Opers (U2,B);
A3: the Charact of U1 = Opers (U0,B1) by Def9;
A4: B2 is opers_closed by Def9;
A5: the Charact of U2 = Opers (U0,B2) by Def9;
assume A6: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U2,B) )
A7: for o being OperSymbol of S holds B is_closed_on o
proof
let o be OperSymbol of S; ::_thesis: B is_closed_on o
A8: B1 is_closed_on o by A2, Def6;
A9: B2 is_closed_on o by A4, Def6;
A10: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def_6
.= o /. B2 by Def8
.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A9, Def7 ;
Den (o,U1) = (Opers (U0,B1)) . o by A3, MSUALG_1:def_6
.= o /. B1 by Def8
.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A8, Def7
.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A10, RELAT_1:71 ;
then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= Result (o,U1) by RELAT_1:def_19;
then rng ((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) c= ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5;
hence B is_closed_on o by A6, Def5; ::_thesis: verum
end;
hence B is opers_closed by Def6; ::_thesis: the Charact of U1 = Opers (U2,B)
for x being set st x in the carrier' of S holds
the Charact of U1 . x = (Opers (U2,B)) . x
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of U1 . x = (Opers (U2,B)) . x )
assume x in the carrier' of S ; ::_thesis: the Charact of U1 . x = (Opers (U2,B)) . x
then reconsider o = x as OperSymbol of S ;
A11: B1 is_closed_on o by A2, Def6;
A12: B2 is_closed_on o by A4, Def6;
A13: Den (o,U2) = (Opers (U0,B2)) . o by A5, MSUALG_1:def_6
.= o /. B2 by Def8
.= (Den (o,U0)) | (((B2 #) * the Arity of S) . o) by A12, Def7 ;
thus the Charact of U1 . x = o /. B1 by A3, Def8
.= (Den (o,U0)) | (((B1 #) * the Arity of S) . o) by A11, Def7
.= (Den (o,U0)) | ((((B2 #) * the Arity of S) . o) /\ (((B1 #) * the Arity of S) . o)) by A1, Th2, XBOOLE_1:28
.= (Den (o,U2)) | (((B1 #) * the Arity of S) . o) by A13, RELAT_1:71
.= o /. B by A6, A7, Def7
.= (Opers (U2,B)) . x by Def8 ; ::_thesis: verum
end;
hence the Charact of U1 = Opers (U2,B) by PBOOLE:3; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U0 be MSAlgebra over S; ::_thesis: 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 #)
let U1, U2 be MSSubAlgebra of U0; ::_thesis: ( the Sorts of U1 = the Sorts of U2 implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
assume the Sorts of U1 = the Sorts of U2 ; ::_thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
then ( U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 ) by Th8;
hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by Th7; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
let U0 be MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
let U1 be MSSubAlgebra of U0; ::_thesis: Constants U0 is MSSubset of U1
Constants U0 c= the Sorts of U1
proof
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S or (Constants U0) . x c= the Sorts of U1 . x )
assume x in the carrier of S ; ::_thesis: (Constants U0) . x c= the Sorts of U1 . x
then reconsider s = x as SortSymbol of S ;
thus (Constants U0) . x c= the Sorts of U1 . x ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )
percases ( the Sorts of U0 . s = {} or the Sorts of U0 . s <> {} ) ;
supposeA1: the Sorts of U0 . s = {} ; ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )
(Constants U0) . s = Constants (U0,s) by Def4
.= {} by A1 ;
hence ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) ; ::_thesis: verum
end;
suppose the Sorts of U0 . s <> {} ; ::_thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )
then A2: ex A being non empty set st
( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3;
reconsider u1 = the Sorts of U1 as MSSubset of U0 by Def9;
assume A3: y in (Constants U0) . x ; ::_thesis: y in the Sorts of U1 . x
(Constants U0) . x = Constants (U0,s) by Def4;
then consider b being Element of the Sorts of U0 . s such that
A4: b = y and
A5: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) by A3, A2;
consider o being OperSymbol of S such that
A6: the Arity of S . o = {} and
A7: the ResultSort of S . o = s and
A8: b in rng (Den (o,U0)) by A5;
A9: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then A10: the Arity of S . o in rng the Arity of S by FUNCT_1:def_3;
( dom {} = {} & rng {} = {} ) ;
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
A11: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
dom (u1 #) = the carrier of S * by PARTFUN1:def_2;
then o in dom ((u1 #) * the Arity of S) by A9, A10, FUNCT_1:11;
then A12: ((u1 #) * the Arity of S) . o = (u1 #) . ( the Arity of S . o) by FUNCT_1:12
.= (u1 #) . (the_arity_of o) by MSUALG_1:def_1
.= product (u1 * (the_arity_of o)) by FINSEQ_2:def_5
.= product (u1 * a) by A6, MSUALG_1:def_1
.= {{}} by CARD_3:10 ;
dom ( the Sorts of U0 #) = the carrier of S * by PARTFUN1:def_2;
then A13: o in dom (( the Sorts of U0 #) * the Arity of S) by A9, A10, FUNCT_1:11;
u1 is opers_closed by Def9;
then u1 is_closed_on o by Def6;
then A14: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by Def5;
rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def_19;
then dom (Den (o,U0)) = Args (o,U0) by A8, FUNCT_2:def_1
.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of U0 #) . ( the Arity of S . o) by A13, FUNCT_1:12
.= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1
.= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5
.= product ( the Sorts of U0 * a) by A6, MSUALG_1:def_1
.= {{}} by CARD_3:10 ;
then (Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (o,U0) by A12, RELAT_1:68;
then b in (u1 * the ResultSort of S) . o by A8, A14;
hence y in the Sorts of U1 . x by A4, A7, A11, FUNCT_1:13; ::_thesis: verum
end;
end;
end;
end;
hence Constants U0 is MSSubset of U1 by PBOOLE:def_18; ::_thesis: verum
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
let S be non empty non void all-with_const_op ManySortedSign ; ::_thesis: 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()
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8()
let U1, U2 be non-empty MSSubAlgebra of U0; ::_thesis: the Sorts of U1 /\ the Sorts of U2 is V8()
Constants U0 is V8() MSSubset of U2 by Th10;
then A1: Constants U0 c= the Sorts of U2 by PBOOLE:def_18;
Constants U0 is V8() MSSubset of U1 by Th10;
then Constants U0 c= the Sorts of U1 by PBOOLE:def_18;
then A2: (Constants U0) /\ (Constants U0) c= the Sorts of U1 /\ the Sorts of U2 by A1, PBOOLE:21;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
not_(_the_Sorts_of_U1_/\_the_Sorts_of_U2)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S implies not ( the Sorts of U1 /\ the Sorts of U2) . i is empty )
assume i in the carrier of S ; ::_thesis: not ( the Sorts of U1 /\ the Sorts of U2) . i is empty
then reconsider s = i as SortSymbol of S ;
( the Sorts of U1 /\ the Sorts of U2) . s = ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by PBOOLE:def_5;
then A3: (Constants U0) . s c= ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by A2, PBOOLE:def_2;
ex a being set st a in (Constants U0) . s by XBOOLE_0:def_1;
hence not ( the Sorts of U1 /\ the Sorts of U2) . i is empty by A3, PBOOLE:def_5; ::_thesis: verum
end;
hence the Sorts of U1 /\ the Sorts of U2 is V8() by PBOOLE:def_13; ::_thesis: verum
end;
begin
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 set 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 b1 being set st
for x being set holds
( x in b1 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
defpred S1[ set ] means ( $1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = $1 holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X 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 ) ) ) )
thus for x being set holds
( x in X 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 ) ) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 set holds
( x in b2 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
b1 = b2
proof
defpred S1[ set ] means ( $1 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & $1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = $1 holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) );
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 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 set holds
( x in b2 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
b1 = b2 ; ::_thesis: verum
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 b4 being set holds
( b4 = SubSort A iff for x being set holds
( x in b4 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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
let A be MSSubset of U0; ::_thesis: the Sorts of U0 in SubSort A
set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0)));
Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def_4;
then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def_2, ZFMISC_1:82;
then A1: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def_2;
( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) by Th3, PBOOLE:def_18;
hence the Sorts of U0 in SubSort A by A1, Def10; ::_thesis: verum
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 set 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 b1 being set st
for x being set holds
( x in b1 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
defpred S1[ set ] means ( $1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = $1 holds
B is opers_closed ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X 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 ) ) )
thus for x being set holds
( x in X 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 ) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 set holds
( x in b2 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
b1 = b2
proof
defpred S1[ set ] means ( $1 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & $1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = $1 holds
B is opers_closed ) );
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 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 set holds
( x in b2 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
b1 = b2 ; ::_thesis: verum
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 b3 being set holds
( b3 = SubSort U0 iff for x being set holds
( x in b3 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
set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0)));
defpred S1[ set ] means ( S is MSSubset of U0 & ( for B being MSSubset of U0 st B = S holds
B is opers_closed ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S1[x] ) ) from XBOOLE_0:sch_1();
Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def_4;
then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def_2, ZFMISC_1:82;
then A2: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def_2;
( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds
B is opers_closed ) ) by Th3, PBOOLE:def_18;
then reconsider X = X as non empty set by A1, A2;
SubSort U0 = X by A1, Def11;
hence not SubSort U0 is empty ; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 ) )
let U0 be MSAlgebra over S; ::_thesis: for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
set C = bool (Union the Sorts of U0);
A1: dom B = the carrier of S by PARTFUN1:def_2;
A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2;
union (rng B) c= union (rng the Sorts of U0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) )
assume x in union (rng B) ; ::_thesis: x in union (rng the Sorts of U0)
then consider Y being set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def_4;
consider y being set such that
A5: y in dom B and
A6: B . y = Y by A4, FUNCT_1:def_3;
A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def_3;
B c= the Sorts of U0 by PBOOLE:def_18;
then B . y c= the Sorts of U0 . y by A1, A5, PBOOLE:def_2;
hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def_4; ::_thesis: verum
end;
then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67;
then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def_4;
thus ( B in SubSort A implies ( B is opers_closed & Constants U0 c= B & A c= B ) ) by Def10; ::_thesis: ( B is opers_closed & Constants U0 c= B & A c= B implies B in SubSort A )
assume ( B is opers_closed & Constants U0 c= B & A c= B ) ; ::_thesis: B in SubSort A
then A9: for C being MSSubset of U0 st C = B holds
( C is opers_closed & Constants U0 c= C & A c= C ) ;
rng B c= bool (union (rng B)) by ZFMISC_1:82;
then rng B c= bool (Union the Sorts of U0) by A8, XBOOLE_1:1;
then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def_2;
hence B in SubSort A by A9, Def10; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
let B be MSSubset of U0; ::_thesis: ( B in SubSort U0 iff B is opers_closed )
set C = bool (Union the Sorts of U0);
A1: dom B = the carrier of S by PARTFUN1:def_2;
A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2;
union (rng B) c= union (rng the Sorts of U0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) )
assume x in union (rng B) ; ::_thesis: x in union (rng the Sorts of U0)
then consider Y being set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def_4;
consider y being set such that
A5: y in dom B and
A6: B . y = Y by A4, FUNCT_1:def_3;
A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def_3;
B c= the Sorts of U0 by PBOOLE:def_18;
then B . y c= the Sorts of U0 . y by A1, A5, PBOOLE:def_2;
hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def_4; ::_thesis: verum
end;
then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67;
then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def_4;
thus ( B in SubSort U0 implies B is opers_closed ) by Def11; ::_thesis: ( B is opers_closed implies B in SubSort U0 )
assume B is opers_closed ; ::_thesis: B in SubSort U0
then A9: for C being MSSubset of U0 st C = B holds
C is opers_closed ;
rng B c= bool (union (rng B)) by ZFMISC_1:82;
then rng B c= bool (Union the Sorts of U0) by A8, XBOOLE_1:1;
then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def_2;
hence B in SubSort U0 by A9, Def11; ::_thesis: verum
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 set holds
( x in it iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
proof
defpred S1[ set ] means ex B being MSSubset of U0 st
( B in SubSort A & $1 = B . s );
set C = bool (Union the Sorts of U0);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (Union the Sorts of U0) & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
A2: bool (Union the Sorts of U0) = bool (union (rng the Sorts of U0)) by CARD_3:def_4;
for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
proof
dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2;
then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def_3;
then A3: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74;
let x be set ; ::_thesis: ( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
thus ( x in X implies ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) implies x in X )
given B being MSSubset of U0 such that A4: B in SubSort A and
A5: x = B . s ; ::_thesis: x in X
B c= the Sorts of U0 by PBOOLE:def_18;
then B . s c= the Sorts of U0 . s by PBOOLE:def_2;
then x c= union (rng the Sorts of U0) by A5, A3, XBOOLE_1:1;
hence x in X by A1, A2, A4, A5; ::_thesis: verum
end;
hence for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) & ( for x being set holds
( x in b2 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex B being MSSubset of U0 st
( B in SubSort A & $1 = B . s );
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) & ( for x being set holds
( x in b2 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) holds
b1 = b2 ; ::_thesis: verum
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 b5 being set holds
( b5 = SubSort (A,s) iff for x being set holds
( x in b5 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
reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
defpred S1[ set ] means ex B being MSSubset of U0 st
( B in SubSort A & S = B . s );
set C = bool (Union the Sorts of U0);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (Union the Sorts of U0) & S1[x] ) ) from XBOOLE_0:sch_1();
A2: bool (Union the Sorts of U0) = bool (union (rng the Sorts of U0)) by CARD_3:def_4;
A3: for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
proof
dom the Sorts of U0 = the carrier of S by PARTFUN1:def_2;
then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def_3;
then A4: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74;
let x be set ; ::_thesis: ( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
thus ( x in X implies ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) implies x in X )
given B being MSSubset of U0 such that A5: B in SubSort A and
A6: x = B . s ; ::_thesis: x in X
B c= the Sorts of U0 by PBOOLE:def_18;
then B . s c= the Sorts of U0 . s by PBOOLE:def_2;
then x c= union (rng the Sorts of U0) by A6, A4, XBOOLE_1:1;
hence x in X by A1, A2, A5, A6; ::_thesis: verum
end;
A7: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def_18;
u0 is opers_closed by Th3;
then u0 in SubSort A by A7, Th13;
then the Sorts of U0 . s in X by A3;
then reconsider X = X as non empty set ;
X = SubSort (A,s) by A3, Def13;
hence not SubSort (A,s) is empty ; ::_thesis: verum
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 b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s))
proof
deffunc H1( SortSymbol of S) -> set = meet (SubSort (A,$1));
consider f being Function such that
A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H1(s) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
f c= the Sorts of U0
proof
reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S or f . x c= the Sorts of U0 . x )
A2: ( A c= u0 & Constants U0 c= u0 ) by PBOOLE:def_18;
assume x in the carrier of S ; ::_thesis: f . x c= the Sorts of U0 . x
then reconsider s = x as SortSymbol of S ;
u0 is opers_closed by Th3;
then u0 in SubSort A by A2, Th13;
then A3: the Sorts of U0 . s in SubSort (A,s) by Def13;
f . s = meet (SubSort (A,s)) by A1;
hence f . x c= the Sorts of U0 . x by A3, SETFAM_1:3; ::_thesis: verum
end;
then reconsider f = f as MSSubset of U0 by PBOOLE:def_18;
take f ; ::_thesis: for s being SortSymbol of S holds f . s = meet (SubSort (A,s))
thus for s being SortSymbol of S holds f . s = meet (SubSort (A,s)) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = meet (SubSort (A,s)) ) holds
b1 = b2
proof
let W1, W2 be MSSubset of U0; ::_thesis: ( ( for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ) implies W1 = W2 )
assume that
A4: for s being SortSymbol of S holds W1 . s = meet (SubSort (A,s)) and
A5: for s being SortSymbol of S holds W2 . s = meet (SubSort (A,s)) ; ::_thesis: W1 = W2
for s being set st s in the carrier of S holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S implies W1 . s = W2 . s )
assume s in the carrier of S ; ::_thesis: W1 . s = W2 . s
then reconsider s = s as SortSymbol of S ;
W1 . s = meet (SubSort (A,s)) by A4;
hence W1 . s = W2 . s by A5; ::_thesis: verum
end;
hence W1 = W2 by PBOOLE:3; ::_thesis: verum
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, b4 being MSSubset of U0 holds
( b4 = MSSubSort A iff for s being SortSymbol of S holds b4 . 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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A
let A be MSSubset of U0; ::_thesis: (Constants U0) \/ A c= MSSubSort A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or ((Constants U0) \/ A) . i c= (MSSubSort A) . i )
assume i in the carrier of S ; ::_thesis: ((Constants U0) \/ A) . i c= (MSSubSort A) . i
then reconsider s = i as SortSymbol of S ;
A1: for Z being set st Z in SubSort (A,s) holds
((Constants U0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in SubSort (A,s) implies ((Constants U0) \/ A) . s c= Z )
assume Z in SubSort (A,s) ; ::_thesis: ((Constants U0) \/ A) . s c= Z
then consider B being MSSubset of U0 such that
A2: B in SubSort A and
A3: Z = B . s by Def13;
( Constants U0 c= B & A c= B ) by A2, Th13;
then (Constants U0) \/ A c= B by PBOOLE:16;
hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
(MSSubSort A) . s = meet (SubSort (A,s)) by Def14;
hence ((Constants U0) \/ A) . i c= (MSSubSort A) . i by A1, SETFAM_1:5; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds
MSSubSort A is V8()
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds
MSSubSort A is V8()
let A be MSSubset of U0; ::_thesis: ( (Constants U0) \/ A is V8() implies MSSubSort A is V8() )
assume A1: (Constants U0) \/ A is V8() ; ::_thesis: MSSubSort A is V8()
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
not_(MSSubSort_A)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S implies not (MSSubSort A) . i is empty )
assume i in the carrier of S ; ::_thesis: not (MSSubSort A) . i is empty
then reconsider s = i as SortSymbol of S ;
for Z being set st Z in SubSort (A,s) holds
((Constants U0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in SubSort (A,s) implies ((Constants U0) \/ A) . s c= Z )
assume Z in SubSort (A,s) ; ::_thesis: ((Constants U0) \/ A) . s c= Z
then consider B being MSSubset of U0 such that
A2: B in SubSort A and
A3: Z = B . s by Def13;
( Constants U0 c= B & A c= B ) by A2, Th13;
then (Constants U0) \/ A c= B by PBOOLE:16;
hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
then A4: ((Constants U0) \/ A) . s c= meet (SubSort (A,s)) by SETFAM_1:5;
ex x being set st x in ((Constants U0) \/ A) . s by A1, XBOOLE_0:def_1;
hence not (MSSubSort A) . i is empty by A4, Def14; ::_thesis: verum
end;
hence MSSubSort A is V8() by PBOOLE:def_13; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: 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
let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A implies (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o )
assume A1: B in SubSort A ; ::_thesis: (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o
MSSubSort A c= B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (MSSubSort A) . i c= B . i )
assume i in the carrier of S ; ::_thesis: (MSSubSort A) . i c= B . i
then reconsider s = i as SortSymbol of S ;
( (MSSubSort A) . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, Def13, Def14;
hence (MSSubSort A) . i c= B . i by SETFAM_1:3; ::_thesis: verum
end;
hence (((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o by Th2; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: 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
let A, B be MSSubset of U0; ::_thesis: ( B in SubSort A implies rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o )
set m = (((MSSubSort A) #) * the Arity of S) . o;
set b = ((B #) * the Arity of S) . o;
set d = Den (o,U0);
assume A1: B in SubSort A ; ::_thesis: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
then (((B #) * the Arity of S) . o) /\ ((((MSSubSort A) #) * the Arity of S) . o) = (((MSSubSort A) #) * the Arity of S) . o by Th17, XBOOLE_1:28;
then (Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o) = ((Den (o,U0)) | (((B #) * the Arity of S) . o)) | ((((MSSubSort A) #) * the Arity of S) . o) by RELAT_1:71;
then A2: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) by RELAT_1:70;
B is opers_closed by A1, Th13;
then B is_closed_on o by Def6;
then rng ((Den (o,U0)) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by Def5;
hence rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A2, XBOOLE_1:1; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: 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
let A be MSSubset of U0; ::_thesis: rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) or x in ((MSSubSort A) * the ResultSort of S) . o )
assume that
A1: x in rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) and
A2: not x in ((MSSubSort A) * the ResultSort of S) . o ; ::_thesis: contradiction
set r = the_result_sort_of o;
A3: ( the_result_sort_of o = the ResultSort of S . o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_2;
then ((MSSubSort A) * the ResultSort of S) . o = (MSSubSort A) . (the_result_sort_of o) by FUNCT_1:13
.= meet (SubSort (A,(the_result_sort_of o))) by Def14 ;
then consider X being set such that
A4: X in SubSort (A,(the_result_sort_of o)) and
A5: not x in X by A2, SETFAM_1:def_1;
consider B being MSSubset of U0 such that
A6: B in SubSort A and
A7: B . (the_result_sort_of o) = X by A4, Def13;
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by A6, Th18;
then x in (B * the ResultSort of S) . o by A1;
hence contradiction by A3, A5, A7, FUNCT_1:13; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
let A be MSSubset of U0; ::_thesis: ( MSSubSort A is opers_closed & A c= MSSubSort A )
thus MSSubSort A is opers_closed ::_thesis: A c= MSSubSort A
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: MSSubSort A is_closed_on o
rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o by Th19;
hence MSSubSort A is_closed_on o by Def5; ::_thesis: verum
end;
( A c= (Constants U0) \/ A & (Constants U0) \/ A c= MSSubSort A ) by Th15, PBOOLE:14;
hence A c= MSSubSort A by PBOOLE:13; ::_thesis: verum
end;
begin
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 ;
funcU0 | 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
reconsider E = MSAlgebra(# A,(Opers (U0,A)) #) as MSAlgebra over S ;
for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) ) by A1;
hence MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0 by Def9; ::_thesis: verum
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;
funcU1 /\ 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 b1 being strict MSSubAlgebra of U0 st
( the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) )
proof
the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 /\ the Sorts of U2 c= the Sorts of U0 /\ the Sorts of U0 by A1, PBOOLE:21;
then reconsider A = the Sorts of U1 /\ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
reconsider E = U0 | A as strict MSSubAlgebra of U0 ;
take E ; ::_thesis: ( the Sorts of E = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) ) ) )
A is opers_closed
proof
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: A is_closed_on o
A2: dom ((u1 #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2;
A3: dom ((u2 #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2;
u2 is opers_closed by Def9;
then u2 is_closed_on o by Def6;
then A4: rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by Def5;
dom ((A #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2;
then A5: ((A #) * the Arity of S) . o = (A #) . ( the Arity of S . o) by FUNCT_1:12
.= (A #) . (the_arity_of o) by MSUALG_1:def_1
.= product ((u1 /\ u2) * (the_arity_of o)) by FINSEQ_2:def_5
.= (product (u1 * (the_arity_of o))) /\ (product (u2 * (the_arity_of o))) by Th1
.= ((u1 #) . (the_arity_of o)) /\ (product (u2 * (the_arity_of o))) by FINSEQ_2:def_5
.= ((u1 #) . (the_arity_of o)) /\ ((u2 #) . (the_arity_of o)) by FINSEQ_2:def_5
.= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . (the_arity_of o)) by MSUALG_1:def_1
.= ((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . ( the Arity of S . o)) by MSUALG_1:def_1
.= (((u1 #) * the Arity of S) . o) /\ ((u2 #) . ( the Arity of S . o)) by A2, FUNCT_1:12
.= (((u1 #) * the Arity of S) . o) /\ (((u2 #) * the Arity of S) . o) by A3, FUNCT_1:12 ;
then (Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) | (((u1 #) * the Arity of S) . o) by RELAT_1:71;
then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) by RELAT_1:70;
then A6: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o by A4, XBOOLE_1:1;
u1 is opers_closed by Def9;
then u1 is_closed_on o by Def6;
then A7: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by Def5;
A8: dom (u2 * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2;
(Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) | (((u2 #) * the Arity of S) . o) by A5, RELAT_1:71;
then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) by RELAT_1:70;
then rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o by A7, XBOOLE_1:1;
then A9: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) by A6, XBOOLE_1:19;
A10: dom (A * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2;
dom (u1 * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2;
then ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) = (u1 . ( the ResultSort of S . o)) /\ ((u2 * the ResultSort of S) . o) by FUNCT_1:12
.= (u1 . ( the ResultSort of S . o)) /\ (u2 . ( the ResultSort of S . o)) by A8, FUNCT_1:12
.= (u1 . (the_result_sort_of o)) /\ (u2 . ( the ResultSort of S . o)) by MSUALG_1:def_2
.= (u1 . (the_result_sort_of o)) /\ (u2 . (the_result_sort_of o)) by MSUALG_1:def_2
.= A . (the_result_sort_of o) by PBOOLE:def_5
.= A . ( the ResultSort of S . o) by MSUALG_1:def_2
.= (A * the ResultSort of S) . o by A10, FUNCT_1:12 ;
hence A is_closed_on o by A9, Def5; ::_thesis: verum
end;
then U0 | A = MSAlgebra(# A,(Opers (U0,A)) #) by Def15;
hence the Sorts of E = the Sorts of U1 /\ the Sorts of U2 ; ::_thesis: for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) )
thus for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) ) by Def9; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers (U0,B) ) ) & the Sorts of b2 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b2 holds
( B is opers_closed & the Charact of b2 = Opers (U0,B) ) ) holds
b1 = b2 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 b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 /\ U2 iff ( the Sorts of b5 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b5 holds
( B is opers_closed & the Charact of b5 = 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 b1 being strict MSSubAlgebra of U0 st
( A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) )
proof
set a = MSSubSort A;
reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ;
take u1 ; ::_thesis: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1 ) )
A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by Def15, Th20;
A c= MSSubSort A by Th20;
hence A is MSSubset of u1 by A1, PBOOLE:def_18; ::_thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1
let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by Def9;
assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2
then A2: A c= B by PBOOLE:def_18;
Constants U0 is MSSubset of U2 by Th10;
then A3: Constants U0 c= B by PBOOLE:def_18;
B is opers_closed by Def9;
then A4: B in SubSort A by A2, A3, Th13;
the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A4, Def13, Def14;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence u1 is MSSubAlgebra of U2 by Th8; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) & A is MSSubset of b2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b2 is MSSubAlgebra of U1 ) holds
b1 = b2
proof
let W1, W2 be strict MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W2 is MSSubAlgebra of U1 ) implies W1 = W2 )
assume ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds
W2 is MSSubAlgebra of U2 ) ) ; ::_thesis: W1 = W2
then ( W1 is strict MSSubAlgebra of W2 & W2 is strict MSSubAlgebra of W1 ) ;
hence W1 = W2 by Th7; ::_thesis: verum
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 b4 being strict MSSubAlgebra of U0 holds
( b4 = GenMSAlg A iff ( A is MSSubset of b4 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b4 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
(Constants U0) \/ A is V8() ;
then reconsider a = MSSubSort A as V8() MSSubset of U0 by Th16;
U0 | a = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20;
then reconsider u1 = U0 | a as strict non-empty MSSubAlgebra of U0 by MSUALG_1:def_3;
A1: A c= a by Th20;
now__::_thesis:_(_A_is_MSSubset_of_u1_&_(_for_U2_being_MSSubAlgebra_of_U0_st_A_is_MSSubset_of_U2_holds_
u1_is_MSSubAlgebra_of_U2_)_)
A2: u1 = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20;
hence A is MSSubset of u1 by A1, PBOOLE:def_18; ::_thesis: for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds
u1 is MSSubAlgebra of U2
let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by Def9;
assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2
then A3: A c= B by PBOOLE:def_18;
Constants U0 is MSSubset of U2 by Th10;
then A4: Constants U0 c= B by PBOOLE:def_18;
B is opers_closed by Def9;
then A5: B in SubSort A by A3, A4, Th13;
the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A2, A5, Def13, Def14;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence u1 is MSSubAlgebra of U2 by Th8; ::_thesis: verum
end;
hence GenMSAlg A is non-empty by Def17; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U0 be MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) )
set W = GenMSAlg B;
reconsider B1 = the Sorts of (GenMSAlg B) as MSSubset of U0 by Def9;
A1: the Charact of (GenMSAlg B) = Opers (U0,B1) by Def9;
assume B = the Sorts of U0 ; ::_thesis: GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
then the Sorts of U0 is MSSubset of (GenMSAlg B) by Def17;
then A2: the Sorts of U0 c= the Sorts of (GenMSAlg B) by PBOOLE:def_18;
the Sorts of (GenMSAlg B) is MSSubset of U0 by Def9;
then the Sorts of (GenMSAlg B) c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U0 = the Sorts of (GenMSAlg B) by A2, PBOOLE:146;
hence GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) by A1, Th4; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U0 be MSAlgebra over S; ::_thesis: 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 #)
let U1 be MSSubAlgebra of U0; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) )
assume A1: B = the Sorts of U1 ; ::_thesis: GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
set W = GenMSAlg B;
B is MSSubset of (GenMSAlg B) by Def17;
then the Sorts of U1 c= the Sorts of (GenMSAlg B) by A1, PBOOLE:def_18;
then A2: U1 is MSSubAlgebra of GenMSAlg B by Th8;
B is MSSubset of U1 by A1, PBOOLE:def_18;
then GenMSAlg B is MSSubAlgebra of U1 by Def17;
hence GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by A2, Th7; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
let U1 be MSSubAlgebra of U0; ::_thesis: (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
set C = Constants U0;
set G = GenMSAlg (Constants U0);
Constants U0 is MSSubset of U1 by Th10;
then GenMSAlg (Constants U0) is strict MSSubAlgebra of U1 by Def17;
then the Sorts of (GenMSAlg (Constants U0)) is MSSubset of U1 by Def9;
then A1: the Sorts of (GenMSAlg (Constants U0)) c= the Sorts of U1 by PBOOLE:def_18;
the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) /\ the Sorts of U1 by Def16;
then the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) by A1, PBOOLE:23;
hence (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) by Th9; ::_thesis: verum
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;
funcU1 "\/" 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 b1 being strict MSSubAlgebra of U0 st
for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenMSAlg A
proof
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
take GenMSAlg B ; ::_thesis: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenMSAlg B = GenMSAlg A
thus for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenMSAlg B = GenMSAlg A ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenMSAlg A ) holds
b1 = b2
proof
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by Def9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
let W1, W2 be strict MSSubAlgebra of U0; ::_thesis: ( ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenMSAlg A ) implies W1 = W2 )
assume that
A3: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenMSAlg A and
A4: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenMSAlg A ; ::_thesis: W1 = W2
W1 = GenMSAlg B by A3;
hence W1 = W2 by A4; ::_thesis: verum
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 b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b5 = 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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let U1 be MSSubAlgebra of U0; ::_thesis: for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenMSAlg A) "\/" U1 = GenMSAlg B
let A, B be MSSubset of U0; ::_thesis: ( B = A \/ the Sorts of U1 implies (GenMSAlg A) "\/" U1 = GenMSAlg B )
reconsider u1 = the Sorts of U1, a = the Sorts of (GenMSAlg A) as MSSubset of U0 by Def9;
A1: the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) c= a by PBOOLE:15;
A2: the Sorts of ((GenMSAlg A) /\ (GenMSAlg B)) = the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by Def16;
( a c= the Sorts of U0 & u1 c= the Sorts of U0 ) by PBOOLE:def_18;
then a \/ u1 c= the Sorts of U0 by PBOOLE:16;
then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def_18;
A3: (GenMSAlg A) "\/" U1 = GenMSAlg b by Def18;
then a \/ u1 is MSSubset of ((GenMSAlg A) "\/" U1) by Def17;
then A4: a \/ u1 c= the Sorts of ((GenMSAlg A) "\/" U1) by PBOOLE:def_18;
A is MSSubset of (GenMSAlg A) by Def17;
then A5: A c= the Sorts of (GenMSAlg A) by PBOOLE:def_18;
B is MSSubset of (GenMSAlg B) by Def17;
then A6: B c= the Sorts of (GenMSAlg B) by PBOOLE:def_18;
assume A7: B = A \/ the Sorts of U1 ; ::_thesis: (GenMSAlg A) "\/" U1 = GenMSAlg B
then A c= B by PBOOLE:14;
then A c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;
then A c= the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A5, PBOOLE:17;
then A is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by A2, PBOOLE:def_18;
then GenMSAlg A is MSSubAlgebra of (GenMSAlg A) /\ (GenMSAlg B) by Def17;
then a is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by Def9;
then a c= the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A2, PBOOLE:def_18;
then a = the Sorts of (GenMSAlg A) /\ the Sorts of (GenMSAlg B) by A1, PBOOLE:146;
then A8: a c= the Sorts of (GenMSAlg B) by PBOOLE:15;
u1 c= B by A7, PBOOLE:14;
then u1 c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;
then b c= the Sorts of (GenMSAlg B) by A8, PBOOLE:16;
then b is MSSubset of (GenMSAlg B) by PBOOLE:def_18;
then A9: GenMSAlg b is strict MSSubAlgebra of GenMSAlg B by Def17;
A \/ u1 c= a \/ u1 by A5, PBOOLE:20;
then B c= the Sorts of ((GenMSAlg A) "\/" U1) by A7, A4, PBOOLE:13;
then B is MSSubset of ((GenMSAlg A) "\/" U1) by PBOOLE:def_18;
then GenMSAlg B is strict MSSubAlgebra of (GenMSAlg A) "\/" U1 by Def17;
hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th7; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
let U1 be MSSubAlgebra of U0; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies (GenMSAlg B) "\/" U1 = GenMSAlg B )
assume A1: B = the Sorts of U0 ; ::_thesis: (GenMSAlg B) "\/" U1 = GenMSAlg B
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= B by A1, PBOOLE:def_18;
then B \/ the Sorts of U1 = B by PBOOLE:22;
hence (GenMSAlg B) "\/" U1 = GenMSAlg B by Th24; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
let U1, U2 be MSSubAlgebra of U0; ::_thesis: U1 "\/" U2 = U2 "\/" U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
U1 "\/" U2 = GenMSAlg A by Def18;
hence U1 "\/" U2 = U2 "\/" U1 by Def18; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
let U1, U2 be MSSubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;
A1: the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/" U2) by Def16;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
U1 "\/" U2 = GenMSAlg A by Def18;
then A is MSSubset of (U1 "\/" U2) by Def17;
then A2: A c= the Sorts of (U1 "\/" U2) by PBOOLE:def_18;
the Sorts of U1 c= A by PBOOLE:14;
then the Sorts of U1 c= the Sorts of (U1 "\/" U2) by A2, PBOOLE:13;
then A3: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/" U2)) by A1, PBOOLE:17;
reconsider u112 = the Sorts of (U1 /\ (U1 "\/" U2)) as MSSubset of U0 by Def9;
A4: the Charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by Def16;
the Sorts of (U1 /\ (U1 "\/" U2)) c= the Sorts of U1 by A1, PBOOLE:15;
then the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 by A3, PBOOLE:146;
hence U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by A4, Def9; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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 #)
let U0 be non-empty MSAlgebra over S; ::_thesis: for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
let U1, U2 be MSSubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by Def9;
( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then u12 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
u12 = the Sorts of U1 /\ the Sorts of U2 by Def16;
then u12 c= u2 by PBOOLE:15;
then A1: A = u2 by PBOOLE:22;
(U1 /\ U2) "\/" U2 = GenMSAlg A by Def18;
hence (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, Th22; ::_thesis: verum
end;
begin
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 set holds
( x in it iff x is strict MSSubAlgebra of U0 );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 )
proof
reconsider X = { (GenMSAlg (@ A)) where A is Element of SubSort U0 : verum } as set ;
take X ; ::_thesis: for x being set holds
( x in X iff x is strict MSSubAlgebra of U0 )
let x be set ; ::_thesis: ( x in X iff x is strict MSSubAlgebra of U0 )
thus ( x in X implies x is strict MSSubAlgebra of U0 ) ::_thesis: ( x is strict MSSubAlgebra of U0 implies x in X )
proof
assume x in X ; ::_thesis: x is strict MSSubAlgebra of U0
then ex A being Element of SubSort U0 st x = GenMSAlg (@ A) ;
hence x is strict MSSubAlgebra of U0 ; ::_thesis: verum
end;
assume x is strict MSSubAlgebra of U0 ; ::_thesis: x in X
then reconsider a = x as strict MSSubAlgebra of U0 ;
reconsider A = the Sorts of a as MSSubset of U0 by Def9;
A is opers_closed by Def9;
then reconsider h = A as Element of SubSort U0 by Th14;
a = GenMSAlg (@ h) by Th22;
hence x in X ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds
( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is strict MSSubAlgebra of U0;
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds
( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds
b1 = b2 ; ::_thesis: verum
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 b3 being set holds
( b3 = MSSub U0 iff for x being set holds
( x in b3 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
set x = the strict MSSubAlgebra of U0;
the strict MSSubAlgebra of U0 in MSSub U0 by Def19;
hence not MSSub U0 is empty ; ::_thesis: verum
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 b1 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
b1 . (x,y) = U1 "\/" U2
proof
defpred S1[ Element of MSSub U0, Element of MSSub U0, Element of MSSub U0] means for U1, U2 being strict MSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 "\/" U2;
A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S1[x,y,z]
proof
let x, y be Element of MSSub U0; ::_thesis: ex z being Element of MSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
reconsider z = U1 "\/" U2 as Element of MSSub U0 by Def19;
take z ; ::_thesis: S1[x,y,z]
thus S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (MSSub U0) such that
A2: for a, b being Element of MSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take o ; ::_thesis: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/" U2
thus for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/" U2 by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (MSSub U0); ::_thesis: ( ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (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
o2 . (x,y) = U1 "\/" U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 "\/" U2 and
A4: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 "\/" U2 ; ::_thesis: o1 = o2
for x, y being Element of MSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of MSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
o1 . (x,y) = U1 "\/" U2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
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 b3 being BinOp of (MSSub U0) holds
( b3 = 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
b3 . (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 b1 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
b1 . (x,y) = U1 /\ U2
proof
defpred S1[ Element of MSSub U0, Element of MSSub U0, Element of MSSub U0] means for U1, U2 being strict MSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 /\ U2;
A1: for x, y being Element of MSSub U0 ex z being Element of MSSub U0 st S1[x,y,z]
proof
let x, y be Element of MSSub U0; ::_thesis: ex z being Element of MSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
reconsider z = U1 /\ U2 as Element of MSSub U0 by Def19;
take z ; ::_thesis: S1[x,y,z]
thus S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (MSSub U0) such that
A2: for a, b being Element of MSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take o ; ::_thesis: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2
thus for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2 by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (MSSub U0); ::_thesis: ( ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (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
o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 and
A4: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2
for x, y being Element of MSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of MSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
o1 . (x,y) = U1 /\ U2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
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 b3 being BinOp of (MSSub U0) holds
( b3 = 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
b3 . (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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative
let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_join U0 is commutative
set o = MSAlg_join U0;
for x, y being Element of MSSub U0 holds (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x)
proof
let x, y be Element of MSSub U0; ::_thesis: (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x)
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
set B = the Sorts of U1 \/ the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
A2: U1 "\/" U2 = GenMSAlg B by Def18;
( (MSAlg_join U0) . (x,y) = U1 "\/" U2 & (MSAlg_join U0) . (y,x) = U2 "\/" U1 ) by Def20;
hence (MSAlg_join U0) . (x,y) = (MSAlg_join U0) . (y,x) by A2, Def18; ::_thesis: verum
end;
hence MSAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative
let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_join U0 is associative
set o = MSAlg_join U0;
for x, y, z being Element of MSSub U0 holds (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z)
proof
let x, y, z be Element of MSSub U0; ::_thesis: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19;
set B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3);
A1: (MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;
the Sorts of U2 is MSSubset of U0 by Def9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
the Sorts of U3 is MSSubset of U0 by Def9;
then the Sorts of U3 c= the Sorts of U0 by PBOOLE:def_18;
then A3: the Sorts of U2 \/ the Sorts of U3 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider C = the Sorts of U2 \/ the Sorts of U3 as MSSubset of U0 by PBOOLE:def_18;
the Sorts of U1 is MSSubset of U0 by Def9;
then A4: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then A5: the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) c= the Sorts of U0 by A3, PBOOLE:16;
the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A4, A2, PBOOLE:16;
then reconsider D = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
reconsider B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) as MSSubset of U0 by A5, PBOOLE:def_18;
A6: B = D \/ the Sorts of U3 by PBOOLE:28;
A7: (U1 "\/" U2) "\/" U3 = (GenMSAlg D) "\/" U3 by Def18
.= GenMSAlg B by A6, Th24 ;
(MSAlg_join U0) . (y,z) = U2 "\/" U3 by Def20;
then A8: (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = U1 "\/" (U2 "\/" U3) by Def20;
U1 "\/" (U2 "\/" U3) = U1 "\/" (GenMSAlg C) by Def18
.= (GenMSAlg C) "\/" U1 by Th26
.= GenMSAlg B by Th24 ;
hence (MSAlg_join U0) . (x,((MSAlg_join U0) . (y,z))) = (MSAlg_join U0) . (((MSAlg_join U0) . (x,y)),z) by A1, A8, A7, Def20; ::_thesis: verum
end;
hence MSAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative
let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_meet U0 is commutative
set o = MSAlg_meet U0;
for x, y being Element of MSSub U0 holds (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x)
proof
let x, y be Element of MSSub U0; ::_thesis: (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x)
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
A1: ( the Sorts of (U2 /\ U1) = the Sorts of U2 /\ the Sorts of U1 & ( for B2 being MSSubset of U0 st B2 = the Sorts of (U2 /\ U1) holds
( B2 is opers_closed & the Charact of (U2 /\ U1) = Opers (U0,B2) ) ) ) by Def16;
( (MSAlg_meet U0) . (x,y) = U1 /\ U2 & (MSAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def21;
hence (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) by A1, Def16; ::_thesis: verum
end;
hence MSAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative
let U0 be non-empty MSAlgebra over S; ::_thesis: MSAlg_meet U0 is associative
set o = MSAlg_meet U0;
for x, y, z being Element of MSSub U0 holds (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)
proof
let x, y, z be Element of MSSub U0; ::_thesis: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19;
reconsider u23 = U2 /\ U3, u12 = U1 /\ U2 as Element of MSSub U0 by Def19;
A1: ( the Sorts of (U1 /\ U2) = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of (U1 /\ (U2 /\ U3)) holds
( B is opers_closed & the Charact of (U1 /\ (U2 /\ U3)) = Opers (U0,B) ) ) ) by Def16;
A2: (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) = (MSAlg_meet U0) . (u12,z) by Def21
.= (U1 /\ U2) /\ U3 by Def21 ;
the Sorts of (U2 /\ U3) = the Sorts of U2 /\ the Sorts of U3 by Def16;
then A3: the Sorts of (U1 /\ (U2 /\ U3)) = the Sorts of U1 /\ ( the Sorts of U2 /\ the Sorts of U3) by Def16;
then reconsider C = the Sorts of U1 /\ ( the Sorts of U2 /\ the Sorts of U3) as MSSubset of U0 by Def9;
A4: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,u23) by Def21
.= U1 /\ (U2 /\ U3) by Def21 ;
C = ( the Sorts of U1 /\ the Sorts of U2) /\ the Sorts of U3 by PBOOLE:29;
hence (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A4, A2, A3, A1, Def16; ::_thesis: verum
end;
hence MSAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum
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
set L = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);
A1: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
MSAlg_join U0 is associative by Th30;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def_3; ::_thesis: verum
end;
A2: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" b = b "/\" a
proof
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a
MSAlg_meet U0 is commutative by Th31;
hence a "/\" b = b "/\" a by BINOP_1:def_2; ::_thesis: verum
end;
A3: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (a "\/" b) = a
proof
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of MSSub U0 ;
(MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = x
proof
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;
hence (MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def21
.= x by Th27 ;
::_thesis: verum
end;
hence a "/\" (a "\/" b) = a ; ::_thesis: verum
end;
A4: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds (a "/\" b) "\/" b = b
proof
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of MSSub U0 ;
(MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_meet U0) . (x,y) = U1 /\ U2 by Def21;
hence (MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def20
.= y by Th28 ;
::_thesis: verum
end;
hence (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
A5: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
MSAlg_meet U0 is associative by Th32;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def_3; ::_thesis: verum
end;
for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" b = b "\/" a
proof
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a
MSAlg_join U0 is commutative by Th29;
hence a "\/" b = b "\/" a by BINOP_1:def_2; ::_thesis: verum
end;
then ( LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-absorbing & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice ; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded
let U0 be non-empty MSAlgebra over S; ::_thesis: MSSubAlLattice U0 is bounded
set L = MSSubAlLattice U0;
thus MSSubAlLattice U0 is lower-bounded :: according to LATTICES:def_15 ::_thesis: MSSubAlLattice U0 is upper-bounded
proof
set C = Constants U0;
reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19;
reconsider G1 = G as Element of (MSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (MSSubAlLattice U0) holds
( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 )
let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "/\" a = (GenMSAlg (Constants U0)) /\ a2 by Def21
.= G1 by Th23 ; ::_thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; ::_thesis: verum
end;
thus MSSubAlLattice U0 is upper-bounded ::_thesis: verum
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;
reconsider G1 = G as Element of (MSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (MSSubAlLattice U0) holds
( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 )
let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "\/" a = (GenMSAlg B) "\/" a2 by Def20
.= G1 by Th25 ; ::_thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; ::_thesis: verum
end;
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
let U0 be non-empty MSAlgebra over S; ::_thesis: Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
set C = Constants U0;
reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19;
set L = MSSubAlLattice U0;
reconsider G1 = G as Element of (MSSubAlLattice U0) ;
now__::_thesis:_for_a_being_Element_of_(MSSubAlLattice_U0)_holds_
(_G1_"/\"_a_=_G1_&_a_"/\"_G1_=_G1_)
let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "/\" a = (GenMSAlg (Constants U0)) /\ a2 by Def21
.= G1 by Th23 ; ::_thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; ::_thesis: verum
end;
hence Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) by LATTICES:def_16; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
Top (MSSubAlLattice U0) = GenMSAlg B
let B be MSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Top (MSSubAlLattice U0) = GenMSAlg B )
reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;
set L = MSSubAlLattice U0;
reconsider G1 = G as Element of (MSSubAlLattice U0) ;
assume A1: B = the Sorts of U0 ; ::_thesis: Top (MSSubAlLattice U0) = GenMSAlg B
now__::_thesis:_for_a_being_Element_of_(MSSubAlLattice_U0)_holds_
(_G1_"\/"_a_=_G1_&_a_"\/"_G1_=_G1_)
let a be Element of (MSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "\/" a = (GenMSAlg B) "\/" a2 by Def20
.= G1 by A1, Th25 ; ::_thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; ::_thesis: verum
end;
hence Top (MSSubAlLattice U0) = GenMSAlg B by LATTICES:def_17; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
let U0 be non-empty MSAlgebra over S; ::_thesis: Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
thus Top (MSSubAlLattice U0) = GenMSAlg B by Th35
.= MSAlgebra(# the Sorts of U0, the Charact of U0 #) by Th21 ; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 holds SubSort A c= SubSort U0
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds SubSort A c= SubSort U0
let A be MSSubset of U0; ::_thesis: SubSort A c= SubSort U0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort A or x in SubSort U0 )
assume A1: x in SubSort A ; ::_thesis: x in SubSort U0
A2: for B being MSSubset of U0 st B = x holds
B is opers_closed by A1, Def10;
( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 ) by A1, Def10;
hence x in SubSort U0 by A2, Def11; ::_thesis: verum
end;