:: MSUALG_9 semantic presentation
begin
registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like I -defined Function-like total V32() for Element of Bool M;
existence
not for b1 being Element of Bool M holds b1 is V32()
proof
[[0]] I c= M by PBOOLE:43;
then [[0]] I is ManySortedSubset of M by PBOOLE:def_18;
then reconsider A = [[0]] I as Element of Bool M by CLOSURE2:def_1;
take A ; ::_thesis: A is V32()
thus A is V32() ; ::_thesis: verum
end;
end;
registration
let I be set ;
let M be V2() ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like total V32() for ManySortedSubset of M;
existence
ex b1 being ManySortedSubset of M st
( b1 is V2() & b1 is V32() )
proof
defpred S1[ set , set ] means ex a being Element of M . I st M = {a};
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume i in I ; ::_thesis: ex j being set st S1[i,j]
set a = the Element of M . i;
take j = { the Element of M . i}; ::_thesis: S1[i,j]
thus S1[i,j] ; ::_thesis: verum
end;
consider C being ManySortedSet of I such that
A2: for i being set st i in I holds
S1[i,C . i] from PBOOLE:sch_3(A1);
C is ManySortedSubset of M
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or C . i c= M . i )
assume A3: i in I ; ::_thesis: C . i c= M . i
then A4: not M . i is empty ;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C . i or q in M . i )
consider a being Element of M . i such that
A5: C . i = {a} by A2, A3;
assume q in C . i ; ::_thesis: q in M . i
then q = a by A5, TARSKI:def_1;
hence q in M . i by A4; ::_thesis: verum
end;
then reconsider C = C as ManySortedSubset of M ;
take C ; ::_thesis: ( C is V2() & C is V32() )
thus C is V2() ::_thesis: C is V32()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not C . i is empty )
assume i in I ; ::_thesis: not C . i is empty
then ex a being Element of M . i st C . i = {a} by A2;
hence not C . i is empty ; ::_thesis: verum
end;
let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or C . i is finite )
assume i in I ; ::_thesis: C . i is finite
then ex a being Element of M . i st C . i = {a} by A2;
hence C . i is finite ; ::_thesis: verum
end;
end;
registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let o be OperSymbol of S;
cluster -> FinSequence-like for Element of Args (o,A);
coherence
for b1 being Element of Args (o,A) holds b1 is FinSequence-like
proof
let x be Element of Args (o,A); ::_thesis: x is FinSequence-like
dom x = dom (the_arity_of o) by MSUALG_6:2;
then consider n being Nat such that
A1: dom x = Seg n by FINSEQ_1:def_2;
take n ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg n
thus dom x = Seg n by A1; ::_thesis: verum
end;
end;
registration
let S be non empty non void ManySortedSign ;
let I be set ;
let s be SortSymbol of S;
let F be MSAlgebra-Family of I,S;
cluster -> Relation-like Function-like for Element of (SORTS F) . s;
coherence
for b1 being Element of (SORTS F) . s holds
( b1 is Function-like & b1 is Relation-like )
proof
let x be Element of (SORTS F) . s; ::_thesis: ( x is Function-like & x is Relation-like )
x is Element of product (Carrier (F,s)) by PRALG_2:def_10;
hence ( x is Function-like & x is Relation-like ) ; ::_thesis: verum
end;
end;
registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeGen X -> V2() free ;
coherence
( FreeGen X is free & FreeGen X is non-empty ) by MSAFREE:14, MSAFREE:16;
end;
registration
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
cluster FreeMSA X -> free ;
coherence
FreeMSA X is free by MSAFREE:17;
end;
registration
let S be non empty non void ManySortedSign ;
let A, B be non-empty MSAlgebra over S;
cluster[:A,B:] -> non-empty ;
coherence
[:A,B:] is non-empty
proof
[:A,B:] = MSAlgebra(# [| the Sorts of A, the Sorts of B|],[[: the Charact of A, the Charact of B:]] #) by PRALG_2:def_8;
hence the Sorts of [:A,B:] is V2() ; :: according to MSUALG_1:def_3 ::_thesis: verum
end;
end;
theorem :: MSUALG_9:1
for a, X, Y being set
for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
proof
let a be set ; ::_thesis: for X, Y being set
for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
let X, Y be set ; ::_thesis: for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
let f be Function; ::_thesis: ( a in dom f & f . a in [:X,Y:] implies f . a = [((pr1 f) . a),((pr2 f) . a)] )
assume that
A1: a in dom f and
A2: f . a in [:X,Y:] ; ::_thesis: f . a = [((pr1 f) . a),((pr2 f) . a)]
( (pr1 f) . a = (f . a) `1 & (pr2 f) . a = (f . a) `2 ) by A1, MCART_1:def_12, MCART_1:def_13;
hence f . a = [((pr1 f) . a),((pr2 f) . a)] by A2, MCART_1:21; ::_thesis: verum
end;
theorem Th2: :: MSUALG_9:2
for X being non empty set
for Y being set
for f being Function of X,{Y} holds rng f = {Y}
proof
let X be non empty set ; ::_thesis: for Y being set
for f being Function of X,{Y} holds rng f = {Y}
let Y be set ; ::_thesis: for f being Function of X,{Y} holds rng f = {Y}
let f be Function of X,{Y}; ::_thesis: rng f = {Y}
thus rng f c= {Y} ; :: according to XBOOLE_0:def_10 ::_thesis: {Y} c= rng f
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {Y} or q in rng f )
consider x being set such that
A1: x in X by XBOOLE_0:def_1;
assume q in {Y} ; ::_thesis: q in rng f
then A2: ( dom f = X & q = Y ) by FUNCT_2:def_1, TARSKI:def_1;
f . x = Y by A1, FUNCT_2:50;
hence q in rng f by A2, A1, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th3: :: MSUALG_9:3
for I being set holds Class (nabla I) c= {I}
proof
let I be set ; ::_thesis: Class (nabla I) c= {I}
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (nabla I) or q in {I} )
assume q in Class (nabla I) ; ::_thesis: q in {I}
then consider x being set such that
A1: x in I and
A2: q = Class ((nabla I),x) by EQREL_1:def_3;
Class ((nabla I),x) = I by A1, EQREL_1:26;
hence q in {I} by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th4: :: MSUALG_9:4
for I being non empty set holds Class (nabla I) = {I}
proof
let I be non empty set ; ::_thesis: Class (nabla I) = {I}
consider a being set such that
A1: a in I by XBOOLE_0:def_1;
thus Class (nabla I) c= {I} by Th3; :: according to XBOOLE_0:def_10 ::_thesis: {I} c= Class (nabla I)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {I} or q in Class (nabla I) )
assume q in {I} ; ::_thesis: q in Class (nabla I)
then A2: q = I by TARSKI:def_1;
Class ((nabla I),a) = I by A1, EQREL_1:26;
hence q in Class (nabla I) by A2, A1, EQREL_1:def_3; ::_thesis: verum
end;
theorem Th5: :: MSUALG_9:5
for I, a being set ex A being ManySortedSet of I st {A} = I --> {a}
proof
let I, a be set ; ::_thesis: ex A being ManySortedSet of I st {A} = I --> {a}
reconsider A = I --> a as ManySortedSet of I ;
take A ; ::_thesis: {A} = I --> {a}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
{A}_._i_=_(I_-->_{a})_._i
let i be set ; ::_thesis: ( i in I implies {A} . i = (I --> {a}) . i )
assume A1: i in I ; ::_thesis: {A} . i = (I --> {a}) . i
hence {A} . i = {(A . i)} by PZFMISC1:def_1
.= {a} by A1, FUNCOP_1:7
.= (I --> {a}) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence {A} = I --> {a} by PBOOLE:3; ::_thesis: verum
end;
theorem :: MSUALG_9:6
for I being set
for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B
proof
let I be set ; ::_thesis: for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B
let A be ManySortedSet of I; ::_thesis: ex B being V2() ManySortedSet of I st A c= B
deffunc H1( set ) -> set = {{}} \/ (A . $1);
consider f being ManySortedSet of I such that
A1: for i being set st i in I holds
f . i = H1(i) from PBOOLE:sch_4();
f is V2()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not f . i is empty )
assume i in I ; ::_thesis: not f . i is empty
then f . i = {{}} \/ (A . i) by A1;
hence not f . i is empty ; ::_thesis: verum
end;
then reconsider f = f as V2() ManySortedSet of I ;
take f ; ::_thesis: A c= f
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= f . i )
assume i in I ; ::_thesis: A . i c= f . i
then f . i = (A . i) \/ {{}} by A1;
hence A . i c= f . i by XBOOLE_1:7; ::_thesis: verum
end;
theorem :: MSUALG_9:7
for I being set
for M being V2() ManySortedSet of I
for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C
proof
let I be set ; ::_thesis: for M being V2() ManySortedSet of I
for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C
let M be V2() ManySortedSet of I; ::_thesis: for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C
let B be V32() ManySortedSubset of M; ::_thesis: ex C being V2() V32() ManySortedSubset of M st B c= C
defpred S1[ set , set ] means ex a being Element of M . $1 st $2 = {a} \/ (B . $1);
A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume i in I ; ::_thesis: ex j being set st S1[i,j]
set a = the Element of M . i;
take j = { the Element of M . i} \/ (B . i); ::_thesis: S1[i,j]
thus S1[i,j] ; ::_thesis: verum
end;
consider C being ManySortedSet of I such that
A2: for i being set st i in I holds
S1[i,C . i] from PBOOLE:sch_3(A1);
A3: C is ManySortedSubset of M
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or C . i c= M . i )
assume A4: i in I ; ::_thesis: C . i c= M . i
then consider a being Element of M . i such that
A5: C . i = {a} \/ (B . i) by A2;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C . i or q in M . i )
assume q in C . i ; ::_thesis: q in M . i
then A6: ( q in {a} or q in B . i ) by A5, XBOOLE_0:def_3;
B c= M by PBOOLE:def_18;
then B . i c= M . i by A4, PBOOLE:def_2;
then A7: ( q = a or q in M . i ) by A6, TARSKI:def_1;
not M . i is empty by A4;
hence q in M . i by A7; ::_thesis: verum
end;
A8: C is V32()
proof
let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or C . i is finite )
assume A9: i in I ; ::_thesis: C . i is finite
reconsider b = B . i as finite set ;
consider a being Element of M . i such that
A10: C . i = {a} \/ (B . i) by A2, A9;
thus C . i is finite by A10; ::_thesis: verum
end;
C is V2()
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not C . i is empty )
assume i in I ; ::_thesis: not C . i is empty
then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2;
hence not C . i is empty ; ::_thesis: verum
end;
then reconsider C = C as V2() V32() ManySortedSubset of M by A3, A8;
take C ; ::_thesis: B c= C
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or B . i c= C . i )
assume i in I ; ::_thesis: B . i c= C . i
then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2;
hence B . i c= C . i by XBOOLE_1:7; ::_thesis: verum
end;
theorem :: MSUALG_9:8
for I being set
for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G
let A, B be ManySortedSet of I; ::_thesis: for F, G being ManySortedFunction of A,{B} holds F = G
let F, G be ManySortedFunction of A,{B}; ::_thesis: F = G
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F_._i_=_G_._i
let i be set ; ::_thesis: ( i in I implies F . i = G . i )
assume A1: i in I ; ::_thesis: F . i = G . i
then A2: {B} . i = {(B . i)} by PZFMISC1:def_1;
( F . i is Function of (A . i),({B} . i) & G . i is Function of (A . i),({B} . i) ) by A1, PBOOLE:def_15;
hence F . i = G . i by A2, FUNCT_2:51; ::_thesis: verum
end;
hence F = G by PBOOLE:3; ::_thesis: verum
end;
theorem Th9: :: MSUALG_9:9
for I being set
for A being V2() ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
proof
let I be set ; ::_thesis: for A being V2() ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
let A be V2() ManySortedSet of I; ::_thesis: for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
let B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,{B} holds F is "onto"
let F be ManySortedFunction of A,{B}; ::_thesis: F is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng (F . i) = {B} . i )
assume A1: i in I ; ::_thesis: rng (F . i) = {B} . i
then ( {B} . i = {(B . i)} & F . i is Function of (A . i),({B} . i) ) by PBOOLE:def_15, PZFMISC1:def_1;
hence rng (F . i) = {B} . i by A1, Th2; ::_thesis: verum
end;
theorem Th10: :: MSUALG_9:10
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of {A},B holds F is "1-1"
let F be ManySortedFunction of {A},B; ::_thesis: F is "1-1"
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F_._i_is_one-to-one
let i be set ; ::_thesis: ( i in I implies F . i is one-to-one )
assume i in I ; ::_thesis: F . i is one-to-one
then ( {A} . i = {(A . i)} & F . i is Function of ({A} . i),(B . i) ) by PBOOLE:def_15, PZFMISC1:def_1;
hence F . i is one-to-one by PARTFUN1:17; ::_thesis: verum
end;
hence F is "1-1" by MSUALG_3:1; ::_thesis: verum
end;
theorem :: MSUALG_9:11
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1"
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1"
let X be V2() ManySortedSet of the carrier of S; ::_thesis: Reverse X is "1-1"
for i being set st i in the carrier of S holds
(Reverse X) . i is one-to-one
proof
set D = DTConMSA X;
let i be set ; ::_thesis: ( i in the carrier of S implies (Reverse X) . i is one-to-one )
assume i in the carrier of S ; ::_thesis: (Reverse X) . i is one-to-one
then reconsider s = i as SortSymbol of S ;
set f = (Reverse X) . s;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom ((Reverse X) . i) or not x2 in dom ((Reverse X) . i) or not ((Reverse X) . i) . x1 = ((Reverse X) . i) . x2 or x1 = x2 )
assume that
A1: x1 in dom ((Reverse X) . i) and
A2: x2 in dom ((Reverse X) . i) and
A3: ((Reverse X) . i) . x1 = ((Reverse X) . i) . x2 ; ::_thesis: x1 = x2
A4: (Reverse X) . s = Reverse (s,X) by MSAFREE:def_18;
then A5: dom ((Reverse X) . s) = FreeGen (s,X) by FUNCT_2:def_1;
then consider a2 being set such that
A6: a2 in X . s and
A7: x2 = root-tree [a2,s] by A2, MSAFREE:def_15;
A8: [a2,s] in Terminals (DTConMSA X) by A6, MSAFREE:7;
then reconsider t2 = [a2,s] as Symbol of (DTConMSA X) ;
t2 `2 = s by MCART_1:7;
then root-tree t2 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A8;
then root-tree t2 in FreeGen (s,X) by MSAFREE:13;
then A9: ((Reverse X) . s) . x2 = [a2,s] `1 by A4, A7, MSAFREE:def_17
.= a2 ;
consider a1 being set such that
A10: a1 in X . s and
A11: x1 = root-tree [a1,s] by A1, A5, MSAFREE:def_15;
A12: [a1,s] in Terminals (DTConMSA X) by A10, MSAFREE:7;
then reconsider t1 = [a1,s] as Symbol of (DTConMSA X) ;
t1 `2 = s by MCART_1:7;
then root-tree t1 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A12;
then root-tree t1 in FreeGen (s,X) by MSAFREE:13;
then ((Reverse X) . s) . x1 = [a1,s] `1 by A4, A11, MSAFREE:def_17
.= a1 ;
hence x1 = x2 by A3, A11, A7, A9; ::_thesis: verum
end;
hence Reverse X is "1-1" by MSUALG_3:1; ::_thesis: verum
end;
theorem :: MSUALG_9:12
for I being set
for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"
proof
let I be set ; ::_thesis: for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"
let A be V2() V32() ManySortedSet of I; ::_thesis: ex F being ManySortedFunction of I --> NAT,A st F is "onto"
defpred S1[ set , set ] means ex f being Function of NAT,(A . $1) st
( $2 = f & rng f = A . $1 );
A1: for i being set st i in I holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume A2: i in I ; ::_thesis: ex j being set st S1[i,j]
consider f being Function of NAT,(A . i) such that
A3: rng f = A . i by A2, CARD_3:96;
take f ; ::_thesis: S1[i,f]
thus S1[i,f] by A3; ::_thesis: verum
end;
consider F being ManySortedSet of I such that
A4: for i being set st i in I holds
S1[i,F . i] from PBOOLE:sch_3(A1);
F is ManySortedFunction of I --> NAT,A
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or F . i is Element of bool [:((I --> NAT) . i),(A . i):] )
assume i in I ; ::_thesis: F . i is Element of bool [:((I --> NAT) . i),(A . i):]
then ( ex f being Function of NAT,(A . i) st
( F . i = f & rng f = A . i ) & (I --> NAT) . i = NAT ) by A4, FUNCOP_1:7;
hence F . i is Element of bool [:((I --> NAT) . i),(A . i):] ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of I --> NAT,A ;
take F ; ::_thesis: F is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng (F . i) = A . i )
assume i in I ; ::_thesis: rng (F . i) = A . i
then ex f being Function of NAT,(A . i) st
( F . i = f & rng f = A . i ) by A4;
hence rng (F . i) = A . i ; ::_thesis: verum
end;
theorem :: MSUALG_9:13
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g
proof
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g
let A be non-empty MSAlgebra over S; ::_thesis: for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g
let f, g be Element of product the Sorts of A; ::_thesis: ( ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) implies f = g )
assume A1: for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ; ::_thesis: f = g
set X = the Sorts of A;
now__::_thesis:_(_dom_f_=_dom_g_&_(_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x_)_)
thus dom f = dom the Sorts of A by CARD_3:9
.= dom g by CARD_3:9 ; ::_thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; ::_thesis: f . x = g . x
A2: dom (proj ( the Sorts of A,x)) = product the Sorts of A by CARD_3:def_16;
hence f . x = (proj ( the Sorts of A,x)) . f by CARD_3:def_16
.= (proj ( the Sorts of A,x)) . g by A1
.= g . x by A2, CARD_3:def_16 ;
::_thesis: verum
end;
hence f = g by FUNCT_1:2; ::_thesis: verum
end;
theorem :: MSUALG_9:14
for S being non empty non void ManySortedSign
for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
proof
let S be non empty non void ManySortedSign ; ::_thesis: for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let I be non empty set ; ::_thesis: for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let s be Element of S; ::_thesis: for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let A be MSAlgebra-Family of I,S; ::_thesis: for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let f, g be Element of product (Carrier (A,s)); ::_thesis: ( ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) implies f = g )
assume A1: for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ; ::_thesis: f = g
now__::_thesis:_(_dom_f_=_dom_g_&_(_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x_)_)
dom f = dom (Carrier (A,s)) by CARD_3:9;
hence dom f = dom g by CARD_3:9; ::_thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A2: x in dom f ; ::_thesis: f . x = g . x
A3: dom (proj ((Carrier (A,s)),x)) = product (Carrier (A,s)) by CARD_3:def_16;
hence f . x = (proj ((Carrier (A,s)),x)) . f by CARD_3:def_16
.= (proj ((Carrier (A,s)),x)) . g by A1, A2
.= g . x by A3, CARD_3:def_16 ;
::_thesis: verum
end;
hence f = g by FUNCT_1:2; ::_thesis: verum
end;
theorem :: MSUALG_9:15
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let A, B be non-empty MSAlgebra over S; ::_thesis: for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let C be non-empty MSSubAlgebra of A; ::_thesis: for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let h1 be ManySortedFunction of B,C; ::_thesis: ( h1 is_homomorphism B,C implies for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A )
assume A1: h1 is_homomorphism B,C ; ::_thesis: for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
the Sorts of C is ManySortedSubset of the Sorts of A by MSUALG_2:def_9;
then id the Sorts of C is ManySortedFunction of C,A by EXTENS_1:5;
then consider G being ManySortedFunction of C,A such that
A2: G = id the Sorts of C ;
G is_monomorphism C,A by A2, MSUALG_3:22;
then A3: G is_homomorphism C,A by MSUALG_3:def_9;
A4: G ** h1 = h1 by A2, MSUALG_3:4;
let h2 be ManySortedFunction of B,A; ::_thesis: ( h1 = h2 implies h2 is_homomorphism B,A )
assume h1 = h2 ; ::_thesis: h2 is_homomorphism B,A
hence h2 is_homomorphism B,A by A1, A4, A3, MSUALG_3:10; ::_thesis: verum
end;
theorem :: MSUALG_9:16
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
let F be ManySortedFunction of A,B; ::_thesis: ( F is_monomorphism A,B implies A, Image F are_isomorphic )
assume A1: F is_monomorphism A,B ; ::_thesis: A, Image F are_isomorphic
then F is_homomorphism A,B by MSUALG_3:def_9;
then consider G being ManySortedFunction of A,(Image F) such that
A2: G = F and
A3: G is_epimorphism A, Image F by MSUALG_3:21;
take G ; :: according to MSUALG_3:def_11 ::_thesis: G is_isomorphism A, Image F
thus G is_epimorphism A, Image F by A3; :: according to MSUALG_3:def_10 ::_thesis: G is_monomorphism A, Image F
thus G is_homomorphism A, Image F by A3, MSUALG_3:def_8; :: according to MSUALG_3:def_9 ::_thesis: G is "1-1"
thus G is "1-1" by A1, A2, MSUALG_3:def_9; ::_thesis: verum
end;
theorem Th17: :: MSUALG_9:17
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" implies for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x )
assume A1: F is "onto" ; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let t be Element of Args (o,B); ::_thesis: ex y being Element of Args (o,A) st F # y = t
set D = len (the_arity_of o);
defpred S1[ set , set ] means ex y1 being Element of the Sorts of A . ((the_arity_of o) /. $1) st
( (F . ((the_arity_of o) /. $1)) . y1 = t . $1 & $2 = y1 );
A2: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds
ex x being set st S1[k,x]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len (the_arity_of o)) implies ex x being set st S1[k,x] )
assume k in Seg (len (the_arity_of o)) ; ::_thesis: ex x being set st S1[k,x]
then A3: k in dom (the_arity_of o) by FINSEQ_1:def_3;
set s = (the_arity_of o) /. k;
A4: t . k in the Sorts of B . ((the_arity_of o) /. k) by A3, MSUALG_6:2;
rng (F . ((the_arity_of o) /. k)) = the Sorts of B . ((the_arity_of o) /. k) by A1, MSUALG_3:def_3;
then consider y1 being set such that
A5: y1 in the Sorts of A . ((the_arity_of o) /. k) and
A6: (F . ((the_arity_of o) /. k)) . y1 = t . k by A4, FUNCT_2:11;
reconsider y2 = y1 as Element of the Sorts of A . ((the_arity_of o) /. k) by A5;
take y1 ; ::_thesis: S1[k,y1]
take y2 ; ::_thesis: ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 )
thus ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 ) by A6; ::_thesis: verum
end;
consider p being FinSequence such that
A7: dom p = Seg (len (the_arity_of o)) and
A8: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds
S1[k,p . k] from MSUALG_8:sch_1(A2);
A9: len p = len (the_arity_of o) by A7, FINSEQ_1:def_3;
for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k)
proof
let k be Nat; ::_thesis: ( k in dom p implies p . k in the Sorts of A . ((the_arity_of o) /. k) )
assume k in dom p ; ::_thesis: p . k in the Sorts of A . ((the_arity_of o) /. k)
then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st
( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A7, A8;
hence p . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum
end;
then reconsider p = p as Element of Args (o,A) by A9, MSAFREE2:5;
set fp = F # p;
take p ; ::_thesis: F # p = t
reconsider E = the Sorts of B * (the_arity_of o) as V2() ManySortedSet of dom (the_arity_of o) ;
A10: Args (o,B) = product E by PRALG_2:3;
A11: Seg (len (the_arity_of o)) = dom (the_arity_of o) by FINSEQ_1:def_3
.= dom ( the Sorts of B * (the_arity_of o)) by PRALG_2:3
.= dom t by A10, CARD_3:9 ;
A12: for k being Nat st k in dom t holds
(F # p) . k = t . k
proof
let k be Nat; ::_thesis: ( k in dom t implies (F # p) . k = t . k )
assume A13: k in dom t ; ::_thesis: (F # p) . k = t . k
then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st
( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A11, A8;
hence (F # p) . k = t . k by A11, A7, A13, MSUALG_3:def_6; ::_thesis: verum
end;
dom (F # p) = dom ( the Sorts of B * (the_arity_of o)) by A10, CARD_3:9
.= dom t by A10, CARD_3:9 ;
hence F # p = t by A12, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th18: :: MSUALG_9:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
let x be Element of Args (o,A); ::_thesis: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)
(Den (o,A)) . x is Element of the Sorts of A . ( the ResultSort of S . o) by FUNCT_2:15;
hence (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: verum
end;
theorem Th19: :: MSUALG_9:19
for S being non empty non void ManySortedSign
for A, B, C being non-empty MSAlgebra over S
for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B, C being non-empty MSAlgebra over S
for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let A, B, C be non-empty MSAlgebra over S; ::_thesis: for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let F1 be ManySortedFunction of A,B; ::_thesis: for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let F2 be ManySortedFunction of A,C; ::_thesis: ( F1 is_epimorphism A,B & F2 is_homomorphism A,C implies for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C )
assume that
A1: F1 is_epimorphism A,B and
A2: F2 is_homomorphism A,C ; ::_thesis: for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let G be ManySortedFunction of B,C; ::_thesis: ( G ** F1 = F2 implies G is_homomorphism B,C )
assume A3: G ** F1 = F2 ; ::_thesis: G is_homomorphism B,C
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,B) = {} or for b1 being Element of Args (o,B) holds (G . (the_result_sort_of o)) . ((Den (o,B)) . b1) = (Den (o,C)) . (G # b1) )
assume Args (o,B) <> {} ; ::_thesis: for b1 being Element of Args (o,B) holds (G . (the_result_sort_of o)) . ((Den (o,B)) . b1) = (Den (o,C)) . (G # b1)
let x be Element of Args (o,B); ::_thesis: (G . (the_result_sort_of o)) . ((Den (o,B)) . x) = (Den (o,C)) . (G # x)
F1 is "onto" by A1, MSUALG_3:def_8;
then consider y being Element of Args (o,A) such that
A4: F1 # y = x by Th17;
set r = the_result_sort_of o;
F1 is_homomorphism A,B by A1, MSUALG_3:def_8;
then A5: (F1 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,B)) . x by A4, MSUALG_3:def_7;
A6: (F2 . (the_result_sort_of o)) . ((Den (o,A)) . y) = ((G . (the_result_sort_of o)) * (F1 . (the_result_sort_of o))) . ((Den (o,A)) . y) by A3, MSUALG_3:2
.= (G . (the_result_sort_of o)) . ((Den (o,B)) . x) by A5, Th18, FUNCT_2:15 ;
(F2 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,C)) . ((G ** F1) # y) by A2, A3, MSUALG_3:def_7
.= (Den (o,C)) . (G # x) by A4, MSUALG_3:8 ;
hence (G . (the_result_sort_of o)) . ((Den (o,B)) . x) = (Den (o,C)) . (G # x) by A6; ::_thesis: verum
end;
definition
let I be set ;
let A be ManySortedSet of I;
let B, C be V2() ManySortedSet of I;
let F be ManySortedFunction of A,[|B,C|];
func Mpr1 F -> ManySortedFunction of A,B means :Def1: :: MSUALG_9:def 1
for i being set st i in I holds
it . i = pr1 (F . i);
existence
ex b1 being ManySortedFunction of A,B st
for i being set st i in I holds
b1 . i = pr1 (F . i)
proof
deffunc H1( set ) -> set = pr1 (F . $1);
consider X being ManySortedSet of I such that
A1: for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4();
X is ManySortedFunction of A,B
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or X . i is Element of bool [:(A . i),(B . i):] )
assume A2: i in I ; ::_thesis: X . i is Element of bool [:(A . i),(B . i):]
then reconsider Bi = B . i as non empty set ;
A3: X . i = pr1 (F . i) by A1, A2;
then reconsider Xi = X . i as Function ;
A4: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15;
A5: rng Xi c= Bi
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Xi or q in Bi )
assume q in rng Xi ; ::_thesis: q in Bi
then consider x being set such that
A6: x in dom Xi and
A7: Xi . x = q by FUNCT_1:def_3;
x in dom (F . i) by A3, A6, MCART_1:def_12;
then A8: ( Xi . x = ((F . i) . x) `1 & (F . i) . x in rng (F . i) ) by A3, FUNCT_1:def_3, MCART_1:def_12;
rng (F . i) c= [|B,C|] . i by A4, RELAT_1:def_19;
then A9: rng (F . i) c= [:(B . i),(C . i):] by A2, PBOOLE:def_16;
assume not q in Bi ; ::_thesis: contradiction
hence contradiction by A7, A9, A8, MCART_1:10; ::_thesis: verum
end;
dom (F . i) = A . i by A2, A4, FUNCT_2:def_1;
then dom Xi = A . i by A3, MCART_1:def_12;
hence X . i is Element of bool [:(A . i),(B . i):] by A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider X = X as ManySortedFunction of A,B ;
take X ; ::_thesis: for i being set st i in I holds
X . i = pr1 (F . i)
thus for i being set st i in I holds
X . i = pr1 (F . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of A,B st ( for i being set st i in I holds
b1 . i = pr1 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr1 (F . i) ) holds
b1 = b2
proof
let M, N be ManySortedFunction of A,B; ::_thesis: ( ( for i being set st i in I holds
M . i = pr1 (F . i) ) & ( for i being set st i in I holds
N . i = pr1 (F . i) ) implies M = N )
assume that
A10: for i being set st i in I holds
M . i = pr1 (F . i) and
A11: for i being set st i in I holds
N . i = pr1 (F . i) ; ::_thesis: M = N
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
M_._i_=_N_._i
let i be set ; ::_thesis: ( i in I implies M . i = N . i )
assume A12: i in I ; ::_thesis: M . i = N . i
hence M . i = pr1 (F . i) by A10
.= N . i by A11, A12 ;
::_thesis: verum
end;
hence M = N by PBOOLE:3; ::_thesis: verum
end;
func Mpr2 F -> ManySortedFunction of A,C means :Def2: :: MSUALG_9:def 2
for i being set st i in I holds
it . i = pr2 (F . i);
existence
ex b1 being ManySortedFunction of A,C st
for i being set st i in I holds
b1 . i = pr2 (F . i)
proof
deffunc H1( set ) -> set = pr2 (F . $1);
consider X being ManySortedSet of I such that
A13: for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4();
X is ManySortedFunction of A,C
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or X . i is Element of bool [:(A . i),(C . i):] )
assume A14: i in I ; ::_thesis: X . i is Element of bool [:(A . i),(C . i):]
then reconsider Ci = C . i as non empty set ;
A15: X . i = pr2 (F . i) by A13, A14;
then reconsider Xi = X . i as Function ;
A16: F . i is Function of (A . i),([|B,C|] . i) by A14, PBOOLE:def_15;
A17: rng Xi c= Ci
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Xi or q in Ci )
assume q in rng Xi ; ::_thesis: q in Ci
then consider x being set such that
A18: x in dom Xi and
A19: Xi . x = q by FUNCT_1:def_3;
x in dom (F . i) by A15, A18, MCART_1:def_13;
then A20: ( Xi . x = ((F . i) . x) `2 & (F . i) . x in rng (F . i) ) by A15, FUNCT_1:def_3, MCART_1:def_13;
rng (F . i) c= [|B,C|] . i by A16, RELAT_1:def_19;
then A21: rng (F . i) c= [:(B . i),(C . i):] by A14, PBOOLE:def_16;
assume not q in Ci ; ::_thesis: contradiction
hence contradiction by A19, A21, A20, MCART_1:10; ::_thesis: verum
end;
dom (F . i) = A . i by A14, A16, FUNCT_2:def_1;
then dom Xi = A . i by A15, MCART_1:def_13;
hence X . i is Element of bool [:(A . i),(C . i):] by A17, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider X = X as ManySortedFunction of A,C ;
take X ; ::_thesis: for i being set st i in I holds
X . i = pr2 (F . i)
thus for i being set st i in I holds
X . i = pr2 (F . i) by A13; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of A,C st ( for i being set st i in I holds
b1 . i = pr2 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr2 (F . i) ) holds
b1 = b2
proof
let M, N be ManySortedFunction of A,C; ::_thesis: ( ( for i being set st i in I holds
M . i = pr2 (F . i) ) & ( for i being set st i in I holds
N . i = pr2 (F . i) ) implies M = N )
assume that
A22: for i being set st i in I holds
M . i = pr2 (F . i) and
A23: for i being set st i in I holds
N . i = pr2 (F . i) ; ::_thesis: M = N
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
M_._i_=_N_._i
let i be set ; ::_thesis: ( i in I implies M . i = N . i )
assume A24: i in I ; ::_thesis: M . i = N . i
hence M . i = pr2 (F . i) by A22
.= N . i by A23, A24 ;
::_thesis: verum
end;
hence M = N by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Mpr1 MSUALG_9:def_1_:_
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,B holds
( b6 = Mpr1 F iff for i being set st i in I holds
b6 . i = pr1 (F . i) );
:: deftheorem Def2 defines Mpr2 MSUALG_9:def_2_:_
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,C holds
( b6 = Mpr2 F iff for i being set st i in I holds
b6 . i = pr2 (F . i) );
theorem :: MSUALG_9:20
for I, a being set
for A being ManySortedSet of I
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
proof
let I, a be set ; ::_thesis: for A being ManySortedSet of I
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
let F be ManySortedFunction of A,[|(I --> {a}),(I --> {a})|]; ::_thesis: Mpr1 F = Mpr2 F
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(Mpr1_F)_._i_=_(Mpr2_F)_._i
let i be set ; ::_thesis: ( i in I implies (Mpr1 F) . i = (Mpr2 F) . i )
A1: dom (pr2 (F . i)) = dom (F . i) by MCART_1:def_13;
assume A2: i in I ; ::_thesis: (Mpr1 F) . i = (Mpr2 F) . i
A3: now__::_thesis:_for_y_being_set_st_y_in_dom_(F_._i)_holds_
(pr2_(F_._i))_._y_=_((F_._i)_._y)_`1
let y be set ; ::_thesis: ( y in dom (F . i) implies (pr2 (F . i)) . y = ((F . i) . y) `1 )
assume A4: y in dom (F . i) ; ::_thesis: (pr2 (F . i)) . y = ((F . i) . y) `1
A5: (F . i) . y in rng (F . i) by A4, FUNCT_1:def_3;
F . i is Function of (A . i),([|(I --> {a}),(I --> {a})|] . i) by A2, PBOOLE:def_15;
then rng (F . i) c= [|(I --> {a}),(I --> {a})|] . i by RELAT_1:def_19;
then A6: rng (F . i) c= [:((I --> {a}) . i),((I --> {a}) . i):] by A2, PBOOLE:def_16;
then ((F . i) . y) `1 in (I --> {a}) . i by A5, MCART_1:10;
then A7: ((F . i) . y) `1 in {a} by A2, FUNCOP_1:7;
((F . i) . y) `2 in (I --> {a}) . i by A5, A6, MCART_1:10;
then A8: ((F . i) . y) `2 in {a} by A2, FUNCOP_1:7;
thus (pr2 (F . i)) . y = ((F . i) . y) `2 by A4, MCART_1:def_13
.= a by A8, TARSKI:def_1
.= ((F . i) . y) `1 by A7, TARSKI:def_1 ; ::_thesis: verum
end;
( (Mpr1 F) . i = pr1 (F . i) & (Mpr2 F) . i = pr2 (F . i) ) by A2, Def1, Def2;
hence (Mpr1 F) . i = (Mpr2 F) . i by A1, A3, MCART_1:def_12; ::_thesis: verum
end;
hence Mpr1 F = Mpr2 F by PBOOLE:3; ::_thesis: verum
end;
theorem :: MSUALG_9:21
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( F is "onto" implies Mpr1 F is "onto" )
assume A1: F is "onto" ; ::_thesis: Mpr1 F is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((Mpr1 F) . i) = B . i )
assume A2: i in I ; ::_thesis: rng ((Mpr1 F) . i) = B . i
then reconsider m = (Mpr1 F) . i as Function of (A . i),(B . i) by PBOOLE:def_15;
rng m = B . i
proof
thus rng m c= B . i ; :: according to XBOOLE_0:def_10 ::_thesis: B . i c= rng m
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B . i or a in rng m )
assume A3: a in B . i ; ::_thesis: a in rng m
consider z being set such that
A4: z in [|B,C|] . i by A2, XBOOLE_0:def_1;
set p = [a,(z `2)];
z in [:(B . i),(C . i):] by A2, A4, PBOOLE:def_16;
then A5: [a,(z `2)] `2 in C . i by MCART_1:10;
[a,(z `2)] `1 in B . i by A3;
then [a,(z `2)] in [:(B . i),(C . i):] by A5, MCART_1:11;
then A6: [a,(z `2)] in [|B,C|] . i by A2, PBOOLE:def_16;
A7: dom m = A . i by A2, FUNCT_2:def_1;
A8: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15;
then A9: dom (F . i) = A . i by A2, FUNCT_2:def_1;
rng (F . i) = [|B,C|] . i by A1, A2, MSUALG_3:def_3;
then consider b being set such that
A10: b in A . i and
A11: (F . i) . b = [a,(z `2)] by A8, A6, FUNCT_2:11;
m . b = (pr1 (F . i)) . b by A2, Def1
.= [a,(z `2)] `1 by A10, A11, A9, MCART_1:def_12
.= a ;
hence a in rng m by A10, A7, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng ((Mpr1 F) . i) = B . i ; ::_thesis: verum
end;
theorem :: MSUALG_9:22
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( F is "onto" implies Mpr2 F is "onto" )
assume A1: F is "onto" ; ::_thesis: Mpr2 F is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((Mpr2 F) . i) = C . i )
assume A2: i in I ; ::_thesis: rng ((Mpr2 F) . i) = C . i
then reconsider m = (Mpr2 F) . i as Function of (A . i),(C . i) by PBOOLE:def_15;
rng m = C . i
proof
thus rng m c= C . i ; :: according to XBOOLE_0:def_10 ::_thesis: C . i c= rng m
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in C . i or a in rng m )
assume A3: a in C . i ; ::_thesis: a in rng m
consider z being set such that
A4: z in [|B,C|] . i by A2, XBOOLE_0:def_1;
set p = [(z `1),a];
z in [:(B . i),(C . i):] by A2, A4, PBOOLE:def_16;
then A5: [(z `1),a] `1 in B . i by MCART_1:10;
[(z `1),a] `2 in C . i by A3;
then [(z `1),a] in [:(B . i),(C . i):] by A5, MCART_1:11;
then A6: [(z `1),a] in [|B,C|] . i by A2, PBOOLE:def_16;
A7: dom m = A . i by A2, FUNCT_2:def_1;
A8: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15;
then A9: dom (F . i) = A . i by A2, FUNCT_2:def_1;
rng (F . i) = [|B,C|] . i by A1, A2, MSUALG_3:def_3;
then consider b being set such that
A10: b in A . i and
A11: (F . i) . b = [(z `1),a] by A8, A6, FUNCT_2:11;
m . b = (pr2 (F . i)) . b by A2, Def2
.= [(z `1),a] `2 by A10, A11, A9, MCART_1:def_13
.= a ;
hence a in rng m by A10, A7, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng ((Mpr2 F) . i) = C . i ; ::_thesis: verum
end;
theorem :: MSUALG_9:23
for I being set
for A, M being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
proof
let I be set ; ::_thesis: for A, M being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let A, M be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( M in doms F implies for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] )
assume A1: M in doms F ; ::_thesis: for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let i be set ; ::_thesis: ( i in I implies (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] )
assume A2: i in I ; ::_thesis: (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
then M . i in (doms F) . i by A1, PBOOLE:def_1;
then A3: M . i in dom (F . i) by A2, MSSUBFAM:14;
A is_transformable_to [|B,C|]
proof
let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in I or not [|B,C|] . i = {} or A . i = {} )
assume i in I ; ::_thesis: ( not [|B,C|] . i = {} or A . i = {} )
hence ( not [|B,C|] . i = {} or A . i = {} ) ; ::_thesis: verum
end;
then M in A by A1, MSSUBFAM:17;
then F .. M in [|B,C|] by CLOSURE1:3;
then (F .. M) . i in [|B,C|] . i by A2, PBOOLE:def_1;
then (F .. M) . i in [:(B . i),(C . i):] by A2, PBOOLE:def_16;
then A4: (F . i) . (M . i) in [:(B . i),(C . i):] by A2, PRALG_1:def_18;
set z = (F . i) . (M . i);
(Mpr2 F) . i = pr2 (F . i) by A2, Def2;
then A5: ((Mpr2 F) .. M) . i = (pr2 (F . i)) . (M . i) by A2, PRALG_1:def_18
.= ((F . i) . (M . i)) `2 by A3, MCART_1:def_13 ;
(Mpr1 F) . i = pr1 (F . i) by A2, Def1;
then ((Mpr1 F) .. M) . i = (pr1 (F . i)) . (M . i) by A2, PRALG_1:def_18
.= ((F . i) . (M . i)) `1 by A3, MCART_1:def_12 ;
then (F . i) . (M . i) = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A4, A5, MCART_1:21;
hence (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A2, PRALG_1:def_18; ::_thesis: verum
end;
begin
registration
let S be non empty ManySortedSign ;
cluster the Sorts of (Trivial_Algebra S) -> V2() V32() ;
coherence
( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty )
proof
ex A being ManySortedSet of the carrier of S st {A} = the carrier of S --> {0} by Th5;
hence ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty ) by MSAFREE2:def_12; ::_thesis: verum
end;
end;
registration
let S be non empty ManySortedSign ;
cluster Trivial_Algebra S -> non-empty finite-yielding ;
coherence
( Trivial_Algebra S is finite-yielding & Trivial_Algebra S is non-empty )
proof
thus the Sorts of (Trivial_Algebra S) is V32() ; :: according to MSAFREE2:def_11 ::_thesis: Trivial_Algebra S is non-empty
let i be set ; :: according to MSUALG_1:def_3,PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not the Sorts of (Trivial_Algebra S) . i is empty )
assume i in the carrier of S ; ::_thesis: not the Sorts of (Trivial_Algebra S) . i is empty
hence not the Sorts of (Trivial_Algebra S) . i is empty ; ::_thesis: verum
end;
end;
theorem Th24: :: MSUALG_9:24
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
let A be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
let F be ManySortedFunction of A,(Trivial_Algebra S); ::_thesis: for o being OperSymbol of S
for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,A) holds
( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
let x be Element of Args (o,A); ::_thesis: ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )
set I = the carrier of S;
set SA = the Sorts of A;
set T = Trivial_Algebra S;
set ST = the Sorts of (Trivial_Algebra S);
set r = the_result_sort_of o;
consider i being set such that
A1: i in the carrier of S and
A2: Result (o,(Trivial_Algebra S)) = the Sorts of (Trivial_Algebra S) . i by PBOOLE:138;
reconsider d = (Den (o,A)) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_2:15;
consider XX being ManySortedSet of the carrier of S such that
A3: {XX} = the carrier of S --> {0} by Th5;
A4: the Sorts of (Trivial_Algebra S) = {XX} by A3, MSAFREE2:def_12;
then A5: the Sorts of (Trivial_Algebra S) . (the_result_sort_of o) = {0} by A3, FUNCOP_1:7;
thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (F . (the_result_sort_of o)) . d
.= 0 by A5, TARSKI:def_1 ; ::_thesis: (Den (o,(Trivial_Algebra S))) . (F # x) = 0
the Sorts of (Trivial_Algebra S) . i = {0} by A3, A4, A1, FUNCOP_1:7;
hence (Den (o,(Trivial_Algebra S))) . (F # x) = 0 by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th25: :: MSUALG_9:25
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
let A be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
let F be ManySortedFunction of A,(Trivial_Algebra S); ::_thesis: F is_epimorphism A, Trivial_Algebra S
set I = the carrier of S;
consider XX being ManySortedSet of the carrier of S such that
A1: {XX} = the carrier of S --> {0} by Th5;
thus F is_homomorphism A, Trivial_Algebra S :: according to MSUALG_3:def_8 ::_thesis: F is "onto"
proof
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,A) = {} or for b1 being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1) )
assume Args (o,A) <> {} ; ::_thesis: for b1 being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1)
let x be Element of Args (o,A); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,(Trivial_Algebra S))) . (F # x)
thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 by Th24
.= (Den (o,(Trivial_Algebra S))) . (F # x) by Th24 ; ::_thesis: verum
end;
the Sorts of (Trivial_Algebra S) = {XX} by A1, MSAFREE2:def_12;
hence F is "onto" by Th9; ::_thesis: verum
end;
theorem :: MSUALG_9:26
for S being non empty non void ManySortedSign
for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds
A, Trivial_Algebra S are_isomorphic
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds
A, Trivial_Algebra S are_isomorphic
let A be MSAlgebra over S; ::_thesis: ( ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} implies A, Trivial_Algebra S are_isomorphic )
assume A1: ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} ; ::_thesis: A, Trivial_Algebra S are_isomorphic
set I = the carrier of S;
set SB = the Sorts of A;
set ST = the Sorts of (Trivial_Algebra S);
consider X being ManySortedSet of the carrier of S such that
A2: the Sorts of A = {X} by A1;
set F = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S);
reconsider F1 = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) as ManySortedFunction of {X}, the Sorts of (Trivial_Algebra S) by A2;
take the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) ; :: according to MSUALG_3:def_11 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_isomorphism A, Trivial_Algebra S
A is non-empty by A2, MSUALG_1:def_3;
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_epimorphism A, Trivial_Algebra S by Th25; :: according to MSUALG_3:def_10 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_monomorphism A, Trivial_Algebra S
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_homomorphism A, Trivial_Algebra S by MSUALG_3:def_8; :: according to MSUALG_3:def_9 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1"
F1 is "1-1" by Th10;
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1" ; ::_thesis: verum
end;
begin
theorem :: MSUALG_9:27
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
let C be MSCongruence of A; ::_thesis: C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
set SF = the Sorts of A;
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of S or C . i c= [| the Sorts of A, the Sorts of A|] . i )
assume A1: i in the carrier of S ; ::_thesis: C . i c= [| the Sorts of A, the Sorts of A|] . i
C . i is Relation of ( the Sorts of A . i),( the Sorts of A . i) by A1, MSUALG_4:def_1;
then C . i c= [:( the Sorts of A . i),( the Sorts of A . i):] ;
hence C . i c= [| the Sorts of A, the Sorts of A|] . i by A1, PBOOLE:def_16; ::_thesis: verum
end;
theorem :: MSUALG_9:28
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let A be non-empty MSAlgebra over S; ::_thesis: for R being Subset of (CongrLatt A)
for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let R be Subset of (CongrLatt A); ::_thesis: for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
let F be SubsetFamily of [| the Sorts of A, the Sorts of A|]; ::_thesis: ( R = F implies meet |:F:| is MSCongruence of A )
assume A1: R = F ; ::_thesis: meet |:F:| is MSCongruence of A
set R0 = meet |:F:|;
set SF = the Sorts of A;
set I = the carrier of S;
percases ( not F is empty or F is empty ) ;
suppose not F is empty ; ::_thesis: meet |:F:| is MSCongruence of A
then reconsider F1 = F as non empty SubsetFamily of [| the Sorts of A, the Sorts of A|] ;
A2: F1 c= the carrier of (EqRelLatt the Sorts of A)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in the carrier of (EqRelLatt the Sorts of A) )
assume q in F1 ; ::_thesis: q in the carrier of (EqRelLatt the Sorts of A)
then q is MSCongruence of A by A1, MSUALG_5:def_6;
hence q in the carrier of (EqRelLatt the Sorts of A) by MSUALG_5:def_5; ::_thesis: verum
end;
then A3: meet |:F:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_7:8;
reconsider R0 = meet |:F:| as ManySortedRelation of A by A2, MSUALG_7:8;
R0 is MSEquivalence-like
proof
let i be set ; :: according to MSUALG_4:def_2,MSUALG_4:def_3 ::_thesis: for b1 being Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] holds
( not i in the carrier of S or not R0 . i = b1 or b1 is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
let R be Relation of ( the Sorts of A . i); ::_thesis: ( not i in the carrier of S or not R0 . i = R or R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
assume ( i in the carrier of S & R0 . i = R ) ; ::_thesis: R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
hence R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] by A3, MSUALG_4:def_2; ::_thesis: verum
end;
then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of A ;
now__::_thesis:_for_o_being_OperSymbol_of_S
for_a,_b_being_Element_of_Args_(o,A)_st_(_for_n_being_Nat_st_n_in_dom_a_holds_
[(a_._n),(b_._n)]_in_R0_._((the_arity_of_o)_/._n)_)_holds_
[((Den_(o,A))_._a),((Den_(o,A))_._b)]_in_R0_._(the_result_sort_of_o)
let o be OperSymbol of S; ::_thesis: for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)
let a, b be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) )
assume A4: for n being Nat st n in dom a holds
[(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o)
set r = the_result_sort_of o;
consider Q being Subset-Family of ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of o)) such that
A5: Q = |:F1:| . (the_result_sort_of o) and
A6: R0 . (the_result_sort_of o) = Intersect Q by MSSUBFAM:def_1;
A7: Q = { (s . (the_result_sort_of o)) where s is Element of Bool [| the Sorts of A, the Sorts of A|] : s in F1 } by A5, CLOSURE2:14;
now__::_thesis:_for_Y_being_set_st_Y_in_Q_holds_
[((Den_(o,A))_._a),((Den_(o,A))_._b)]_in_Y
let Y be set ; ::_thesis: ( Y in Q implies [((Den (o,A)) . a),((Den (o,A)) . b)] in Y )
assume Y in Q ; ::_thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in Y
then consider s being Element of Bool [| the Sorts of A, the Sorts of A|] such that
A8: Y = s . (the_result_sort_of o) and
A9: s in F1 by A7;
reconsider s = s as MSCongruence of A by A1, A9, MSUALG_5:def_6;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_a_holds_
[(a_._n),(b_._n)]_in_s_._((the_arity_of_o)_/._n)
let n be Nat; ::_thesis: ( n in dom a implies [(a . n),(b . n)] in s . ((the_arity_of o) /. n) )
assume A10: n in dom a ; ::_thesis: [(a . n),(b . n)] in s . ((the_arity_of o) /. n)
set t = (the_arity_of o) /. n;
consider G being Subset-Family of ([| the Sorts of A, the Sorts of A|] . ((the_arity_of o) /. n)) such that
A11: G = |:F1:| . ((the_arity_of o) /. n) and
A12: R0 . ((the_arity_of o) /. n) = Intersect G by MSSUBFAM:def_1;
G = { (j . ((the_arity_of o) /. n)) where j is Element of Bool [| the Sorts of A, the Sorts of A|] : j in F1 } by A11, CLOSURE2:14;
then A13: s . ((the_arity_of o) /. n) in G by A9;
[(a . n),(b . n)] in Intersect G by A4, A10, A12;
then [(a . n),(b . n)] in meet G by A11, SETFAM_1:def_9;
hence [(a . n),(b . n)] in s . ((the_arity_of o) /. n) by A13, SETFAM_1:def_1; ::_thesis: verum
end;
hence [((Den (o,A)) . a),((Den (o,A)) . b)] in Y by A8, MSUALG_4:def_4; ::_thesis: verum
end;
then [((Den (o,A)) . a),((Den (o,A)) . b)] in meet Q by A5, SETFAM_1:def_1;
hence [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) by A5, A6, SETFAM_1:def_9; ::_thesis: verum
end;
hence meet |:F:| is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum
end;
suppose F is empty ; ::_thesis: meet |:F:| is MSCongruence of A
then |:F:| = [[0]] the carrier of S by CLOSURE2:def_3;
then meet |:F:| = [| the Sorts of A, the Sorts of A|] by MSSUBFAM:41;
hence meet |:F:| is MSCongruence of A by MSUALG_5:18; ::_thesis: verum
end;
end;
end;
theorem :: MSUALG_9:29
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
let C be MSCongruence of A; ::_thesis: ( C = [| the Sorts of A, the Sorts of A|] implies the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} )
assume A1: C = [| the Sorts of A, the Sorts of A|] ; ::_thesis: the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
the_Sorts_of_(QuotMSAlg_(A,C))_._i_=_{_the_Sorts_of_A}_._i
let i be set ; ::_thesis: ( i in the carrier of S implies the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i )
assume i in the carrier of S ; ::_thesis: the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i
then reconsider s = i as Element of S ;
A2: C . s = [:( the Sorts of A . s),( the Sorts of A . s):] by A1, PBOOLE:def_16
.= nabla ( the Sorts of A . s) by EQREL_1:def_1 ;
thus the Sorts of (QuotMSAlg (A,C)) . i = Class (C . s) by MSUALG_4:def_6
.= {( the Sorts of A . s)} by A2, Th4
.= { the Sorts of A} . i by PZFMISC1:def_1 ; ::_thesis: verum
end;
hence the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} by PBOOLE:3; ::_thesis: verum
end;
theorem Th30: :: MSUALG_9:30
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F
let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F
let F be ManySortedFunction of A,B; ::_thesis: ( F is_homomorphism A,B implies (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F )
assume A1: F is_homomorphism A,B ; ::_thesis: (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
((MSHomQuot_F)_**_(MSNat_Hom_(A,(MSCng_F))))_._i_=_F_._i
let i be set ; ::_thesis: ( i in the carrier of S implies ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = F . i )
assume i in the carrier of S ; ::_thesis: ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = F . i
then reconsider s = i as SortSymbol of S ;
reconsider h = MSHomQuot (F,s) as Function of ((Class (MSCng F)) . s),( the Sorts of B . s) ;
reconsider f = h * (MSNat_Hom (A,(MSCng F),s)) as Function of ( the Sorts of A . s),( the Sorts of B . s) ;
A2: for c being Element of the Sorts of A . s holds f . c = (F . s) . c
proof
let c be Element of the Sorts of A . s; ::_thesis: f . c = (F . s) . c
thus f . c = h . ((MSNat_Hom (A,(MSCng F),s)) . c) by FUNCT_2:15
.= h . (Class (((MSCng F) . s),c)) by MSUALG_4:def_15
.= h . (Class ((MSCng (F,s)),c)) by A1, MSUALG_4:def_18
.= (F . s) . c by A1, MSUALG_4:def_19 ; ::_thesis: verum
end;
thus ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = ((MSHomQuot F) . s) * ((MSNat_Hom (A,(MSCng F))) . s) by MSUALG_3:2
.= (MSHomQuot (F,s)) * ((MSNat_Hom (A,(MSCng F))) . s) by MSUALG_4:def_20
.= (MSHomQuot (F,s)) * (MSNat_Hom (A,(MSCng F),s)) by MSUALG_4:def_16
.= F . i by A2, FUNCT_2:63 ; ::_thesis: verum
end;
hence (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F by PBOOLE:3; ::_thesis: verum
end;
theorem Th31: :: MSUALG_9:31
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
let C be MSCongruence of A; ::_thesis: for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
let s be SortSymbol of S; ::_thesis: for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)
let a be Element of the Sorts of (QuotMSAlg (A,C)) . s; ::_thesis: ex x being Element of the Sorts of A . s st a = Class (C,x)
a in (Class C) . s ;
then a in Class (C . s) by MSUALG_4:def_6;
then consider t being set such that
A1: t in the Sorts of A . s and
A2: a = Class ((C . s),t) by EQREL_1:def_3;
reconsider t = t as Element of the Sorts of A . s by A1;
take t ; ::_thesis: a = Class (C,t)
thus a = Class (C,t) by A2; ::_thesis: verum
end;
theorem :: MSUALG_9:32
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
let A be MSAlgebra over S; ::_thesis: for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
let C1, C2 be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C1 c= C2 implies for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) )
assume A1: C1 c= C2 ; ::_thesis: for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
let i be Element of S; ::_thesis: for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
let x, y be Element of the Sorts of A . i; ::_thesis: ( [x,y] in C1 . i implies ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) )
assume A2: [x,y] in C1 . i ; ::_thesis: ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )
field (C1 . i) = the Sorts of A . i by ORDERS_1:12;
then A3: C1 . i is_transitive_in the Sorts of A . i by RELAT_2:def_16;
A4: C1 . i c= C2 . i by A1, PBOOLE:def_2;
thus Class (C1,x) c= Class (C2,y) ::_thesis: ( A is non-empty implies Class (C1,y) c= Class (C2,x) )
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (C1,x) or q in Class (C2,y) )
assume A5: q in Class (C1,x) ; ::_thesis: q in Class (C2,y)
then [q,x] in C1 . i by EQREL_1:19;
then [q,y] in C1 . i by A2, A3, A5, RELAT_2:def_8;
hence q in Class (C2,y) by A4, EQREL_1:19; ::_thesis: verum
end;
assume A is non-empty ; ::_thesis: Class (C1,y) c= Class (C2,x)
then reconsider B = A as non-empty MSAlgebra over S ;
field (C1 . i) = the Sorts of A . i by ORDERS_1:12;
then C1 . i is_symmetric_in the Sorts of B . i by RELAT_2:def_11;
then A6: [y,x] in C1 . i by A2, RELAT_2:def_3;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (C1,y) or q in Class (C2,x) )
assume A7: q in Class (C1,y) ; ::_thesis: q in Class (C2,x)
[q,y] in C1 . i by A7, EQREL_1:19;
then [q,x] in C1 . i by A3, A7, A6, RELAT_2:def_8;
hence q in Class (C2,x) by A4, EQREL_1:19; ::_thesis: verum
end;
theorem :: MSUALG_9:33
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let C be MSCongruence of A; ::_thesis: for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let s be SortSymbol of S; ::_thesis: for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let x, y be Element of the Sorts of A . s; ::_thesis: ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
set f = (MSNat_Hom (A,C)) . s;
set g = MSNat_Hom (A,C,s);
A1: (MSNat_Hom (A,C)) . s = MSNat_Hom (A,C,s) by MSUALG_4:def_16;
hereby ::_thesis: ( [x,y] in C . s implies ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y )
assume A2: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y ; ::_thesis: [x,y] in C . s
Class ((C . s),x) = (MSNat_Hom (A,C,s)) . x by MSUALG_4:def_15
.= Class ((C . s),y) by A1, A2, MSUALG_4:def_15 ;
hence [x,y] in C . s by EQREL_1:35; ::_thesis: verum
end;
assume A3: [x,y] in C . s ; ::_thesis: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y
thus ((MSNat_Hom (A,C)) . s) . x = Class ((C . s),x) by A1, MSUALG_4:def_15
.= Class ((C . s),y) by A3, EQREL_1:35
.= ((MSNat_Hom (A,C)) . s) . y by A1, MSUALG_4:def_15 ; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_A_being_non-empty_MSAlgebra_over_S
for_C1,_C2_being_MSCongruence_of_A
for_G_being_ManySortedFunction_of_(QuotMSAlg_(A,C1)),(QuotMSAlg_(A,C2))_st_(_for_i_being_Element_of_S
for_x_being_Element_of_the_Sorts_of_(QuotMSAlg_(A,C1))_._i
for_xx_being_Element_of_the_Sorts_of_A_._i_st_x_=_Class_(C1,xx)_holds_
(G_._i)_._x_=_Class_(C2,xx)_)_holds_
G_is_"onto"
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is "onto"
let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) implies G is "onto" )
assume A1: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ; ::_thesis: G is "onto"
thus G is "onto" ::_thesis: verum
proof
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of S or rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i )
set sL = the Sorts of (QuotMSAlg (A,C1));
set sP = the Sorts of (QuotMSAlg (A,C2));
assume i in the carrier of S ; ::_thesis: rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i
then reconsider s = i as SortSymbol of S ;
A2: dom (G . s) = the Sorts of (QuotMSAlg (A,C1)) . s by FUNCT_2:def_1;
rng (G . s) c= the Sorts of (QuotMSAlg (A,C2)) . s ;
hence rng (G . i) c= the Sorts of (QuotMSAlg (A,C2)) . i ; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (QuotMSAlg (A,C2)) . i c= rng (G . i)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Sorts of (QuotMSAlg (A,C2)) . i or q in rng (G . i) )
assume q in the Sorts of (QuotMSAlg (A,C2)) . i ; ::_thesis: q in rng (G . i)
then q in Class (C2 . s) by MSUALG_4:def_6;
then consider a being set such that
A3: a in the Sorts of A . s and
A4: q = Class ((C2 . s),a) by EQREL_1:def_3;
reconsider a = a as Element of the Sorts of A . s by A3;
Class ((C1 . s),a) in Class (C1 . s) by EQREL_1:def_3;
then reconsider x = Class (C1,a) as Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def_6;
(G . s) . x = Class (C2,a) by A1
.= Class ((C2 . s),a) ;
hence q in rng (G . i) by A4, A2, FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem Th34: :: MSUALG_9:34
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
set sL = the Sorts of (QuotMSAlg (A,C1));
let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) implies G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) )
assume A1: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ; ::_thesis: G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(G_**_(MSNat_Hom_(A,C1)))_._i_=_(MSNat_Hom_(A,C2))_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (G ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,C2)) . i )
assume i in the carrier of S ; ::_thesis: (G ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,C2)) . i
then reconsider s = i as SortSymbol of S ;
A2: for c being Element of the Sorts of A . s holds ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = ((MSNat_Hom (A,C2)) . s) . c
proof
let c be Element of the Sorts of A . s; ::_thesis: ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = ((MSNat_Hom (A,C2)) . s) . c
Class ((C1 . s),c) in Class (C1 . s) by EQREL_1:def_3;
then A3: Class (C1,c) is Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def_6;
thus ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = (G . s) . (((MSNat_Hom (A,C1)) . s) . c) by FUNCT_2:15
.= (G . s) . ((MSNat_Hom (A,C1,s)) . c) by MSUALG_4:def_16
.= (G . s) . (Class (C1,c)) by MSUALG_4:def_15
.= Class (C2,c) by A1, A3
.= (MSNat_Hom (A,C2,s)) . c by MSUALG_4:def_15
.= ((MSNat_Hom (A,C2)) . s) . c by MSUALG_4:def_16 ; ::_thesis: verum
end;
thus (G ** (MSNat_Hom (A,C1))) . i = (G . s) * ((MSNat_Hom (A,C1)) . s) by MSUALG_3:2
.= (MSNat_Hom (A,C2)) . i by A2, FUNCT_2:63 ; ::_thesis: verum
end;
hence G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) by PBOOLE:3; ::_thesis: verum
end;
theorem Th35: :: MSUALG_9:35
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) holds
G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
MSNat_Hom (A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3;
then A1: MSNat_Hom (A,C2) is_homomorphism A, QuotMSAlg (A,C2) by MSUALG_3:def_8;
let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ) implies G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) )
assume A2: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(G . i) . x = Class (C2,xx) ; ::_thesis: G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) by A2, Th34;
hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A1, Th19, MSUALG_4:3; :: according to MSUALG_3:def_8 ::_thesis: G is "onto"
thus G is "onto" by A2, Lm1; ::_thesis: verum
end;
theorem :: MSUALG_9:36
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
let F be ManySortedFunction of A,B; ::_thesis: ( F is_homomorphism A,B implies for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) )
assume A1: F is_homomorphism A,B ; ::_thesis: for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
MSHomQuot F is_monomorphism QuotMSAlg (A,(MSCng F)),B by A1, MSUALG_4:4;
then A2: MSHomQuot F is_homomorphism QuotMSAlg (A,(MSCng F)),B by MSUALG_3:def_9;
let C1 be MSCongruence of A; ::_thesis: ( C1 c= MSCng F implies ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) )
assume A3: C1 c= MSCng F ; ::_thesis: ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
set G = MSNat_Hom (A,C1);
set I = the carrier of S;
set sQ = the Sorts of (QuotMSAlg (A,C1));
set sF = the Sorts of (QuotMSAlg (A,(MSCng F)));
defpred S1[ set , set , set ] means ex s being Element of the carrier of S ex xx being Element of the Sorts of A . s st
( $3 = s & $2 = Class (C1,xx) & $1 = Class ((MSCng F),xx) );
A4: for i being set st i in the carrier of S holds
for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
ex y being set st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] )
proof
let i be set ; ::_thesis: ( i in the carrier of S implies for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
ex y being set st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) )
assume i in the carrier of S ; ::_thesis: for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
ex y being set st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] )
then reconsider s = i as Element of the carrier of S ;
let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (A,C1)) . i implies ex y being set st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) )
assume x in the Sorts of (QuotMSAlg (A,C1)) . i ; ::_thesis: ex y being set st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] )
then consider x1 being Element of the Sorts of A . s such that
A5: x = Class (C1,x1) by Th31;
take y = Class ((MSCng F),x1); ::_thesis: ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] )
y in Class ((MSCng F) . s) by EQREL_1:def_3;
hence y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i by MSUALG_4:def_6; ::_thesis: S1[y,x,i]
thus S1[y,x,i] by A5; ::_thesis: verum
end;
consider C12 being ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of (QuotMSAlg (A,(MSCng F))) such that
A6: for i being set st i in the carrier of S holds
ex f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) st
( f = C12 . i & ( for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
S1[f . x,x,i] ) ) from MSSUBFAM:sch_1(A4);
reconsider H = (MSHomQuot F) ** C12 as ManySortedFunction of (QuotMSAlg (A,C1)),B ;
take H ; ::_thesis: ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )
A7: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(C12 . i) . x = Class ((MSCng F),xx)
proof
let i be Element of S; ::_thesis: for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(C12 . i) . x = Class ((MSCng F),xx)
let x be Element of the Sorts of (QuotMSAlg (A,C1)) . i; ::_thesis: for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(C12 . i) . x = Class ((MSCng F),xx)
let xx be Element of the Sorts of A . i; ::_thesis: ( x = Class (C1,xx) implies (C12 . i) . x = Class ((MSCng F),xx) )
assume A8: x = Class (C1,xx) ; ::_thesis: (C12 . i) . x = Class ((MSCng F),xx)
consider f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) such that
A9: f = C12 . i and
A10: for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
S1[f . x,x,i] by A6;
consider s being Element of the carrier of S, x1 being Element of the Sorts of A . s such that
A11: i = s and
A12: x = Class (C1,x1) and
A13: f . x = Class ((MSCng F),x1) by A10;
xx in Class ((C1 . s),x1) by A8, A12, EQREL_1:23;
then A14: [xx,x1] in C1 . s by EQREL_1:19;
C1 . s c= (MSCng F) . s by A3, PBOOLE:def_2;
then xx in Class (((MSCng F) . s),x1) by A14, EQREL_1:19;
hence (C12 . i) . x = Class ((MSCng F),xx) by A9, A11, A13, EQREL_1:23; ::_thesis: verum
end;
then C12 is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,(MSCng F)) by Th35;
then C12 is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,(MSCng F)) by MSUALG_3:def_8;
hence H is_homomorphism QuotMSAlg (A,C1),B by A2, MSUALG_3:10; ::_thesis: F = H ** (MSNat_Hom (A,C1))
A15: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(C12_**_(MSNat_Hom_(A,C1)))_._i_=_(MSNat_Hom_(A,(MSCng_F)))_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (C12 ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,(MSCng F))) . i )
assume i in the carrier of S ; ::_thesis: (C12 ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,(MSCng F))) . i
then reconsider s = i as SortSymbol of S ;
A16: for x being Element of the Sorts of A . s holds ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = ((MSNat_Hom (A,(MSCng F))) . s) . x
proof
let x be Element of the Sorts of A . s; ::_thesis: ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = ((MSNat_Hom (A,(MSCng F))) . s) . x
Class ((C1 . s),x) in Class (C1 . s) by EQREL_1:def_3;
then A17: Class (C1,x) in (Class C1) . s by MSUALG_4:def_6;
thus ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = (C12 . s) . (((MSNat_Hom (A,C1)) . s) . x) by FUNCT_2:15
.= (C12 . s) . ((MSNat_Hom (A,C1,s)) . x) by MSUALG_4:def_16
.= (C12 . s) . (Class (C1,x)) by MSUALG_4:def_15
.= Class ((MSCng F),x) by A7, A17
.= (MSNat_Hom (A,(MSCng F),s)) . x by MSUALG_4:def_15
.= ((MSNat_Hom (A,(MSCng F))) . s) . x by MSUALG_4:def_16 ; ::_thesis: verum
end;
thus (C12 ** (MSNat_Hom (A,C1))) . i = (C12 . s) * ((MSNat_Hom (A,C1)) . s) by MSUALG_3:2
.= (MSNat_Hom (A,(MSCng F))) . i by A16, FUNCT_2:63 ; ::_thesis: verum
end;
thus F = (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) by A1, Th30
.= (MSHomQuot F) ** (C12 ** (MSNat_Hom (A,C1))) by A15, PBOOLE:3
.= H ** (MSNat_Hom (A,C1)) by PBOOLE:140 ; ::_thesis: verum
end;