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

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

proof end;

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"

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;

func F "" A -> ManySortedSet of I means :Def1: :: EQUATION:def 1
for i being object st i in I holds
it . i = (F . i) " (A . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = (F . i) " (A . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (F . i) " (A . i) ) & ( for i being object st i in I holds
b₂ . i = (F . i) " (A . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines "" EQUATION:def 1 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b₄ being ManySortedSet of I holds
( b₄ = F "" A iff for i being object st i in I holds
b₄ . 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th13: :: EQUATION:13

for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f

proof end;

theorem Th14: :: EQUATION:14

for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f

proof end;

theorem :: EQUATION:15

for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A

proof end;

theorem :: EQUATION:16

for I being set
for A being ManySortedSet of I holds (id A) "" A = A

proof end;

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 #) by MSUALG_2:5;

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)

proof end;

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

proof end;

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 object st x in Args (o,B) holds
( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )

proof end;

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 object holds
( x in it iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )

proof end;

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

proof end;

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 b₄ being set holds
( b₄ = SuperAlgebraSet B iff for x being object holds
( x in b₄ 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

proof end;

end;

registration

let S be non empty non void ManySortedSign ;

cluster strict non-empty free for MSAlgebra over S;

existence
ex b₁ being MSAlgebra over S st
( b₁ is strict & b₁ is non-empty & b₁ is free )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let X be V2() V32() MSSubset of A;

cluster GenMSAlg X -> finitely-generated ;

coherence
GenMSAlg X is finitely-generated

proof end;

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 b₁ being MSSubAlgebra of A st
( b₁ is strict & b₁ is non-empty & b₁ is finitely-generated )

proof end;

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 b₁ being MSSubAlgebra of A st b₁ is feasible

proof end;

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) <> {} & x = y holds
h # x = g # y

proof end;

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

proof end;

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 & f is_homomorphism U0,B holds
f is_epimorphism U0,B

proof end;

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 & G = F ** H )

proof end;

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

proof end;

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 & B is MSSubAlgebra of M )

proof end;

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 object 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

proof end;

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 & GenMSAlg Z is feasible holds
GenMSAlg Z is free

proof end;

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 & TermAlg S is non-empty & 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 func x '=' y -> Element of (Equations S) . s;
coherence
'=' is Element of (Equations S) . s

proof end;

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

proof end;

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

proof end;

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;

pred A |= e means :: 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 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;

pred A |= E means :: 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 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

proof end;

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 by Th31;

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 & U0 |= e holds
U1 |= e

proof end;

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 & U0 |= E holds
U1 |= E by Th33;

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

proof end;

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 by Th35;

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

proof end;

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 & A |= e ) ) holds
product F |= e

proof end;

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 & A |= E ) ) holds
product F |= E

proof end;