The abstract of the Mizar article:

The Product of the Families of the Groups

by

Artur Kornilowicz

Received June 10, 1998

MML identifier: GROUP_7

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FUNCT_1, PBOOLE, RELAT_1, VECTSP_1, PRALG_1, RLVECT_2,
      ZF_REFLE, CARD_3, TARSKI, BINOP_1, GROUP_1, REALSET1, BOOLE, SEMI_AF1,
      GROUP_2, FINSET_1, FUNCT_4, GROUP_6, WELLORD1, GROUP_7;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      PARTFUN1, XREAL_0, NAT_1, FINSEQ_1, FUNCT_2, FUNCT_4, FINSET_1, BINOP_1,
      STRUCT_0, VECTSP_1, GROUP_1, GROUP_2, GROUP_6, PBOOLE, CARD_3, PRALG_1,
      PRALG_2;
 constructors BINOP_1, GROUP_6, PRALG_2, ENUMSET1, XCMPLX_0, MEMBERED;
 clusters STRUCT_0, PRALG_2, GROUP_1, FINSET_1, RELAT_1, GROUP_2, FINSEQ_1,
      MOD_2, RELSET_1, ARYTM_3, MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET;


begin  :: Preliminaries

reserve a, b, c, d, e, f for set;

theorem :: GROUP_7:1
 <*a*> = <*b*> implies a = b;

theorem :: GROUP_7:2
   <*a,b*> = <*c,d*> implies a = c & b = d;

theorem :: GROUP_7:3
   <*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f;


begin  :: The product of the families of the groups

reserve i, I for set,
        f, g, h for Function,
        s for ManySortedSet of I;

definition let R be Relation;
 attr R is HGrStr-yielding means
:: GROUP_7:def 1
  for y being set st y in rng R holds y is non empty HGrStr;
end;

definition
 cluster HGrStr-yielding -> 1-sorted-yielding Function;
end;

definition let I be set;
 cluster HGrStr-yielding ManySortedSet of I;
end;

definition
 cluster HGrStr-yielding Function;
end;

definition let I be set;
 mode HGrStr-Family of I is HGrStr-yielding ManySortedSet of I;
end;

definition let I be non empty set,
               F be HGrStr-Family of I,
               i be Element of I;
 redefine func F.i -> non empty HGrStr;
end;

definition let I be set, F be HGrStr-Family of I;
 cluster Carrier F -> non-empty;
end;

definition let I be set,
               F be HGrStr-Family of I;
 func product F -> strict HGrStr means
:: GROUP_7:def 2
  the carrier of it = product Carrier F &
  for f, g being Element of product Carrier F, i being set st i in I
   ex Fi being non empty HGrStr, h being Function st
    Fi = F.i & h = (the mult of it).(f,g) &
   h.i = (the mult of Fi).(f.i,g.i);
end;

definition let I be set, F be HGrStr-Family of I;
 cluster product F -> non empty;
end;

definition let I be set, F be HGrStr-Family of I;
 cluster -> Function-like Relation-like Element of product F;
end;

definition let I be set,
               F be HGrStr-Family of I,
               f, g be Element of product Carrier F;
 cluster (the mult of product F).(f,g) -> Function-like Relation-like;
end;

theorem :: GROUP_7:4
 for F being HGrStr-Family of I, G being non empty HGrStr,
     p, q being Element of product F,
     x, y being Element of G st
   i in I & G = F.i & f = p & g = q & h = p * q & f.i = x & g.i = y holds
  x * y = h.i;

definition let I be set, F be HGrStr-Family of I;
 attr F is Group-like means
:: GROUP_7:def 3
  for i being set st i in I ex Fi being Group-like (non empty HGrStr)
   st Fi = F.i;
 attr F is associative means
:: GROUP_7:def 4
  for i being set st i in I ex Fi being associative (non empty HGrStr)
   st Fi = F.i;
 attr F is commutative means
