begin
:: deftheorem Def1 defines multMagma-yielding GROUP_7:def 1 :
definition
let I be
set ;
let F be
multMagma-Family of
I;
func product F -> strict multMagma means :
Def2:
( 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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
:: 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
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
:: deftheorem Def9 defines sum GROUP_7:def 9 :
theorem
begin
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
definition
let G1,
G2,
G3 be non
empty multMagma ;
<*redefine func <*G1,G2,G3*> -> multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is multMagma-Family of {1,2,3}
by Th25;
end;
theorem Th26:
definition
let G1,
G2,
G3 be non
empty Group-like multMagma ;
<*redefine func <*G1,G2,G3*> -> Group-like multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}
by Th26;
end;
theorem Th27:
definition
let G1,
G2,
G3 be non
empty associative multMagma ;
<*redefine func <*G1,G2,G3*> -> associative multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is associative multMagma-Family of {1,2,3}
by Th27;
end;
theorem Th28:
definition
let G1,
G2,
G3 be non
empty commutative multMagma ;
<*redefine func <*G1,G2,G3*> -> commutative multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
by Th28;
end;
theorem Th29:
definition
let G1,
G2,
G3 be
Group;
<*redefine func <*G1,G2,G3*> -> Group-like associative multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3}
by Th29;
end;
theorem Th30:
definition
let G1,
G2,
G3 be
commutative Group;
<*redefine func <*G1,G2,G3*> -> Group-like associative commutative multMagma-Family of
{1,2,3};
coherence
<*G1,G2,G3*> is Group-like associative commutative multMagma-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;
<*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:
theorem
theorem
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
theorem
theorem
theorem
theorem
theorem
theorem Th40:
theorem Th41:
theorem