:: Equations in Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Received May 30, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

theorem Th1: :: EQUATION:1
for A being set
for B, C being non empty set
for f being Function of A,B
for g being Function of B,C st rng (g * f) = C holds
rng g = C
proofend;

theorem :: EQUATION: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
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
proofend;

theorem Th3: :: EQUATION:3
for A, B being non empty set
for C, y being set
for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
proofend;

theorem :: EQUATION:4
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B
proofend;

theorem Th5: :: EQUATION:5
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
proofend;

theorem Th6: :: EQUATION:6
for I being set
for B being V2() ManySortedSet of I
for C being ManySortedSet of I
for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
proofend;

definition
let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
funcF "" A ->  ManySortedSet of I means :Def1: :: EQUATION:def 1
 for i being set st i in I holds
it . i = (F . i) " (A . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (F . i) " (A . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (F . i) " (A . i) ) & ( for i being set st i in I holds
b2 . i = (F . i) " (A . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines "" EQUATION:def_1_:_
 for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F "" A iff for i being set st i in I holds
b4 . i = (F . i) " (A . i) );

theorem :: EQUATION:7
for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B
proofend;

theorem :: EQUATION:8
for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
proofend;

theorem :: EQUATION:9
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B
proofend;

theorem :: EQUATION:10
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
proofend;

theorem :: EQUATION:11
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A
proofend;

theorem :: EQUATION:12
for I being set
for f being ManySortedFunction of I
for X being ManySortedSet of I holds f .:.: X c= rngs f
proofend;

theorem Th13: :: EQUATION:13
for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
proofend;

theorem Th14: :: EQUATION:14
for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f
proofend;

theorem :: EQUATION:15
for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A
proofend;

theorem :: EQUATION:16
for I being set
for A being ManySortedSet of I holds (id A) "" A = A
proofend;

begin

theorem Th17: :: EQUATION:17
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #)
proofend;

theorem Th18: :: EQUATION:18
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args (o,A) holds
x in Args (o,U0)
proofend;

theorem Th19: :: EQUATION:19
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args (o,A) holds
(Den (o,A)) . x = (Den (o,U0)) . x
proofend;

theorem Th20: :: EQUATION:20
for I being set
for S being non empty non void ManySortedSign
for F being MSAlgebra-Family of I,S
for B being MSSubAlgebra of product F
for o being OperSymbol of S
for x being set st x in Args (o,B) holds
( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let B be MSSubAlgebra of A;
func SuperAlgebraSet B ->  set  means :Def2: :: EQUATION:def 2
 for x being set holds
( x in it iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds
( x in b2 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def_2_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being MSSubAlgebra of A
for b4 being set holds
( b4 = SuperAlgebraSet B iff for x being set holds
( x in b4 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) );

registration
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let B be MSSubAlgebra of A;
cluster SuperAlgebraSet B ->  non empty ;
coherence
 not SuperAlgebraSet B is empty
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty & b1 is free )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let X be V2() V29() MSSubset of A;
cluster GenMSAlg X ->  finitely-generated ;
coherence
 GenMSAlg X is finitely-generated
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster strict non-empty finitely-generated for MSSubAlgebra of A;
existence
 ex b1 being MSSubAlgebra of A st
( b1 is strict & b1 is non-empty & b1 is finitely-generated )
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let A be feasible MSAlgebra over S;
cluster feasible for MSSubAlgebra of A;
existence
 ex b1 being MSSubAlgebra of A st b1 is feasible
proofend;
end;

theorem Th21: :: EQUATION:21
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A being MSAlgebra over S
for C being MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} &amp; x = y holds
h # x = g # y
proofend;

theorem Th22: :: EQUATION:22
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A being feasible MSAlgebra over S
for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
proofend;

theorem :: EQUATION:23
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for B being strict non-empty MSAlgebra over S
for G being GeneratorSet of U0
for H being V2() GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G &amp; f is_homomorphism U0,B holds
f is_epimorphism U0,B
proofend;

theorem Th24: :: EQUATION:24
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for W being strict non-empty free MSAlgebra over S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 &amp; G = F ** H )
proofend;

theorem Th25: :: EQUATION:25
for S being non empty non void ManySortedSign
for I being non empty finite set
for A being non-empty MSAlgebra over S
for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds
ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B
proofend;

theorem Th26: :: EQUATION:26
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M &amp; B is MSSubAlgebra of M )
proofend;

