The abstract of the Mizar article:

Equations in Many Sorted Algebras

by

Artur Kornilowicz

Received May 30, 1997

MML identifier: EQUATION

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, PRALG_1, MSUALG_3, FUNCT_2,
      PRALG_2, BOOLE, NATTRA_1, FUNCT_6, MSUALG_2, REALSET1, AMI_1, MSUALG_1,
      UNIALG_2, TDGROUP, FINSEQ_4, CARD_3, RLVECT_2, PRELAMB, MSAFREE,
      PRE_CIRC, MSAFREE2, FREEALG, MSUALG_6, QC_LANG1, ALG_1, GROUP_6,
      FINSET_1, CLOSURE2, TARSKI, FINSEQ_1, PRALG_3, FUNCT_4, FUNCOP_1,
      ZF_LANG, MCART_1, ZF_MODEL, WELLORD1, MSUALG_4, BORSUK_1, EQUATION;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      PARTFUN1, STRUCT_0, FUNCT_2, MCART_1, FINSET_1, FINSEQ_1, FUNCT_4,
      CARD_3, PBOOLE, MSUALG_1, PRALG_1, PRALG_2, FINSEQ_4, PRE_CIRC, MSUALG_2,
      PRALG_3, MSUALG_3, MSUALG_4, EXTENS_1, MSAFREE, MSAFREE2, AUTALG_1,
      CLOSURE2, MSUALG_6;
 constructors AUTALG_1, PRALG_3, MSAFREE2, PRE_CIRC, CLOSURE2, FINSEQ_4,
      MSUALG_6, EXTENS_1;
 clusters MSUALG_6, FINSET_1, EXTENS_1, CANTOR_1, FUNCT_1, MSAFREE, MSUALG_1,
      MSUALG_2, MSUALG_9, PBOOLE, PRALG_1, PRALG_2, PRALG_3, STRUCT_0,
      CLOSURE2, PRELAMB, MSUALG_4, FINSEQ_1, RELSET_1, SUBSET_1, MEMBERED,
      ORDINAL2;
 requirements SUBSET, BOOLE;


begin  :: On the Functions and Many Sorted Functions

reserve I for set;

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

theorem :: EQUATION:2
  for A being ManySortedSet of I, B, C being non-empty ManySortedSet of I
 for f being ManySortedFunction of A, B, g being ManySortedFunction of B, C
  st g ** f is "onto" holds g is "onto";

theorem :: EQUATION:3    :: see PRALG_2:5
for A, B being non empty set, 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;

canceled;

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

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

theorem :: EQUATION:7
for B being non-empty ManySortedSet of I, C being ManySortedSet of I
 for A being ManySortedSubset of C, F being ManySortedFunction of A, B
  ex G being ManySortedFunction of C, B st G || A = F;

definition let I be set,
               A be ManySortedSet of I,
               F be ManySortedFunction of I;
 func F""A -> ManySortedSet of I means
:: EQUATION:def 1
  for i being set st i in I holds it.i = (F.i)"(A.i);
end;

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

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

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

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

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

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

theorem :: EQUATION:14
for f being ManySortedFunction of I holds f.:.:(doms f) = rngs f;

theorem :: EQUATION:15
for f being ManySortedFunction of I holds f""(rngs f) = doms f;

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

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


begin  :: On the Many Sorted Algebras

reserve S for non empty non void ManySortedSign,
        U0, U1 for non-empty MSAlgebra over S;

canceled;

theorem :: EQUATION:19
for A being MSAlgebra over S holds A is MSSubAlgebra of the MSAlgebra of A;

theorem :: EQUATION:20
for U0 being MSAlgebra over S, A being MSSubAlgebra of U0
 for o being OperSymbol of S, x being set st x in Args(o,A)
  holds x in Args(o,U0);

theorem :: EQUATION:21
for U0 being MSAlgebra over S, A being MSSubAlgebra of U0
 for o being OperSymbol of S, x being set st x in Args(o,A)
  holds Den(o,A).x = Den(o,U0).x;

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

definition let S be non void non empty ManySortedSign,
               A be MSAlgebra over S,
               B be MSSubAlgebra of A;
 func SuperAlgebraSet B means
:: 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;
end;

