The abstract of the Mizar article:

More on Products of Many Sorted Algebras

by

Mariusz Giero

Received April 29, 1996

MML identifier: PRALG_3

[ Mizar article, MML identifier index ]

environ

 vocabulary PBOOLE, AMI_1, MSUALG_1, PRALG_2, EQREL_1, FUNCT_1, CARD_3,
      ZF_REFLE, RELAT_1, BOOLE, RLVECT_2, FUNCT_2, PRALG_1, FRAENKEL, TARSKI,
      QC_LANG1, UNIALG_2, FUNCT_5, CQC_LANG, FUNCT_6, TDGROUP, FINSEQ_4,
      FINSEQ_1, BORSUK_1, ALG_1, MSUALG_3, ARYTM_3, WELLORD1, GROUP_6, PRALG_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0,
      FUNCT_2, FRAENKEL, CQC_LANG, EQREL_1, FINSEQ_1, FUNCT_5, FUNCT_6, CARD_3,
      PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, AMI_1, FINSEQ_4, PRALG_1, MSUALG_2;
 constructors EQREL_1, AMI_1, PRALG_2, FINSEQ_4, MSUALG_3, TOLER_1;
 clusters SUBSET_1, STRUCT_0, MSUALG_1, FUNCT_1, PBOOLE, AMI_1, PUA2MSS1,
      RELAT_1, MSUALG_3, PRALG_1, RELSET_1, MSAFREE, PRALG_2, FILTER_1,
      EQREL_1, TOLER_1, PARTFUN1;
 requirements NUMERALS, BOOLE, SUBSET;


begin  ::Preliminaries

::-------------------------------------------------------------------
:: Acknowledgements:
:: ================
::
:: I would like to thank Professor A.Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------

reserve I for non empty set,
        J for ManySortedSet of I,
        S for non void non empty ManySortedSign,
        i for Element of I,
        c for set,
        A for MSAlgebra-Family of I,S,
        EqR for Equivalence_Relation of I,
        U0,U1,U2 for MSAlgebra over S,
        s for SortSymbol of S,
        o for OperSymbol of S,
        f for Function;

definition let I be set, S; let AF be MSAlgebra-Family of I,S;
 cluster product AF -> non-empty;
end;

definition let I be set;
 redefine func id I -> ManySortedSet of I;
end;

definition let I, EqR;
 cluster Class EqR -> with_non-empty_elements;
end;

definition let X be with_non-empty_elements set;
 redefine func id X -> non-empty ManySortedSet of X;
end;

theorem :: PRALG_3:1
 for f,F being Function, A being set st f in product F holds
   f|A in product(F|A);

theorem :: PRALG_3:2
  for A be MSAlgebra-Family of I,S,
      s be SortSymbol of S,
      a be non empty Subset of I,
      Aa be MSAlgebra-Family of a,S st A|a = Aa
      holds Carrier(Aa,s) = (Carrier(A,s))|a;

theorem :: PRALG_3:3
  for i be set,
      I be non empty set,
      EqR be Equivalence_Relation of I,
      c1,c2 be Element of Class EqR st i in c1 & i in c2 holds
      c1 = c2;

theorem :: PRALG_3:4
  for X,Y being set
  for f being Function st f in Funcs(X,Y) holds dom f = X & rng f c= Y;

theorem :: PRALG_3:5
  for D being non empty set
for F being ManySortedFunction of D
for C being with_common_domain functional non empty set st C = rng F
for d being Element of D,e being set st d in dom F & e in DOM C
holds F.d.e = (commute F).e.d;

begin  :: Constants of Many Sorted Algebras

definition let S,U0;
           let o be OperSymbol of S;
func const(o,U0) equals
:: PRALG_3:def 1
 Den(o,U0).{};
end;

theorem :: PRALG_3:6
the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0);

theorem :: PRALG_3:7
  (the Sorts of U0).s <> {} implies
Constants(U0,s) = { const(o,U0) where o is Element of the OperSymbols of S :
                    the_result_sort_of o = s & the_arity_of o = {} };

theorem :: PRALG_3:8
the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs({{}},
     union { Result(o,A.i') where i' is Element of I: not contradiction }));

