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;
theorem Th31:
theorem
theorem
for
G1,
G2,
G3 being non
empty multMagma for
x1,
x2 being
Element of
for
y1,
y2 being
Element of
for
z1,
z2 being
Element of holds
<*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th40:
theorem Th41:
theorem