The abstract of the Mizar article:

Products of Many Sorted Algebras

by

Beata Madras

Received April 25, 1994

MML identifier: PRALG_2

[ Mizar article, MML identifier index ]

environ

 vocabulary PBOOLE, MSUALG_1, FUNCT_1, RELAT_1, FRAENKEL, BOOLE, ZF_REFLE,
      CARD_3, PRALG_1, FUNCT_5, FUNCT_2, FUNCT_6, FINSEQ_4, TDGROUP, FUNCT_3,
      MCART_1, COMPLEX1, TARSKI, AMI_1, QC_LANG1, RLVECT_2, CAT_4, CQC_LANG,
      PRALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      MCART_1, STRUCT_0, CQC_LANG, FRAENKEL, FINSEQ_2, FUNCT_5, FUNCT_6,
      CARD_3, DTCONSTR, PBOOLE, PRALG_1, MSUALG_1;
 constructors CQC_LANG, FRAENKEL, PRALG_1, MSUALG_1, XBOOLE_0;
 clusters FUNCT_1, PBOOLE, PRALG_1, MSUALG_1, RELAT_1, RELSET_1, STRUCT_0,
      AMI_1, SUBSET_1, FRAENKEL, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

reserve I,J,i,j,x for set,
        A,B for ManySortedSet of I,
        S for non empty ManySortedSign,
        f for Function;

::
:: Preliminaries
::

definition let IT be set;
  attr IT is with_common_domain means
:: PRALG_2:def 1
   for f,g be Function st f in IT & g in IT holds dom f = dom g;
end;

definition
  cluster with_common_domain functional non empty set;
end;

theorem :: PRALG_2:1
    {{}} is functional with_common_domain set;

definition
 let X be with_common_domain functional set;
func DOM X -> set means
:: PRALG_2:def 2
 (for x be Function st x in X holds it = dom x) if X <> {}
 otherwise it = {};
end;

definition let X be with_common_domain functional non empty set;
  redefine mode Element of X -> ManySortedSet of (DOM X);
end;

theorem :: PRALG_2:2
    for X be with_common_domain functional set st X = {{}} holds DOM X = {};

definition
 let I be set,
     M be non-empty ManySortedSet of I;
 cluster product M -> with_common_domain functional non empty;
end;

begin
::
:: Operations on Functions
::

scheme LambdaDMS {D()->non empty set, F(set)->set}:
ex X be ManySortedSet of D() st for d be Element of D()
holds X.d = F(d);

definition
 let f be Function;
 canceled 2;

func commute f -> Function-yielding Function equals
:: PRALG_2:def 5
 curry' uncurry f;
end;

theorem :: PRALG_2:3
  for f be Function, x be set st x in dom (commute f) holds
(commute f).x is Function;

theorem :: PRALG_2:4
for A,B,C be set, f be Function st A <> {} & B <> {} &
f in Funcs(A,Funcs(B,C)) holds commute f in Funcs(B,Funcs(A,C));

theorem :: PRALG_2:5
for A,B,C be set, f be Function st A <> {} & B <> {} &
f in Funcs(A,Funcs(B,C))
for g,h be Function, x,y be set st x in A & y in B & f.x = g &
(commute f).y = h holds
h.x = g.y & dom h = A & dom g = B & rng h c= C & rng g c= C;

theorem :: PRALG_2:6
for A,B,C be set, f be Function st A <> {} & B <> {} &
f in Funcs(A,Funcs(B,C)) holds commute commute f = f;

theorem :: PRALG_2:7
commute {} = {};

definition
 let F be Function;
func Commute F -> Function means
:: PRALG_2:def 6
 (for x holds x in dom it iff ex f being Function st f in dom F &
   x = commute f) &
 (for f being Function st f in dom it holds it.f = F.commute f);
end;

theorem :: PRALG_2:8
  for F be Function st dom F = {{}} holds Commute F = F;

definition
 let f be Function-yielding Function;
 redefine canceled;