theorem :: PRALG_3:9
the_arity_of o = {} implies const(o,product A) in Funcs(I,
   union { Result(o,A.i') where i' is Element of I: not contradiction });

definition let S,I,o,A;
 cluster const (o,product A) -> Relation-like Function-like;
end;

theorem :: PRALG_3:10
for o be OperSymbol of S st the_arity_of o = {}
 holds (const (o,product A)).i = const (o,A.i);

theorem :: PRALG_3:11
  the_arity_of o = {} & dom f = I &
(for i be Element of I holds f.i = const(o,A.i)) implies
f = const(o,product A);

theorem :: PRALG_3:12
 for e be Element of Args(o,U1) st
 e = {} & the_arity_of o = {} & Args(o,U1) <> {} & Args(o,U2) <> {}
 for F be ManySortedFunction of U1,U2
 holds F#e = {};

begin :: Properties of Arguments of operations in Many Sorted Algebras

theorem :: PRALG_3:13
  for U1,U2 be non-empty MSAlgebra over S
  for F be ManySortedFunction of U1,U2
  for x be Element of Args(o,U1) holds
  x in product doms (F*the_arity_of o);

theorem :: PRALG_3:14
  for U1,U2 be non-empty MSAlgebra over S
  for F be ManySortedFunction of U1,U2
  for x be Element of Args(o,U1)
  for n be set st n in dom (the_arity_of o) holds
  (F#x).n = F.((the_arity_of o)/.n).(x.n);

theorem :: PRALG_3:15
for x be Element of Args(o,product A) holds
x in Funcs (dom (the_arity_of o),Funcs (I,union { (the Sorts of A.i').s'
     where i' is Element of I,s' is Element of (the carrier of S) :
     not contradiction }));

theorem :: PRALG_3:16
  for x be Element of Args(o,product A)
  for n be set st n in dom (the_arity_of o) holds
   x.n in product Carrier(A,(the_arity_of o)/.n);

theorem :: PRALG_3:17
  for i be Element of I
  for n be set st n in dom(the_arity_of o)
  for s be SortSymbol of S st s = (the_arity_of o).n
  for y be Element of Args(o,product A)
  for g be Function st g = y.n holds
  g.i in (the Sorts of A.i).s;

theorem :: PRALG_3:18
  for y be Element of Args(o,product A) st (the_arity_of o) <> {} holds
  (commute y) in product doms (A?.o);

theorem :: PRALG_3:19
  for y be Element of Args(o,product A) st the_arity_of o <> {} holds
    y in dom (Commute Frege(A?.o));

theorem :: PRALG_3:20
  for I be set, S be non void non empty ManySortedSign,
      A be MSAlgebra-Family of I,S, o be OperSymbol of S
  for x be Element of Args(o,product A) holds
  Den(o,product A).x in product Carrier(A,the_result_sort_of o);

theorem :: PRALG_3:21
  for I,S,A,i
  for o be OperSymbol of S st (the_arity_of o) <> {}
  for U1 be non-empty MSAlgebra over S
  for x be Element of Args(o,product A) holds
  (commute x).i is Element of Args(o,A.i);

theorem :: PRALG_3:22
  for I,S,A,i,o
  for x be Element of Args(o,product A)
  for n be set st n in dom(the_arity_of o)
  for f be Function st f = x.n holds
  ((commute x).i).n = f.i;

theorem :: PRALG_3:23
  for o be OperSymbol of S st (the_arity_of o) <> {}
  for y be Element of Args(o,product A),
      i' be Element of I
  for g be Function st g = Den(o,product A).y
  holds g.i' = Den(o,A.i').((commute y).i');

begin :: The Projection of Family of Many Sorted Algebras

definition let f be Function, x be set;
 func proj(f,x) -> Function means
:: PRALG_3:def 2
  dom it = product f &
  for y being Function st y in dom it holds it.y = y.x;
end;

definition let I,S;
           let A be MSAlgebra-Family of I,S,
               i be Element of I;
func proj(A,i) -> ManySortedFunction of product A,A.i means
:: PRALG_3:def 3
    for s be Element of S holds
     it.s = proj (Carrier(A,s), i);
end;

theorem :: PRALG_3:24
for x be Element of Args(o,product A) st Args(o,product A) <> {} &
the_arity_of o <> {}
for i be Element of I holds
proj(A,i)#x = (commute x).i;

theorem :: PRALG_3:25
    for i be Element of I
  for A be MSAlgebra-Family of I,S
  holds proj(A,i) is_homomorphism product A,A.i;

theorem :: PRALG_3:26
  for U1 be non-empty MSAlgebra over S
  for F being ManySortedFunction of I st
  (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
      F1 = F.i & F1 is_homomorphism U1,A.i) holds
      F in Funcs(I,Funcs(the carrier of S,
{F.i'.s1 where s1 is SortSymbol of S,i' is Element of I :not contradiction}))
      & (commute F).s.i = F.i.s;

theorem :: PRALG_3:27
  for U1 be non-empty MSAlgebra over S
  for F being ManySortedFunction of I st
  (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
      F1 = F.i & F1 is_homomorphism U1,A.i) holds
  (commute F).s in Funcs(I,Funcs((the Sorts of U1).s,
union {(the Sorts of A.i').s1 where
         i' is Element of I,s1 is SortSymbol of S : not contradiction}));

theorem :: PRALG_3:28
  for U1 be non-empty MSAlgebra over S
  for F being ManySortedFunction of I st
  (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
      F1 = F.i & F1 is_homomorphism U1,A.i)
  for F' be ManySortedFunction of U1,A.i st F' = F.i
  for x be set st x in (the Sorts of U1).s
  for f be Function st f = (commute((commute F).s)).x holds
  f.i = F'.s.x;

theorem :: PRALG_3:29
  for U1 be non-empty MSAlgebra over S
  for F being ManySortedFunction of I st
  (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
      F1 = F.i & F1 is_homomorphism U1,A.i)
   for x be set st x in (the Sorts of U1).s holds
   (commute ((commute F).s)).x in product (Carrier(A,s));

theorem :: PRALG_3:30
    for U1 be non-empty MSAlgebra over S
  for F being ManySortedFunction of I st
  (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
      F1 = F.i & F1 is_homomorphism U1,A.i) holds
  ex H being ManySortedFunction of U1,(product A) st
  H is_homomorphism U1,(product A) &
  (for i be Element of I holds proj(A,i) ** H = F.i);

begin :: The Class of Family of Many Sorted Algebras

definition let I,J,S;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means
:: PRALG_3:def 4
for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S;
end;

definition
  let I,S,A,EqR;
func A / EqR -> MSAlgebra-Class of S,id (Class EqR) means
:: PRALG_3:def 5
  for c st c in Class EqR holds it.c = A|c;
end;

definition let I,S;
           let J be non-empty ManySortedSet of I;
           let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means
:: PRALG_3:def 6
   for i st i in I ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S
   st Ji = J.i & Cs = C.i & it.i = product Cs;
end;

theorem :: PRALG_3:31
    for A be MSAlgebra-Family of I,S,
      EqR be Equivalence_Relation of I holds
  product A, product (product (A/EqR)) are_isomorphic;