:: GROUP_7:def 5
  for i being set st i in I ex Fi being commutative (non empty HGrStr)
   st Fi = F.i;
end;

definition let I be non empty set, F be HGrStr-Family of I;
 redefine attr F is Group-like means
:: GROUP_7:def 6
  for i being Element of I holds F.i is Group-like;
 redefine attr F is associative means
:: GROUP_7:def 7
  for i being Element of I holds F.i is associative;
 redefine attr F is commutative means
:: GROUP_7:def 8
    for i being Element of I holds F.i is commutative;
end;

definition let I be set;
 cluster Group-like associative
         commutative HGrStr-Family of I;
end;

definition let I be set, F be Group-like HGrStr-Family of I;
 cluster product F -> Group-like;
end;

definition let I be set, F be associative HGrStr-Family of I;
 cluster product F -> associative;
end;

definition let I be set, F be commutative HGrStr-Family of I;
 cluster product F -> commutative;
end;

theorem :: GROUP_7:5
   for F being HGrStr-Family of I, G being non empty HGrStr st
   i in I & G = F.i & product F is Group-like holds
  G is Group-like;

theorem :: GROUP_7:6
   for F being HGrStr-Family of I, G being non empty HGrStr st
   i in I & G = F.i & product F is associative holds
  G is associative;

theorem :: GROUP_7:7
   for F being HGrStr-Family of I, G being non empty HGrStr st
   i in I & G = F.i & product F is commutative holds
  G is commutative;

theorem :: GROUP_7:8
 for F being Group-like HGrStr-Family of I
  st for i being set st i in I ex G being Group-like (non empty HGrStr)
   st G = F.i & s.i = 1.G
 holds s = 1.product F;

theorem :: GROUP_7:9
 for F being Group-like HGrStr-Family of I,
     G being Group-like (non empty HGrStr) st i in I & G = F.i &
   f = 1.product F
 holds f.i = 1.G;

theorem :: GROUP_7:10
 for F being associative Group-like HGrStr-Family of I,
     x being Element of product F
  st x = g & for i being set st i in I
   ex G being Group, y being Element of G st G = F.i & s.i = y"
    & y = g.i
  holds s = x";

theorem :: GROUP_7:11
 for F being associative Group-like HGrStr-Family of I,
     x being Element of product F,
     G being Group, y being Element of G
   st i in I & G = F.i & f = x & g = x" & f.i = y
  holds g.i = y";

definition let I be set,
      F be associative Group-like HGrStr-Family of I;
 func sum F -> strict Subgroup of product F means
:: GROUP_7:def 9
  for x being set holds x in the carrier of it iff
   ex g being Element of product Carrier F,
      J being finite Subset of I, f being ManySortedSet of J st
     g = 1.product F & x = g +* f &
     for j being set st j in J ex G being Group-like (non empty HGrStr) st
      G = F.j & f.j in the carrier of G & f.j <> 1.G;
end;

definition let I be set,
     F be associative Group-like HGrStr-Family of I,
               f, g be Element of sum F;
 cluster (the mult of sum F).(f,g) -> Function-like Relation-like;
end;

theorem :: GROUP_7:12
   for I being finite set,
     F being associative Group-like HGrStr-Family of I
   holds product F = sum F;


begin  :: The product of one, two and three groups

theorem :: GROUP_7:13
 for G1 being non empty HGrStr holds <*G1*> is HGrStr-Family of {1};

definition let G1 be non empty HGrStr;
 redefine func <*G1*> -> HGrStr-Family of {1};
end;

theorem :: GROUP_7:14
 for G1 being Group-like (non empty HGrStr) holds
  <*G1*> is Group-like HGrStr-Family of {1};

definition let G1 be Group-like (non empty HGrStr);
 redefine func <*G1*> -> Group-like HGrStr-Family of {1};
end;

theorem :: GROUP_7:15
 for G1 being associative (non empty HGrStr) holds
  <*G1*> is associative HGrStr-Family of {1};