func Frege f -> ManySortedFunction of product doms f means
:: PRALG_2:def 8
 for g be Function st g in product doms f holds it.g = f..g;
end;

definition
 let I, A,B;
func [|A,B|] -> ManySortedSet of I means
:: PRALG_2:def 9
 for i st i in I holds it.i = [:A.i,B.i:];
end;

definition
 let I; let A,B be non-empty ManySortedSet of I;
 cluster [|A,B|] -> non-empty;
end;

theorem :: PRALG_2:9
for I be non empty set, J be set, A,B be ManySortedSet of I,
f be Function of J,I holds [|A,B|]*f = [|A*f,B*f|];

definition
 let I be non empty set,J;
 let A,B be non-empty ManySortedSet of I,
       p be Function of J,I*,
       r be Function of J,I,
       j be set,
       f be Function of (A# * p).j,(A*r).j,
       g be Function of (B# * p).j,(B*r).j;
assume  j in J;
func [[:f,g:]] -> Function of ([|A,B|]# * p).j,([|A,B|]*r).j means
:: PRALG_2:def 10
   for h be Function st h in ([|A,B|]#*p).j
 holds it.h = [f.(pr1 h),g.(pr2 h)];
end;

definition
 let I be non empty set,J;
 let A,B be non-empty ManySortedSet of I,
       p be Function of J,I*,
       r be Function of J,I,
       F be ManySortedFunction of A#*p,A*r,
       G be ManySortedFunction of B#*p,B*r;
func [[:F,G:]] -> ManySortedFunction of [|A,B|]#*p,[|A,B|]*r means
:: PRALG_2:def 11
  for j st j in J
for f be Function of (A#*p).j,(A*r).j,
    g be Function of (B#*p).j,(B*r).j
    st f = F.j & g = G.j holds it.j = [[:f,g:]];
end;

begin

::
:: Family of Many Sorted Universal Algebras
::

definition
let I,S;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means
:: PRALG_2:def 12
for i st i in I holds it.i is non-empty MSAlgebra over S;
end;

definition
 let I be non empty set,
     S;
 let A be MSAlgebra-Family of I,S,
     i be Element of I;
redefine func A.i -> non-empty MSAlgebra over S;
end;

definition
 let S be non empty ManySortedSign,
     U1 be MSAlgebra over S;
func |.U1.| -> set equals
:: PRALG_2:def 13
 union (rng the Sorts of U1);
end;

definition
 let S be non empty ManySortedSign,
     U1 be non-empty MSAlgebra over S;
 cluster |.U1.| -> non empty;
end;

definition
 let I be non empty set,
     S be non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
func |.A.| -> set equals
:: PRALG_2:def 14
 union {|.A.i.| where i is Element of I: not contradiction};
end;

definition
 let I be non empty set,
     S be non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
cluster |.A.| -> non empty;
end;

begin

::
:: Product of Many Sorted Universal Algebras
::

theorem :: PRALG_2:10
for S be non void non empty ManySortedSign, U0 be MSAlgebra over S,
o be OperSymbol of S holds
Args(o,U0) = product ((the Sorts of U0)*(the_arity_of o)) &
dom ((the Sorts of U0)*(the_arity_of o)) = dom (the_arity_of o)
& Result(o,U0) = (the Sorts of U0).(the_result_sort_of o);

theorem :: PRALG_2:11
for S be non void non empty ManySortedSign, U0 be MSAlgebra over S,
o be OperSymbol of S st the_arity_of o = {} holds
Args(o,U0) = {{}};

definition
 let S; let U1,U2 be non-empty MSAlgebra over S;
func [:U1,U2:] -> MSAlgebra over S equals
:: PRALG_2:def 15
 MSAlgebra (# [|the Sorts of U1,the Sorts of U2|],
                 [[:the Charact of U1,the Charact of U2:]] #);
end;

definition
 let S; let U1,U2 be non-empty MSAlgebra over S;
 cluster [:U1,U2:] -> strict;
end;

definition
 let I,S;
 let s be SortSymbol of S,
     A be MSAlgebra-Family of I,S;
func Carrier (A,s) -> ManySortedSet of I means
:: PRALG_2:def 16
  for i be set st i in I
   ex U0 being MSAlgebra over S st U0 = A.i &
      it.i = (the Sorts of U0).s if I <> {}
  otherwise it = {};
end;

definition
 let I,S;
 let s be SortSymbol of S,
     A be MSAlgebra-Family of I,S;
cluster Carrier (A,s) -> non-empty;
end;

definition
 let I,S;
let A be MSAlgebra-Family of I,S;
func SORTS(A) -> ManySortedSet of the carrier of S means
:: PRALG_2:def 17
for s be SortSymbol of S holds it.s = product Carrier(A,s);
end;

definition
 let I, S; let A be MSAlgebra-Family of I,S;
cluster SORTS(A) -> non-empty;
end;

definition
 let I;
 let S be non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
func OPER(A) -> ManySortedFunction of I means
:: PRALG_2:def 18
for i be set st i in I
 ex U0 being MSAlgebra over S st U0 = A.i & it.i = the Charact of U0
                      if I <> {}
  otherwise it = {};
end;

theorem :: PRALG_2:12
for S be non empty ManySortedSign, A be MSAlgebra-Family of I,S holds
dom uncurry (OPER A) = [:I,the OperSymbols of S:];

theorem :: PRALG_2:13
for I be non empty set, S be non void non empty ManySortedSign,
    A be MSAlgebra-Family of I,S, o be OperSymbol of S holds
commute (OPER A) in Funcs(the OperSymbols of S,
Funcs(I,rng uncurry (OPER A)));

definition
 let I be set,
     S be non void non empty ManySortedSign,
     A be MSAlgebra-Family of I,S,
     o be OperSymbol of S;
func A?.o -> ManySortedFunction of I equals
:: PRALG_2:def 19
  (commute (OPER A)).o;
end;

theorem :: PRALG_2:14
for I be non empty set, i be Element of I,
    S be non void non empty ManySortedSign,
    A be MSAlgebra-Family of I,S, o be OperSymbol of S holds
(A?.o).i = Den(o,A.i);

theorem :: PRALG_2:15
  for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S, x be set
 st x in rng (Frege (A?.o)) holds x is Function;

theorem :: PRALG_2:16
for I be non empty set, S be non void non empty ManySortedSign,
    A be MSAlgebra-Family of I,S, o be OperSymbol of S,
    f be Function st f in rng (Frege (A?.o)) holds
dom f = I & for i be Element of I holds f.i in Result(o,A.i);

theorem :: PRALG_2:17
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S,
f be Function st f in dom (Frege (A?.o)) holds
dom f = I & (for i be Element of I holds f.i in Args(o,A.i)) &
rng f c= Funcs(dom(the_arity_of o),|.A.|);

theorem :: PRALG_2:18
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S holds
dom doms (A?.o) = I &
for i be Element of I holds (doms (A?.o)).i = Args(o,A.i);

definition
 let I;
 let S be non void non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
func OPS(A) -> ManySortedFunction of
    (SORTS A)# * the Arity of S, (SORTS A) * the ResultSort of S
means
:: PRALG_2:def 20
  for o be OperSymbol of S holds
 it.o=IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) if I <> {}
  otherwise not contradiction;
end;

definition
 let I be set,
     S be non void non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
func product A -> MSAlgebra over S equals
:: PRALG_2:def 21
    MSAlgebra (# SORTS A, OPS A #);
end;

definition
 let I be set,
     S be non void non empty ManySortedSign,
     A be MSAlgebra-Family of I,S;
cluster product A -> strict;
end;

canceled;

theorem :: PRALG_2:20
  for S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S holds
the Sorts of product A = SORTS A &
the Charact of product A = OPS A;