Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### The Product of the Families of the Groups

by
Artur Kornilowicz

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;
```