theorem :: EQUATION:27
for SG being non empty non void ManySortedSign
for AG being non-empty MSAlgebra over SG
for C being set st C =  {  A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A  }  holds
for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
proofend;

theorem :: EQUATION:28
for S being non empty non void ManySortedSign
for U0 being free feasible MSAlgebra over S
for A being free GeneratorSet of U0
for Z being MSSubset of U0 st Z c= A &amp; GenMSAlg Z is feasible holds
GenMSAlg Z is free
proofend;

begin

definition
let S be non empty non void ManySortedSign ;
func TermAlg S ->  MSAlgebra over S equals :: EQUATION:def 3
 FreeMSA ( the carrier of S --> NAT);
correctness
coherence
FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S;
;
end;

:: deftheorem  defines TermAlg EQUATION:def_3_:_
 for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);

registration
let S be non empty non void ManySortedSign ;
cluster TermAlg S ->  strict non-empty free ;
coherence
 ( TermAlg S is strict &amp; TermAlg S is non-empty &amp; TermAlg S is free ) ;
end;

definition
let S be non empty non void ManySortedSign ;
func Equations S ->  ManySortedSet of the carrier of S equals :: EQUATION:def 4
[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];
correctness
coherence
[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|] is ManySortedSet of the carrier of S;
;
end;

:: deftheorem  defines Equations EQUATION:def_4_:_
 for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];

registration
let S be non empty non void ManySortedSign ;
cluster Equations S -> V2() ;
coherence
 Equations S is non-empty ;
end;

definition
let S be non empty non void ManySortedSign ;
mode EqualSet of S is ManySortedSubset of Equations S;
end;

notation
let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let x, y be Element of the Sorts of (TermAlg S) . s;
synonym x '=' y for [S,s];
end;

definition
let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let x, y be Element of the Sorts of (TermAlg S) . s;
:: original:'='
redefine funcx '=' y ->  Element of (Equations S) . s;
coherence
 '=' is Element of (Equations S) . s
proofend;
end;

theorem Th29: :: EQUATION:29
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s
proofend;

theorem Th30: :: EQUATION:30
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let s be SortSymbol of S;
let e be Element of (Equations S) . s;
predA |= e means :Def5: :: EQUATION:def 5
 for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e `1) = (h . s) . (e `2);
end;

:: deftheorem Def5 defines |= EQUATION:def_5_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds
( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e `1) = (h . s) . (e `2) );

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let E be EqualSet of S;
predA |= E means :Def6: :: EQUATION:def 6
 for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e;
end;

:: deftheorem Def6 defines |= EQUATION:def_6_:_
 for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for E being EqualSet of S holds
( A |= E iff for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e );

theorem Th31: :: EQUATION:31
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
proofend;

theorem :: EQUATION:32
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
proofend;

theorem Th33: :: EQUATION:33
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic &amp; U0 |= e holds
U1 |= e
proofend;

theorem :: EQUATION:34
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for E being EqualSet of S st U0,U1 are_isomorphic &amp; U0 |= E holds
U1 |= E
proofend;

theorem Th35: :: EQUATION:35
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
proofend;

theorem :: EQUATION:36
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg (U0,R) |= E
proofend;

Lm1:  for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
proofend;

theorem Th37: :: EQUATION:37
for I being set
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i &amp; A |= e ) ) holds
product F |= e
proofend;

theorem :: EQUATION:38
for I being set
for S being non empty non void ManySortedSign
for E being EqualSet of S
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i &amp; A |= E ) ) holds
product F |= E
proofend;