definition let G1 be associative (non empty HGrStr);
 redefine func <*G1*> -> associative HGrStr-Family of {1};
end;

theorem :: GROUP_7:16
 for G1 being commutative (non empty HGrStr) holds
  <*G1*> is commutative HGrStr-Family of {1};

definition let G1 be commutative (non empty HGrStr);
 redefine func <*G1*> -> commutative HGrStr-Family of {1};
end;

theorem :: GROUP_7:17
 for G1 being Group holds
  <*G1*> is Group-like associative HGrStr-Family of {1};

definition let G1 be Group;
 redefine func <*G1*> -> Group-like associative HGrStr-Family of {1};
end;

theorem :: GROUP_7:18
 for G1 being commutative Group holds
  <*G1*> is commutative Group-like associative HGrStr-Family of {1};

definition let G1 be commutative Group;
 redefine func <*G1*> ->
                    Group-like associative commutative HGrStr-Family of {1};
end;

definition let G1 be non empty HGrStr;
 cluster -> FinSequence-like Element of product Carrier <*G1*>;
end;

definition let G1 be non empty HGrStr;
 cluster -> FinSequence-like Element of product <*G1*>;
end;

definition let G1 be non empty HGrStr,
               x be Element of G1;
 redefine func <*x*> -> Element of product <*G1*>;
end;

theorem :: GROUP_7:19
 for G1, G2 being non empty HGrStr holds <*G1,G2*> is HGrStr-Family of {1,2};

definition let G1, G2 be non empty HGrStr;
 redefine func <*G1,G2*> -> HGrStr-Family of {1,2};
end;

theorem :: GROUP_7:20
 for G1, G2 being Group-like (non empty HGrStr) holds
  <*G1,G2*> is Group-like HGrStr-Family of {1,2};

definition let G1, G2 be Group-like (non empty HGrStr);
 redefine func <*G1,G2*> -> Group-like HGrStr-Family of {1,2};
end;

theorem :: GROUP_7:21
 for G1, G2 being associative (non empty HGrStr) holds
  <*G1,G2*> is associative HGrStr-Family of {1,2};

definition let G1, G2 be associative (non empty HGrStr);
 redefine func <*G1,G2*> -> associative HGrStr-Family of {1,2};
end;

theorem :: GROUP_7:22
 for G1, G2 being commutative (non empty HGrStr) holds
  <*G1,G2*> is commutative HGrStr-Family of {1,2};

definition let G1, G2 be commutative (non empty HGrStr);
 redefine func <*G1,G2*> -> commutative HGrStr-Family of {1,2};
end;

theorem :: GROUP_7:23
 for G1, G2 being Group holds
  <*G1,G2*> is Group-like associative HGrStr-Family of {1,2};

definition let G1, G2 be Group;
 redefine func <*G1,G2*> -> Group-like associative HGrStr-Family of {1,2};
end;

theorem :: GROUP_7:24
 for G1, G2 being commutative Group holds
  <*G1,G2*> is Group-like associative commutative HGrStr-Family of {1,2};

definition let G1, G2 be commutative Group;
 redefine func <*G1,G2*> ->
                   Group-like associative commutative HGrStr-Family of {1,2};
end;

definition let G1, G2 be non empty HGrStr;
 cluster -> FinSequence-like Element of product Carrier <*G1,G2*>;
end;

definition let G1, G2 be non empty HGrStr;
 cluster -> FinSequence-like Element of product <*G1,G2*>;
end;

definition let G1, G2 be non empty HGrStr,
               x be Element of G1,
               y be Element of G2;
 redefine func <*x,y*> -> Element of product <*G1,G2*>;
end;

theorem :: GROUP_7:25
 for G1, G2, G3 being non empty HGrStr holds
  <*G1,G2,G3*> is HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be non empty HGrStr;
 redefine func <*G1,G2,G3*> -> HGrStr-Family of {1,2,3};
end;

