:: The Product of the Families of the Groups
:: by Artur Korni{\l}owicz
::
:: Received June 10, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: GROUP_7:1
theorem :: GROUP_7:2
theorem :: GROUP_7:3
:: deftheorem Def1 defines HGrStr-yielding GROUP_7:def 1 :
definition
let I be
set ;
let F be
HGrStr-Family of
I;
func product F -> strict multMagma means :
Def2:
:: GROUP_7:def 2
( the
carrier of
it = product (Carrier F) & ( for
f,
g being
Element of
product (Carrier F) for
i being
set st
i in I holds
ex
Fi being non
empty multMagma ex
h being
Function st
(
Fi = F . i &
h = the
multF of
it . f,
g &
h . i = the
multF of
Fi . (f . i),
(g . i) ) ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . f,g & h . i = the multF of Fi . (f . i),(g . i) ) ) )
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . f,g & h . i = the multF of Fi . (f . i),(g . i) ) ) & the carrier of b2 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b2 . f,g & h . i = the multF of Fi . (f . i),(g . i) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines product GROUP_7:def 2 :
theorem Th4: :: GROUP_7:4
:: deftheorem Def3 defines Group-like GROUP_7:def 3 :
:: deftheorem Def4 defines associative GROUP_7:def 4 :
:: deftheorem Def5 defines commutative GROUP_7:def 5 :
:: deftheorem Def6 defines Group-like GROUP_7:def 6 :
:: deftheorem Def7 defines associative GROUP_7:def 7 :
:: deftheorem defines commutative GROUP_7:def 8 :
theorem :: GROUP_7:5
theorem :: GROUP_7:6
theorem :: GROUP_7:7
theorem Th8: :: GROUP_7:8
theorem Th9: :: GROUP_7:9
theorem Th10: :: GROUP_7:10
theorem Th11: :: GROUP_7:11
:: deftheorem Def9 defines sum GROUP_7:def 9 :
theorem :: GROUP_7:12
theorem Th13: :: GROUP_7:13
theorem Th14: :: GROUP_7:14
theorem Th15: :: GROUP_7:15
theorem Th16: :: GROUP_7:16
theorem Th17: :: GROUP_7:17
theorem Th18: :: GROUP_7:18
theorem Th19: :: GROUP_7:19
theorem Th20: :: GROUP_7:20
theorem Th21: :: GROUP_7:21
theorem Th22: :: GROUP_7:22
theorem Th23: :: GROUP_7:23
theorem Th24: :: GROUP_7:24
theorem Th25: :: GROUP_7:25
definition
let G1,
G2,
G3 be non
empty multMagma ;
:: original: <*redefine func <*G1,G2,G3*> -> HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is HGrStr-Family of {1,2,3}
by Th25;
end;
theorem Th26: :: GROUP_7:26
definition
let G1,
G2,
G3 be non
empty Group-like multMagma ;
:: original: <*redefine func <*G1,G2,G3*> -> Group-like HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like HGrStr-Family of {1,2,3}
by Th26;
end;
theorem Th27: :: GROUP_7:27
definition
let G1,
G2,
G3 be non
empty associative multMagma ;
:: original: <*redefine func <*G1,G2,G3*> -> associative HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is associative HGrStr-Family of {1,2,3}
by Th27;
end;
theorem Th28: :: GROUP_7:28
definition
let G1,
G2,
G3 be non
empty commutative multMagma ;
:: original: <*redefine func <*G1,G2,G3*> -> commutative HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is commutative HGrStr-Family of {1,2,3}
by Th28;
end;
theorem Th29: :: GROUP_7:29
definition
let G1,
G2,
G3 be
Group;
:: original: <*redefine func <*G1,G2,G3*> -> Group-like associative HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like associative HGrStr-Family of {1,2,3}
by Th29;
end;
theorem Th30: :: GROUP_7:30
definition
let G1,
G2,
G3 be
commutative Group;
:: original: <*redefine func <*G1,G2,G3*> -> Group-like associative commutative HGrStr-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like associative commutative HGrStr-Family of {1,2,3}
by Th30;
end;
definition
let G1,
G2,
G3 be non
empty multMagma ;
let x be
Element of
G1;
let y be
Element of
G2;
let z be
Element of
G3;
:: original: <*redefine func <*x,y,z*> -> Element of
(product <*G1,G2,G3*>);
coherence
<*x,y,z*> is Element of (product <*G1,G2,G3*>)
end;
theorem Th31: :: GROUP_7:31
theorem :: GROUP_7:32
theorem :: GROUP_7:33
for
G1,
G2,
G3 being non
empty multMagma for
x1,
x2 being
Element of
G1 for
y1,
y2 being
Element of
G2 for
z1,
z2 being
Element of
G3 holds
<*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
theorem :: GROUP_7:34
theorem :: GROUP_7:35
theorem :: GROUP_7:36
theorem :: GROUP_7:37
theorem :: GROUP_7:38
theorem :: GROUP_7:39
theorem Th40: :: GROUP_7:40
theorem Th41: :: GROUP_7:41
theorem :: GROUP_7:42