definition let S be non void non empty ManySortedSign,
               A be MSAlgebra over S,
               B be MSSubAlgebra of A;
 cluster SuperAlgebraSet B -> non empty;
end;

definition let S be non empty non void ManySortedSign;
 cluster strict non-empty free MSAlgebra over S;
end;

definition let S be non empty non void ManySortedSign,
               A be non-empty MSAlgebra over S,
               X be non-empty locally-finite MSSubset of A;
 cluster GenMSAlg X -> finitely-generated;
end;

definition let S be non empty non void ManySortedSign,
               A be non-empty MSAlgebra over S;
 cluster strict non-empty finitely-generated MSSubAlgebra of A;
end;

definition let S be non empty non void ManySortedSign,
               A be feasible MSAlgebra over S;
 cluster feasible MSSubAlgebra of A;
end;

theorem :: EQUATION:23
for A being MSAlgebra over S, C being MSSubAlgebra of A
 for D being ManySortedSubset of the Sorts of A st D = the Sorts of C
  for h being ManySortedFunction of A, U0
   for g being ManySortedFunction of C, U0 st g = h || D
    for o being OperSymbol of S, 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;

theorem :: EQUATION:24
for A being feasible MSAlgebra over S, C being feasible MSSubAlgebra of A
 for D being ManySortedSubset of the Sorts of A st D = the Sorts of C
  for h being ManySortedFunction of A, U0 st h is_homomorphism A, U0
   for g being ManySortedFunction of C, U0 st g = h || D
 holds g is_homomorphism C, U0;

theorem :: EQUATION:25
  for B being strict non-empty MSAlgebra over S
 for G being GeneratorSet of U0, H being non-empty 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;

theorem :: EQUATION:26
for W being strict free non-empty MSAlgebra over S
 for F being ManySortedFunction of U0, U1 st F is_epimorphism U0, U1
  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;

theorem :: EQUATION:27
for I being non empty finite set, 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
 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;

theorem :: EQUATION:28
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;

theorem :: EQUATION:29
  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 }
 for F being MSAlgebra-Family of C, SG st
  for c being set st c in C holds c = F.c
 ex PS being strict non-empty MSSubAlgebra of product F,
    BA being ManySortedFunction of PS, AG st
  BA is_epimorphism PS, AG;

theorem :: EQUATION:30
  for U0 being feasible free MSAlgebra over S, 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;

begin  :: Equations in Many Sorted Algebras

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);
end;

definition let S be non empty non void ManySortedSign;
 cluster TermAlg S -> strict non-empty 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|];
end;

definition let S be non empty non void ManySortedSign;
 cluster Equations S -> non-empty;
end;

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

reserve s for SortSymbol of S;
reserve e for Element of (Equations S).s;
reserve E for EqualSet of S;

definition let S be non empty non void ManySortedSign,
               s be SortSymbol of S,
               x, y be Element of (the Sorts of TermAlg S).s;
 redefine func [x,y] -> Element of (Equations S).s;
 synonym x '=' y;
end;

theorem :: EQUATION:31
e`1 in (the Sorts of TermAlg S).s;

theorem :: EQUATION:32
e`2 in (the Sorts of TermAlg S).s;

definition let S be non empty non void ManySortedSign,
               A be MSAlgebra over S,
               s be SortSymbol of S,
               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;

definition let S be non empty non void ManySortedSign,
               A be MSAlgebra over S,
               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;

theorem :: EQUATION:33
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e;

theorem :: EQUATION:34
  for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E;

theorem :: EQUATION:35
U0, U1 are_isomorphic & U0 |= e implies U1 |= e;

theorem :: EQUATION:36
  U0, U1 are_isomorphic & U0 |= E implies U1 |= E;

theorem :: EQUATION:37
for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e;

theorem :: EQUATION:38
  for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E;

theorem :: EQUATION:39
for F being MSAlgebra-Family of I, S st
 (for i being set st i in I ex A being MSAlgebra over S st A = F.i & A |= e)
  holds product F |= e;

theorem :: EQUATION:40
  for F being MSAlgebra-Family of I, S st
 (for i being set st i in I ex A being MSAlgebra over S st A = F.i & A |= E)
  holds product F |= E;