theorem :: GROUP_7:26
 for G1, G2, G3 being Group-like (non empty HGrStr) holds
  <*G1,G2,G3*> is Group-like HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be Group-like (non empty HGrStr);
 redefine func <*G1,G2,G3*> -> Group-like HGrStr-Family of {1,2,3};
end;

theorem :: GROUP_7:27
 for G1, G2, G3 being associative (non empty HGrStr) holds
  <*G1,G2,G3*> is associative HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be associative (non empty HGrStr);
 redefine func <*G1,G2,G3*> -> associative HGrStr-Family of {1,2,3};
end;

theorem :: GROUP_7:28
 for G1, G2, G3 being commutative (non empty HGrStr) holds
  <*G1,G2,G3*> is commutative HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be commutative (non empty HGrStr);
 redefine func <*G1,G2,G3*> -> commutative HGrStr-Family of {1,2,3};
end;

theorem :: GROUP_7:29
 for G1, G2, G3 being Group holds
  <*G1,G2,G3*> is Group-like associative HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be Group;
 redefine func <*G1,G2,G3*> -> Group-like associative HGrStr-Family of {1,2,3};
end;

theorem :: GROUP_7:30
 for G1, G2, G3 being commutative Group holds
  <*G1,G2,G3*> is Group-like associative commutative HGrStr-Family of {1,2,3};

definition let G1, G2, G3 be commutative Group;
 redefine func <*G1,G2,G3*> ->
                 Group-like associative commutative HGrStr-Family of {1,2,3};
end;

definition let G1, G2, G3 be non empty HGrStr;
 cluster -> FinSequence-like Element of product Carrier <*G1,G2,G3*>;
end;

definition let G1, G2, G3 be non empty HGrStr;
 cluster -> FinSequence-like Element of product <*G1,G2,G3*>;
end;

definition let G1, G2, G3 be non empty HGrStr,
               x be Element of G1,
               y be Element of G2,
               z be Element of G3;
 redefine func <*x,y,z*> -> Element of product <*G1,G2,G3*>;
end;

reserve G1, G2, G3 for non empty HGrStr,
        x1, x2 for Element of G1,
        y1, y2 for Element of G2,
        z1, z2 for Element of G3;

theorem :: GROUP_7:31
 <*x1*> * <*x2*> = <*x1*x2*>;

theorem :: GROUP_7:32
   <*x1,y1*> * <*x2,y2*> = <*x1*x2,y1*y2*>;

theorem :: GROUP_7:33
   <*x1,y1,z1*> * <*x2,y2,z2*> = <*x1*x2,y1*y2,z1*z2*>;

reserve G1, G2, G3 for Group-like (non empty HGrStr);

theorem :: GROUP_7:34
   1.product <*G1*> = <*1.G1*>;

theorem :: GROUP_7:35
   1.product <*G1,G2*> = <*1.G1,1.G2*>;

theorem :: GROUP_7:36
   1.product <*G1,G2,G3*> = <*1.G1,1.G2,1.G3*>;

reserve G1, G2, G3 for Group,
        x for Element of G1,
        y for Element of G2,
        z for Element of G3;

theorem :: GROUP_7:37
   (<*x*> qua Element of product <*G1*>)" = <*x"*>;

theorem :: GROUP_7:38
   (<*x,y*> qua Element of product <*G1,G2*>)" = <*x",y"*>;

theorem :: GROUP_7:39
   (<*x,y,z*> qua Element of product <*G1,G2,G3*>)" = <*x",y",z"
*>;

theorem :: GROUP_7:40
 for f being Function of the carrier of G1, the carrier of product <*G1*> st
  for x being Element of G1 holds f.x = <*x*> holds
   f is Homomorphism of G1, product <*G1*>;

theorem :: GROUP_7:41
 for f being Homomorphism of G1, product <*G1*> st
  for x being Element of G1 holds f.x = <*x*> holds
   f is_isomorphism;

theorem :: GROUP_7:42
   G1, product <*G1*> are_isomorphic;