:: Commutator and Center of a Group
:: by Wojciech A. Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, TARSKI, NUMBERS, INT_1, GROUP_1, GROUP_2,
PRE_TOPC, FINSEQ_1, STRUCT_0, NEWTON, RELAT_1, EQREL_1, BINOP_1, NAT_1,
FUNCT_1, PARTFUN1, ORDINAL4, ARYTM_3, CARD_1, CARD_3, QC_LANG1, XXREAL_1,
ARYTM_1, GROUP_4, RLSUB_1, FINSET_1, CQC_SIM1, GROUP_3, GROUP_5;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
FUNCT_1, PARTFUN1, CARD_1, FINSEQ_1, FINSET_1, FINSEQ_4, INT_1, DOMAIN_1,
STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4;
constructors PARTFUN1, SETFAM_1, NAT_1, FINSEQ_4, FINSOP_1, REALSET1, GROUP_4,
RELSET_1, BINOP_2;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, INT_1, STRUCT_0, GROUP_1,
GROUP_2, GROUP_3, ORDINAL1, FINSEQ_1, CARD_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, GROUP_1, XBOOLE_0;
equalities XBOOLE_0, GROUP_2, GROUP_3, GROUP_4;
expansions TARSKI, GROUP_1, GROUP_3;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, GROUP_1, GROUP_2,
GROUP_3, GROUP_4, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, CARD_2, FINSOP_1,
STRUCT_0, PARTFUN1;
schemes FINSEQ_2, DOMAIN_1;
begin :: Preliminaries.
reserve x,y for set,
k,n for Nat,
i for Integer,
G for Group,
a,b,c ,d,e for Element of G,
A,B,C,D for Subset of G,
H,H1,H2,H3,H4 for Subgroup of G ,
N1,N2 for normal Subgroup of G,
F,F1,F2 for FinSequence of the carrier of G,
I,I1,I2 for FinSequence of INT;
theorem Th1:
x in (1).G iff x = 1_G
proof
thus x in (1).G implies x = 1_G
proof
assume x in (1).G;
then x in the carrier of (1).G by STRUCT_0:def 5;
then x in {1_G} by GROUP_2:def 7;
hence thesis by TARSKI:def 1;
end;
thus thesis by GROUP_2:46;
end;
theorem
a in H & b in H implies a |^ b in H
proof
assume a in H & b in H;
then b" in H & a * b in H by GROUP_2:50,51;
then b " * (a * b) in H by GROUP_2:50;
hence thesis by GROUP_1:def 3;
end;
theorem Th3:
for N being strict normal Subgroup of G holds a in N implies a |^ b in N
proof
let N be strict normal Subgroup of G;
assume a in N;
then a |^ b in N |^ b by GROUP_3:58;
hence thesis by GROUP_3:def 13;
end;
theorem Th4:
x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2
proof
thus x in H1 * H2 implies ex a,b st x = a * b & a in H1 & b in H2
proof
assume x in H1 * H2;
then x in carr H1 * H2;
then consider a,b such that
A1: x = a * b and
A2: a in carr H1 and
A3: b in H2 by GROUP_2:94;
a in H1 by A2,STRUCT_0:def 5;
hence thesis by A1,A3;
end;
given a,b such that
A4: x = a * b & a in H1 and
A5: b in H2;
b in carr H2 by A5,STRUCT_0:def 5;
then x in H1 * carr H2 by A4,GROUP_2:95;
hence thesis;
end;
theorem Th5:
H1 * H2 = H2 * H1 implies (x in H1 "\/" H2 iff ex a,b st x = a *
b & a in H1 & b in H2)
proof
assume
A1: H1 * H2 = H2 * H1;
thus x in H1 "\/" H2 implies ex a,b st x = a * b & a in H1 & b in H2
proof
assume x in H1 "\/" H2;
then x in the carrier of H1 "\/" H2 by STRUCT_0:def 5;
then x in H1 * H2 by A1,GROUP_4:51;
hence thesis by Th4;
end;
given a,b such that
A2: x = a * b & a in H1 & b in H2;
x in H1 * H2 by A2,Th4;
then x in the carrier of H1 "\/" H2 by A1,GROUP_4:51;
hence thesis by STRUCT_0:def 5;
end;
theorem
G is commutative Group implies (x in H1 "\/" H2 iff ex a,b st x = a *
b & a in H1 & b in H2)
proof
assume G is commutative Group;
then H1 * H2 = H2 * H1 by GROUP_2:25;
hence thesis by Th5;
end;
theorem Th7:
for N1,N2 being strict normal Subgroup of G holds x in N1 "\/" N2
iff ex a,b st x = a * b & a in N1 & b in N2
proof
let N1,N2 be strict normal Subgroup of G;
N1 * N2 = N2 * N1 by GROUP_3:125;
hence thesis by Th5;
end;
theorem
for N being normal Subgroup of G holds H * N = N * H
proof
let N be normal Subgroup of G;
thus H * N = carr H * N .= N * carr H by GROUP_3:120
.= N * H;
end;
definition
let G,F,a;
func F |^ a -> FinSequence of the carrier of G means
:Def1:
len it = len F & for k be Nat st k in dom F holds it.k = (F/.k) |^ a;
existence
proof
deffunc F(Nat) = (F/.$1) |^ a;
consider F1 such that
A1: len F1 = len F & for k be Nat st k in dom F1 holds F1.k = F(k)
from FINSEQ_2:sch 1;
dom F1 = dom F by A1,FINSEQ_3:29;
hence thesis by A1;
end;
correctness
proof
let F1,F2;
assume that
A2: len F1 = len F and
A3: for k be Nat st k in dom F holds F1.k = (F/.k) |^ a and
A4: len F2 = len F and
A5: for k be Nat st k in dom F holds F2.k = (F/.k) |^ a;
A6: dom F1 = Seg len F by A2,FINSEQ_1:def 3;
now
let k be Nat;
assume k in dom F1;
then
A7: k in dom F by A6,FINSEQ_1:def 3;
hence F1.k = (F/.k) |^ a by A3
.= F2.k by A5,A7;
end;
hence thesis by A2,A4,FINSEQ_2:9;
end;
end;
theorem Th9:
(F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
proof
A1: now
let k;
assume k in dom(F1 |^ a);
then k in Seg len(F1 |^ a) by FINSEQ_1:def 3;
then k in Seg len F1 by Def1;
then
A2: k in dom F1 by FINSEQ_1:def 3;
then
A3: F1/.k = (F1 ^ F2)/.k & k in dom(F1 ^ F2) by FINSEQ_3:22,FINSEQ_4:68;
thus (F1 |^ a).k = (F1/.k) |^ a by A2,Def1
.= ((F1 ^ F2) |^ a).k by A3,Def1;
end;
A4: now
let k;
assume
A5: k in dom(F2 |^ a);
len F2 = len(F2 |^ a) by Def1;
then
A6: k in dom F2 by A5,FINSEQ_3:29;
then len F1 + k in dom(F1 ^ F2) by FINSEQ_1:28;
then len(F1 |^ a) + k in dom(F1 ^ F2) by Def1;
hence
((F1 ^ F2) |^ a).(len(F1 |^ a) + k) = ((F1 ^ F2)/.(len(F1 |^ a) + k))
|^ a by Def1
.= ((F1 ^ F2)/.(len F1 + k)) |^ a by Def1
.= (F2/.k) |^ a by A6,FINSEQ_4:69
.= (F2 |^ a).k by A6,Def1;
end;
len(F1 |^ a) + len(F2 |^ a) = len F1 + len(F2 |^ a) by Def1
.= len F1 + len F2 by Def1
.= len(F1 ^ F2) by FINSEQ_1:22
.= len((F1 ^ F2) |^ a) by Def1;
hence thesis by A1,A4,FINSEQ_3:38;
end;
theorem Th10:
(<*> the carrier of G) |^ a = {}
proof
len((<*> the carrier of G) |^ a) = len <*> the carrier of G by Def1
.= 0;
hence thesis;
end;
theorem Th11:
<* a *> |^ b = <* a |^ b *>
proof
A1: now
let k be Nat;
assume k in dom<* a *>;
then k in {1} by FINSEQ_1:2,38;
then
A2: k = 1 by TARSKI:def 1;
hence <* a |^ b *>.k = a |^ b
.= (<* a *>/.k) |^ b by A2,FINSEQ_4:16;
end;
len<* a |^ b *> = 1 by FINSEQ_1:40
.= len<* a *> by FINSEQ_1:39;
hence thesis by A1,Def1;
end;
theorem Th12:
<* a,b *> |^ c = <* a |^ c,b |^ c *>
proof
thus <* a,b *> |^ c = (<* a *> ^ <* b *>) |^ c by FINSEQ_1:def 9
.= (<* a *> |^ c) ^ (<* b *> |^ c) by Th9
.= <* a |^ c *> ^ (<* b *> |^ c) by Th11
.= <* a |^ c *> ^ <* b |^ c *> by Th11
.= <* a |^ c, b |^ c *> by FINSEQ_1:def 9;
end;
theorem
<* a,b,c *> |^ d = <* a |^ d,b |^ d,c |^ d *>
proof
thus <* a,b,c *> |^ d = (<* a *> ^ <* b,c *>) |^ d by FINSEQ_1:43
.= (<* a *> |^ d) ^ (<* b,c *> |^ d) by Th9
.= <* a *> |^ d ^ <* b |^ d,c |^ d *> by Th12
.= <* a |^ d *> ^ <* b |^ d,c |^ d *> by Th11
.= <* a |^ d,b |^ d,c |^ d *> by FINSEQ_1:43;
end;
theorem Th14:
Product(F |^ a) = Product(F) |^ a
proof
defpred P[FinSequence of the carrier of G] means Product($1 |^ a) = Product(
$1) |^ a;
A1: now
let F,b;
assume
A2: P[F];
Product((F ^ <* b *>) |^ a) = Product((F |^ a) ^ (<* b *> |^ a)) by Th9
.= Product(F) |^ a * Product(<* b *> |^ a) by A2,GROUP_4:5
.= Product(F) |^ a * Product<* b |^ a *> by Th11
.= Product(F) |^ a * (b |^ a) by FINSOP_1:11
.= (Product(F) * b) |^ a by GROUP_3:23
.= Product(F ^ <* b *>) |^ a by GROUP_4:6;
hence P[F^<*b*>];
end;
A3: P[<*> the carrier of G]
proof
set p = <*> the carrier of G;
thus Product(p |^ a) = Product p by Th10
.= 1_G by GROUP_4:8
.= (1_G) |^ a by GROUP_3:17
.= Product p |^ a by GROUP_4:8;
end;
for F holds P[F] from FINSEQ_2:sch 2(A3,A1);
hence thesis;
end;
theorem Th15:
(F |^ a) |^ I = (F |^ I) |^ a
proof
len(F |^ I) = len F by GROUP_4:def 3;
then
A1: dom(F |^ I) = dom F by FINSEQ_3:29;
A2: len(F |^ a) = len F by Def1;
then
A3: dom(F |^ a) = dom F by FINSEQ_3:29;
A4: len((F |^ a) |^ I) = len(F |^ a) by GROUP_4:def 3;
then
A5: dom ((F |^ a) |^ I) = Seg len F by A2,FINSEQ_1:def 3;
A6: now
let k be Nat;
assume k in dom ((F |^ a) |^ I);
then
A7: k in dom F by A5,FINSEQ_1:def 3;
then
A8: (F |^ a)/.k = (F |^ a).k by A3,PARTFUN1:def 6;
A9: (F |^ I)/.k = (F |^ I).k by A1,A7,PARTFUN1:def 6;
thus ((F |^ a) |^ I).k = ((F |^ a)/.k) |^ @(I/.k) by A3,A7,GROUP_4:def 3
.= ((F/.k) |^ a) |^ @(I/.k) by A7,A8,Def1
.= ((F/.k) |^ @(I/.k)) |^ a by GROUP_3:28
.= ((F |^ I)/.k) |^ a by A7,A9,GROUP_4:def 3
.= ((F |^ I) |^ a).k by A1,A7,Def1;
end;
len(F |^ I |^ a) = len(F |^ I) by Def1
.= len F by GROUP_4:def 3;
hence thesis by A2,A4,A6,FINSEQ_2:9;
end;
begin :: Commutators.
definition
let G,a,b;
func [.a,b.] -> Element of G equals
a" * b" * a * b;
correctness;
end;
theorem Th16:
[.a,b.] = a" * b" * a * b & [.a,b.] = a" * (b" * a) * b & [.a,b
.] = a" * (b" * a * b) & [.a,b.] = a" * (b" * (a * b)) & [.a,b.] = (a" * b") *
(a * b)
proof
thus [.a,b.] = a" * b" * a * b;
thus [.a,b.] = a" * (b" * a) * b by GROUP_1:def 3;
hence [.a,b.] = a" * (b" * a * b) by GROUP_1:def 3;
hence [.a,b.] = a" * (b" * (a * b)) by GROUP_1:def 3;
thus thesis by GROUP_1:def 3;
end;
theorem Th17:
[.a,b.] = (b * a)" * (a * b)
proof
thus [.a,b.] = (a" * b") * (a * b) by Th16
.= (b * a)" * (a * b) by GROUP_1:17;
end;
theorem
[.a,b.] = (b" |^ a) * b & [.a,b.] = a" * (a |^ b) by Th16;
theorem Th19:
[.1_G,a.] = 1_G & [.a,1_G.] = 1_G
proof
thus [.1_G,a.] = ((1_G)" * a") * a by GROUP_1:def 4
.= (1_G * a") * a by GROUP_1:8
.= a" * a by GROUP_1:def 4
.= 1_G by GROUP_1:def 5;
thus [.a,1_G.] = (a" * (1_G)") * a by GROUP_1:def 4
.= (a" * 1_G) * a by GROUP_1:8
.= a" * a by GROUP_1:def 4
.= 1_G by GROUP_1:def 5;
end;
theorem Th20:
[.a,a.] = 1_G
proof
thus [.a,a.] = (a * a)" * (a * a) by Th17
.= 1_G by GROUP_1:def 5;
end;
theorem
[.a,a".] = 1_G & [.a",a.] = 1_G
proof
thus [.a,a".] = (a" * a"") * (a * a") by Th16
.= 1_G * (a * a") by GROUP_1:def 5
.= a * a" by GROUP_1:def 4
.= 1_G by GROUP_1:def 5;
thus [.a",a.] = (a"" * a") * (a" * a) by Th16
.= (a"" * a") * 1_G by GROUP_1:def 5
.= a"" * a" by GROUP_1:def 4
.= 1_G by GROUP_1:def 5;
end;
theorem Th22:
[.a,b.]" = [.b,a.]
proof
thus [.a,b.]" = ((a" * b") * (a * b))" by Th16
.= (a * b)" * (a" * b")" by GROUP_1:17
.= (b" * a") * (a" * b")" by GROUP_1:17
.= (b" * a") * (b"" * a"") by GROUP_1:17
.= (b" * a") * (b"" * a)
.= (b" * a") * (b * a)
.= [.b,a.] by Th16;
end;
theorem Th23:
[.a,b.] |^ c = [.a |^ c,b |^ c.]
proof
thus [.a,b.] |^ c = c" * (a" * 1_G * b" * a * b) * c by GROUP_1:def 4
.= c" * (a" * (c * c") * b" * a * b) * c by GROUP_1:def 5
.= c" * (a" * (c * c") * b" * (a * b)) * c by GROUP_1:def 3
.= c" * (a" * (c * c") * (b" * (a * b))) * c by GROUP_1:def 3
.= c" * (a" * ((c * c") * (b" * (a * b)))) * c by GROUP_1:def 3
.= c" * a" * ((c * c") * (b" * (a * b))) * c by GROUP_1:def 3
.= c" * a" * (c * (c" * (b" * (a * b)))) * c by GROUP_1:def 3
.= (a" |^ c) * (c" * (b" * (a * b))) * c by GROUP_1:def 3
.= (a |^ c)" * (c" * (b" * (a * b))) * c by GROUP_3:26
.= (a |^ c)" * (c" * (b" * 1_G * (a * b))) * c by GROUP_1:def 4
.= (a |^ c)" * (c" * (b" * (c * c") * (a * b))) * c by GROUP_1:def 5
.= (a |^ c)" * (c" * (b" * ((c * c") * (a * b)))) * c by GROUP_1:def 3
.= (a |^ c)" * (c" * b" * ((c * c") * (a * b))) * c by GROUP_1:def 3
.= (a |^ c)" * (c" * b" * (c * (c" * (a * b)))) * c by GROUP_1:def 3
.= (a |^ c)" * ((b" |^ c) * (c" * (a * b))) * c by GROUP_1:def 3
.= (a |^ c)" * ((b |^ c)" * (c" * (a * b))) * c by GROUP_3:26
.= (a |^ c)" * ((b |^ c)" * (c" * (a * 1_G * b))) * c by GROUP_1:def 4
.= (a |^ c)" * ((b |^ c)" * (c" * (a * (c * c") * b))) * c by GROUP_1:def 5
.= (a |^ c)" * ((b |^ c)" * (c" * (a * ((c * c") * b)))) * c by
GROUP_1:def 3
.= (a |^ c)" * ((b |^ c)" * (c" * a * ((c * c") * b))) * c by GROUP_1:def 3
.= (a |^ c)" * ((b |^ c)" * (c" * a * (c * (c" * b)))) * c by GROUP_1:def 3
.= (a |^ c)" * ((b |^ c)" * ((a |^ c) * (c" * b))) * c by GROUP_1:def 3
.= (a |^ c)" * (((b |^ c)" * ((a |^ c) * (c" * b))) * c) by GROUP_1:def 3
.= (a |^ c)" * (((b |^ c)" * ((a |^ c) * (c" * b) * c))) by GROUP_1:def 3
.= (a |^ c)" * (((b |^ c)" * ((a |^ c) * (b |^ c)))) by GROUP_1:def 3
.= [.a |^ c,b |^ c.] by Th16;
end;
theorem
[.a,b.] = (a" |^ 2) * ((a * b") |^ 2)* (b |^ 2)
proof
thus [.a,b.] = (a" * b") * (a * b) by Th16
.= (a" * 1_G * b") * (a * b) by GROUP_1:def 4
.= (a" * 1_G * b") * (a * 1_G * b) by GROUP_1:def 4
.= (a" * (a" * a) * b") * (a * 1_G * b) by GROUP_1:def 5
.= (a" * (a" * a) * b") * (a * (b" * b) * b) by GROUP_1:def 5
.= (a" * a" * a * b") * (a * (b" * b) * b) by GROUP_1:def 3
.= (a" |^ 2 * a * b") * (a * (b" * b) * b) by GROUP_1:27
.= (a" |^ 2 * a * b") * (a * ((b" * b) * b)) by GROUP_1:def 3
.= (a" |^ 2 * a * b") * (a * (b" * (b * b))) by GROUP_1:def 3
.= (a" |^ 2 * a * b") * (a * (b" * (b |^ 2))) by GROUP_1:27
.= (a" |^ 2 * (a * b")) * (a * (b" * (b |^ 2))) by GROUP_1:def 3
.= (a" |^ 2) * ((a * b") * (a * (b" * (b |^ 2)))) by GROUP_1:def 3
.= (a" |^ 2) * ((a * b") * (a * b" * (b |^ 2))) by GROUP_1:def 3
.= (a" |^ 2) * ((a * b") * (a * b") * (b |^ 2)) by GROUP_1:def 3
.= (a" |^ 2) * ((a * b") * (a * b")) * (b |^ 2) by GROUP_1:def 3
.= (a" |^ 2) * ((a * b") |^ 2) * (b |^ 2) by GROUP_1:27;
end;
theorem Th25:
[.a * b,c.] = [.a,c.] |^ b * [.b,c.]
proof
thus [.a * b,c.] = ((a * b)" * c") * (a * b * c) by Th16
.= (b" * a" * c") * (a * b * c) by GROUP_1:17
.= (b" * a" * c") * (a * 1_G * b * c) by GROUP_1:def 4
.= (b" * a" * c") * (a * (c * c") * b * c) by GROUP_1:def 5
.= (b" * a" * c") * (a * (c * 1_G * c") * b * c) by GROUP_1:def 4
.= (b" * a" * c") * (a * (c * (b * b") * c") * b * c) by GROUP_1:def 5
.= b" * (a" * c") * (a * (c * (b * b") * c") * b * c) by GROUP_1:def 3
.= b" * (a" * c") * (a * (c * (b * b") * c") * (b * c)) by GROUP_1:def 3
.= b" * (a" * c") * (a * (c * b * b" * c") * (b * c)) by GROUP_1:def 3
.= b" * (a" * c") * (a * (c * b * (b" * c")) * (b * c)) by GROUP_1:def 3
.= b" * (a" * c") * (a * (c * (b * (b" * c"))) * (b * c)) by GROUP_1:def 3
.= b" * (a" * c") * (a * c * (b * (b" * c")) * (b * c)) by GROUP_1:def 3
.= b" * (a" * c") * (a * c * ((b * (b" * c")) * (b * c))) by GROUP_1:def 3
.= b" * (a" * c") * (a * c) * ((b * (b" * c")) * (b * c)) by GROUP_1:def 3
.= b" * ((a" * c") * (a * c)) * ((b * (b" * c")) * (b * c)) by
GROUP_1:def 3
.= b" * ((a" * c") * (a * c)) * (b * ((b" * c") * (b * c))) by
GROUP_1:def 3
.= b" * ((a" * c") * (a * c)) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= [.a,c.] |^ b * ((b" * c") * (b * c)) by Th16
.= [.a,c.] |^ b * [.b,c.] by Th16;
end;
theorem
[.a,b * c.] = [.a,c.] * ([.a,b.] |^ c)
proof
thus [.a,b * c.] = (a" * (b * c)") * (a * (b * c)) by Th16
.= (a" * (c" * b")) * (a * (b * c)) by GROUP_1:17
.= (a" * (c" * 1_G * b")) * (a * (b * c)) by GROUP_1:def 4
.= (a" * (c" * (a * a") * b")) * (a * (b * c)) by GROUP_1:def 5
.= (a" * (c" * (a * 1_G * a") * b")) * (a * (b * c)) by GROUP_1:def 4
.= (a" * (c" * (a * (c * c") * a") * b")) * (a * (b * c)) by GROUP_1:def 5
.= (a" * (c" * (a * c * c" * a") * b")) * (a * (b * c)) by GROUP_1:def 3
.= (a" * (c" * ((a * c) * (c" * a")) * b")) * (a * (b * c)) by
GROUP_1:def 3
.= (a" * (c" * (((a * c) * (c" * a")) * b"))) * (a * (b * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c * (c" * a") * b")) * (a * (b * c)) by GROUP_1:def 3
.= ((a" * c") * ((a * c) * (c" * a")) * b") * (a * (b * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (c" * a") * b" * (a * (b * c)) by GROUP_1:def 3
.= ((a" * c") * (a * c)) * ((c" * a") * b") * (a * (b * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (((c" * a") * b") * (a * (b * c))) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (((c" * a") * b") * ((a * b) * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * ((c" * (a" * b")) * ((a * b) * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (c" * ((a" * b") * ((a * b) * c))) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (c" * ((a" * b") * (a * b) * c)) by
GROUP_1:def 3
.= ((a" * c") * (a * c)) * (c" * ((a" * b") * (a * b)) * c) by
GROUP_1:def 3
.= [.a,c.] * (c" * ((a" * b") * (a * b)) * c) by Th16
.= [.a,c.] * ([.a,b.] |^ c) by Th16;
end;
theorem Th27:
[.a",b.] = [.b,a.] |^ a"
proof
thus [.a",b.] = a"" * (b" * (a" * b)) by Th16
.= a"" * (b" * (a" * b)) * 1_G by GROUP_1:def 4
.= a"" * (b" * (a" * b)) * (a * a") by GROUP_1:def 5
.= a"" * (b" * (a" * b)) * a * a" by GROUP_1:def 3
.= a"" * ((b" * (a" * b)) * a) * a" by GROUP_1:def 3
.= [.b,a.] |^ a" by Th16;
end;
theorem Th28:
[.a,b".] = [.b,a.] |^ b"
proof
thus [.a,b".] = a" * b * a * b" .= 1_G * (a" * b * a * b") by GROUP_1:def 4
.= (b"" * b") * (a" * b * a * b") by GROUP_1:def 5
.= (b"" * b") * (a" * b * a) * b" by GROUP_1:def 3
.= b"" * (b" * (a" * b * a)) * b" by GROUP_1:def 3
.= [.b,a.] |^ b" by Th16;
end;
theorem
[.a",b".] = [.a,b.] |^ (a * b)" & [.a",b".] = [.a,b.] |^ (b * a)"
proof
thus [.a",b".] = [.b",a.] |^ a" by Th27
.= ([.a,b.] |^ b") |^ a" by Th27
.= [.a,b.] |^ (b" * a") by GROUP_3:24
.= [.a,b.] |^ (a * b)" by GROUP_1:17;
thus [.a",b".] = [.b,a".] |^ b" by Th28
.= [.a,b.] |^ a" |^ b" by Th28
.= [.a,b.] |^ (a" * b") by GROUP_3:24
.= [.a,b.] |^ (b * a)" by GROUP_1:17;
end;
theorem
[.a,b |^ a".] = [.b,a".]
proof
thus [.a,b |^ a".] = a" * (b" |^ a") * a * (b |^ a") by GROUP_3:26
.= a" * (a"" * (b" * a")) * a * (b |^ a") by GROUP_1:def 3
.= (b" * a") * a * (b |^ a") by GROUP_3:1
.= b" * (a"" * b * a") by GROUP_3:1
.= [.b,a".] by Th16;
end;
theorem
[.a |^ b",b.] = [.b",a.]
proof
thus [.a |^ b",b.] = (a" |^ b") * b" * (a |^ b") * b by GROUP_3:26
.= (a" |^ b") * (b" * (b"" * a * b")) * b by GROUP_1:def 3
.= (a" |^ b") * (b" * (b"" * (a * b"))) * b by GROUP_1:def 3
.= (a" |^ b") * (a * b") * b by GROUP_3:1
.= (a" |^ b") * ((a * b") * b) by GROUP_1:def 3
.= [.b",a.] by GROUP_3:1;
end;
theorem
[.a |^ n,b.] = a |^ (- n) * ((a |^ b) |^ n)
proof
thus [.a |^ n,b.] = (a |^ n)" * (b" * (a |^ n) * b) by Th16
.= a |^ (- n) * ((a |^ n) |^ b) by GROUP_1:36
.= a |^ (- n) * ((a |^ b) |^ n) by GROUP_3:27;
end;
theorem
[.a,b |^ n.] = (b |^ a) |^ (- n) * (b |^ n)
proof
thus [.a,b |^ n.] = (b |^ (- n)) |^ a * (b |^ n) by GROUP_1:36
.= (b |^ a) |^ (- n) * (b |^ n) by GROUP_3:28;
end;
theorem
[.a |^ i,b.] = a |^ (- i) * ((a |^ b) |^ i)
proof
thus [.a |^ i,b.] = (a |^ i)" * (b" * (a |^ i) * b) by Th16
.= a |^ (- i) * ((a |^ i) |^ b) by GROUP_1:36
.= a |^ (- i) * ((a |^ b) |^ i) by GROUP_3:28;
end;
theorem
[.a,b |^ i.] = (b |^ a) |^ (- i) * (b |^ i)
proof
thus [.a,b |^ i.] = (b |^ (- i)) |^ a * (b |^ i) by GROUP_1:36
.= (b |^ a) |^ (- i) * (b |^ i) by GROUP_3:28;
end;
theorem Th36:
[.a,b.] = 1_G iff a * b = b * a
proof
thus [.a,b.] = 1_G implies a * b = b * a
proof
assume [.a,b.] = 1_G;
then (b * a)" * (a * b) = 1_G by Th17;
then a * b = (b * a)"" by GROUP_1:12;
hence thesis;
end;
assume a * b = b * a;
then
A1: (b * a)" = b" * a" by GROUP_1:18;
[.a,b.] = (b * a)" * (a * b) by Th17;
hence [.a,b.] = (b" * a") * a * b by A1,GROUP_1:def 3
.= b" * b by GROUP_3:1
.= 1_G by GROUP_1:def 5;
end;
Lm1: for G being commutative Group for a,b being Element of G holds a * b = b
* a;
theorem
G is commutative Group iff for a,b holds [.a,b.] = 1_G
proof
thus G is commutative Group implies for a,b holds [.a,b.] = 1_G
proof
assume
A1: G is commutative Group;
let a,b;
a * b = b * a by A1,Lm1;
hence thesis by Th36;
end;
assume
A2: for a,b holds [.a,b.] = 1_G;
G is commutative
proof
let a,b;
[.a,b.] = 1_G by A2;
hence thesis by Th36;
end;
hence thesis;
end;
theorem Th38:
a in H & b in H implies [.a,b.] in H
proof
assume
A1: a in H & b in H;
then a" in H & b" in H by GROUP_2:51;
then
A2: a" * b" in H by GROUP_2:50;
a * b in H by A1,GROUP_2:50;
then (a" * b") * (a * b) in H by A2,GROUP_2:50;
hence thesis by Th16;
end;
definition
let G,a,b,c;
func [.a,b,c.] -> Element of G equals
[.[.a,b.],c.];
correctness;
end;
theorem
[.a,b,1_G.] = 1_G & [.a,1_G,b.] = 1_G & [.1_G,a,b.] = 1_G
proof
thus [.a,b,1_G.] = 1_G by Th19;
thus [.a,1_G,b.] = [.1_G,b.] by Th19
.= 1_G by Th19;
thus [.1_G,a,b.] = [.1_G,b.] by Th19
.= 1_G by Th19;
end;
theorem
[.a,a,b.] = 1_G
proof
thus [.a,a,b.] = [.1_G,b.] by Th20
.= 1_G by Th19;
end;
theorem
[.a,b,a.] = [.a |^ b,a.]
proof
thus [.a,b,a.] = [.b,a.] * a" * [.a,b.] * a by Th22
.= (a" |^ b) * (a" * b" * a * b) * a by GROUP_3:1
.= (a |^ b)" * (a" * b" * a * b) * a by GROUP_3:26
.= (a |^ b)" * (a" * b" * (a * b)) * a by GROUP_1:def 3
.= (a |^ b)" * (a" * (b" * (a * b))) * a by GROUP_1:def 3
.= (a |^ b)" * (a" * (a |^ b)) * a by GROUP_1:def 3
.= [.a |^ b,a.] by Th16;
end;
theorem
[.b,a,a.] = ([.b,a".] * [.b,a.]) |^ a
proof
thus [.b,a,a.] = [.a,b.] * a" * [.b,a.] * a by Th22
.= (a" * (b" * (a * b))) * a" * [.b,a.] * a by Th16
.= (a" * ((b" * (a"" * b))) * a") * [.b,a.] * a
.= (a" * (((b" * (a"" * b))) * a")) * [.b,a.] * a by GROUP_1:def 3
.= a" * [.b,a".] * [.b,a.] * a by Th16
.= ([.b,a".] * [.b,a.]) |^ a by GROUP_1:def 3;
end;
theorem
[.a,b,b |^ a.] = [.b,[.b,a.].]
proof
thus [.a,b,b |^ a.] = [.b,a.] * (b |^ a)" * [.a,b.] * (b |^ a) by Th22
.= (b" * a" * b * a) * (b" |^ a) * [.a,b.] * (b |^ a) by GROUP_3:26
.= (b" * a" * b * a) * (a" * (b" * a)) * [.a,b.] * (b |^ a) by
GROUP_1:def 3
.= (b" * a" * b * a) * a" * (b" * a) * [.a,b.] * (b |^ a) by GROUP_1:def 3
.= (b" * a" * b) * (b" * a) * [.a,b.] * (b |^ a) by GROUP_3:1
.= b" * a" * (b * (b" * a)) * [.a,b.] * (b |^ a) by GROUP_1:def 3
.= b" * a" * a * [.a,b.] * (b |^ a) by GROUP_3:1
.= b" * (a"* b"* a * b) * (b |^ a) by GROUP_3:1
.= b" * (a"* b"* a * b) * 1_G * (a" * b * a) by GROUP_1:def 4
.= b" * [.a,b.] * (b * b") * (a" * b * a) by GROUP_1:def 5
.= b" * [.a,b.] * ((b * b") * (a" * b * a)) by GROUP_1:def 3
.= b" * [.a,b.] * (b * (b" * (a" * b * a))) by GROUP_1:def 3
.= b" * [.a,b.] * (b * [.b,a.]) by Th16
.= b" * [.b,a.]" * (b * [.b,a.]) by Th22
.= [.b,[.b,a.].] by Th16;
end;
theorem
[.a * b,c.] = [.a,c.] * [.a,c,b.] * [.b,c.]
proof
[.a,c.] * [.a,c,b.] * [.b,c.] = a" * c" * a * c * ([.c,a.] * b" * [.a,c
.] * b) * [.b,c.] by Th22
.= a" * c" * a * c * ((c" * a") * (c * a) * b" * [.a,c.] * b) * [.b,c.]
by Th16
.= a" * c" * a * c * ((a * c)" * (c * a) * b" * [.a,c.] * b) * [.b,c.]
by GROUP_1:17
.= a" * c" * (a * c) * ((a * c)" * (c * a) * b" * [.a,c.] * b) * [.b,c.]
by GROUP_1:def 3
.= a" * c" * ((a * c) * ((a * c)" * (c * a) * b" * [.a,c.] * b)) * [.b,c
.] by GROUP_1:def 3
.= a" * c" * ((a * c) * ((a * c)" * (c * a) * b" * ([.a,c.] * b))) * [.b
,c.] by GROUP_1:def 3
.= a" * c" * ((a * c) * ((a * c)" * (c * a) * (b" * ([.a,c.] * b)))) *
[.b,c.] by GROUP_1:def 3
.= a" * c" * ((a * c) * ((a * c)" * ((c * a) * (b" * ([.a,c.] * b))))) *
[.b,c.] by GROUP_1:def 3
.= a" * c" * ((a * c) * (a * c)" * ((c * a) * (b" * ([.a,c.] * b)))) *
[.b,c.] by GROUP_1:def 3
.= a" * c" * (1_G * ((c * a) * (b" * ([.a,c.] * b)))) * [.b,c.] by
GROUP_1:def 5
.= a" * c" * ((c * a) * (b" * ([.a,c.] * b))) * [.b,c.] by GROUP_1:def 4
.= a" * c" * (c * a) * (b" * ([.a,c.] * b)) * [.b,c.] by GROUP_1:def 3
.= (c * a)" * (c * a) * (b" * ([.a,c.] * b)) * [.b,c.] by GROUP_1:17
.= 1_G * (b" * ([.a,c.] * b)) * [.b,c.] by GROUP_1:def 5
.= b" * ([.a,c.] * b) * [.b,c.] by GROUP_1:def 4
.= b" * ((a" * c" * a * c) * b) * ((b" * c") * (b * c)) by Th16
.= b" * ((a" * c" * a) * c) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * (a" * c" * (a * c)) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * (a" * (c" * (a * c))) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * a" * (c" * (a * c)) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * a" * c" * (a * c) * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * a" * c" * a * c * b * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * a" * c" * a * (c * b) * ((b" * c") * (b * c)) by GROUP_1:def 3
.= b" * a" * c" * a * (c * b) * (b" * c") * (b * c) by GROUP_1:def 3
.= b" * a" * c" * a * (c * b) * (c * b)" * (b * c) by GROUP_1:17
.= b" * a" * c" * a * ((c * b) * (c * b)") * (b * c) by GROUP_1:def 3
.= b" * a" * c" * a * 1_G * (b * c) by GROUP_1:def 5
.= b" * a" * c" * a * (b * c) by GROUP_1:def 4
.= (a * b)" * c" * a * (b * c) by GROUP_1:17
.= (a * b)" * c" * (a * (b * c)) by GROUP_1:def 3
.= (a * b)" * c" * (a * b * c) by GROUP_1:def 3;
hence thesis by Th16;
end;
theorem
[.a,b * c.] = [.a,c.] * [.a,b.] * [.a,b,c.]
proof
[.a,c.] * [.a,b.] * [.a,b,c.] = [.a,c.] * ([.a,b.] * [.[.a,b.],c.]) by
GROUP_1:def 3
.= [.a,c.] * ((a" * b") * (a * b) * ([.a,b.]" * c" * [.a,b.] * c)) by Th16
.= [.a,c.] * ((a" * b") * (a * b) * ([.b,a.] * c" * [.a,b.] * c)) by Th22
.= [.a,c.] * ((a" * b") * (a * b) * ((b" * a" * (b * a)) * c" * [.a,b.]
* c)) by Th16
.= [.a,c.] * ((a" * b") * ((a * b) * (((b" * a") * (b * a)) * c" * [.a,b
.] * c))) by GROUP_1:def 3
.= [.a,c.] * ((a" * b") * ((a * b) * (((b" * a") * (b * a)) * c" * ([.a,
b.] * c)))) by GROUP_1:def 3
.= [.a,c.] * ((a" * b") * ((a * b) * (((b" * a") * (b * a)) * (c" * ([.a
,b.] * c))))) by GROUP_1:def 3
.= [.a,c.] * ((a" * b") * ((a * b) * ((b" * a") * (b * a)) * (c" * ([.a,
b.] * c)))) by GROUP_1:def 3
.= [.a,c.] * ((a" * b") * ((a * b) * (b" * a") * (b * a) * (c" * ([.a,b
.] * c)))) by GROUP_1:def 3
.= [.a,c.] * ((a" * b") * ((a * b) * (a * b)" * (b * a) * (c" * ([.a,b.]
* c)))) by GROUP_1:17
.= [.a,c.] * ((a" * b") * (1_G * (b * a) * (c" * ([.a,b.] * c)))) by
GROUP_1:def 5
.= [.a,c.] * ((a" * b") * ((b * a) * (c" * ([.a,b.] * c)))) by
GROUP_1:def 4
.= [.a,c.] * ((a" * b") * (b * a) * (c" * ([.a,b.] * c))) by GROUP_1:def 3
.= [.a,c.] * ((b * a)" * (b * a) * (c" * ([.a,b.] * c))) by GROUP_1:17
.= [.a,c.] * (1_G * (c" * ([.a,b.] * c))) by GROUP_1:def 5
.= [.a,c.] * (c" * ([.a,b.] * c)) by GROUP_1:def 4
.= (a" * c") * (a * c) * (c" * ([.a,b.] * c)) by Th16
.= (a" * c") * (a * c) * (c" * ((a" * (b" * a * b)) * c)) by Th16
.= (a" * c") * (a * c) * (c" * (a" * (b" * a * b)) * c) by GROUP_1:def 3
.= (a" * c") * (a * c) * ((c" * a") * (b" * a * b) * c) by GROUP_1:def 3
.= (a" * c") * (a * c) * ((c" * a") * ((b" * a * b) * c)) by GROUP_1:def 3
.= (a" * c") * (a * c) * (c" * a") * ((b" * a * b) * c) by GROUP_1:def 3
.= (a" * c") * ((a * c) * (c" * a")) * ((b" * a * b) * c) by GROUP_1:def 3
.= (a" * c") * ((a * c) * (a * c)") * ((b" * a * b) * c) by GROUP_1:17
.= (a" * c") * 1_G * ((b" * a * b) * c) by GROUP_1:def 5
.= (a" * c") * ((b" * a * b) * c) by GROUP_1:def 4
.= (a" * c") * (b" * a * b) * c by GROUP_1:def 3
.= (a" * c") * (b" * (a * b)) * c by GROUP_1:def 3
.= a" * c" * b" * (a * b) * c by GROUP_1:def 3
.= a" * (c" * b") * (a * b) * c by GROUP_1:def 3
.= a" * (c" * b") * ((a * b) * c) by GROUP_1:def 3
.= a" * (c" * b") * (a * (b * c)) by GROUP_1:def 3
.= a" * (b * c)" * (a * (b * c)) by GROUP_1:17;
hence thesis by Th16;
end;
::
:: P. Hall Identity.
::
theorem
([.a,b",c.] |^ b) * ([.b,c",a.] |^ c) * ([.c,a",b.] |^ a) = 1_G
proof
set d = a" * [.b,c".] * a;
set e = c" * [.a,b".] * c;
set f = b" * [.c,a".] * b;
set x = [.a,b",c.] |^ b;
set y = [.b,c",a.] |^ c;
set z = [.c,a",b.] |^ a;
A1: [.c",b.] = c"" * (b" * c" * b) by Th16;
A2: [.a",c.] = a"" * (c" * a" * c) by Th16;
A3: [.b",a.] = b"" * (a" * b" * a) by Th16;
[.a,b",c.] = [.a,b".]" * e by Th16
.= [.b",a.] * e by Th22;
then
A4: [.a,b",c.] |^ b = b" * (b"" * ((a" * b" * a) * e)) * b by A3,GROUP_1:def 3
.= (a" * b" * a) * e * b by GROUP_3:1;
[.c,a",b.] = [.c,a".]" * f by Th16
.= [.a",c.] * f by Th22;
then
A5: z = a" * (a"" * ((c" * a" * c) * f)) * a by A2,GROUP_1:def 3
.= (c" * a" * c) * f * a by GROUP_3:1;
[.b,c",a.] = [.b,c".]" * (a" * [.b,c".] * a) by Th16
.= [.c",b.] * (a" * [.b,c".] * a) by Th22;
then [.b,c",a.] |^ c = c" * (c"" * ((b" * c" * b) * d)) * c by A1,
GROUP_1:def 3
.= (b" * c" * b) * d * c by GROUP_3:1
.= (b" * c" * b) * (d * c) by GROUP_1:def 3
.= b" * (c" * b) * (d * c) by GROUP_1:def 3
.= b" * ((c" * b) * (d * c)) by GROUP_1:def 3;
then x * y = (a" * b" * a) * e * (b * (b" * ((c" * b) * (d * c)))) by A4,
GROUP_1:def 3
.= (a" * b" * a) * e * ((c" * b) * (d * c)) by GROUP_3:1
.= (a" * b" * a) * (c" * ([.a,b".] * c)) * ((c" * b) * (d * c)) by
GROUP_1:def 3
.= (a" * b" * a) * c" * ([.a,b".] * c) * ((c" * b) * (d * c)) by
GROUP_1:def 3
.= (a" * b" * a) * c" * (([.a,b".] * c) * ((c" * b) * (d * c))) by
GROUP_1:def 3
.= (a" * b" * a) * c" * (([.a,b".] * c) * (c" * b) * (d * c)) by
GROUP_1:def 3
.= (a" * b" * a) * c" * (([.a,b".] * c) * c" * b * (d * c)) by
GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"" * a) * b" * b * (d * c)) by GROUP_3:1
.= (a" * b" * a) * c" * ((a" * b"" * a) * (d * c)) by GROUP_3:1
.= (a" * b" * a) * c" * ((a" * b"" * a) * (a" * [.b,c".] * (a * c))) by
GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"" * a) * (a" * ([.b,c".] * (a * c))))
by GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"" * a) * a" * ([.b,c".] * (a * c))) by
GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"") * ([.b,c".] * (a * c))) by GROUP_3:1
.= (a" * b" * a) * c" * ((a" * b"") * [.b,c".] * (a * c)) by GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"") * (b" * (c"" * b * c")) * (a * c))
by Th16
.= (a" * b" * a) * c" * ((a" * b"") * ((b" * (c"" * b * c")) * (a * c)))
by GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"") * (b" * ((c"" * b * c") * (a * c))))
by GROUP_1:def 3
.= (a" * b" * a) * c" * ((a" * b"") * b" * ((c"" * b * c") * (a * c)))
by GROUP_1:def 3
.= (a" * b" * a) * c" * (a" * ((c"" * b * c") * (a * c))) by GROUP_3:1;
then
x * y * z = ((a" * b" * a) * c" * (a" * (c"" * b * c") * (a * c))) * ((
c" * a" * c) * f * a) by A5,GROUP_1:def 3
.= ((a" * b" * a) * (c" * (a" * (c"" * b * c") * (a * c)))) * ((c" * a"
* c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * (c" * (a" * ((c"" * b * c") * (a * c))))) * ((c" * a
" * c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * (a" * ((c"" * b * c") * (a * c)))) * ((c" * a"
* c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * (a" * (c"" * (b * c") * (a * c)))) * ((c" * a"
* c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * (a" * (c"" * (b * c" * (a * c))))) * ((c" * a"
* c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * a" * (c"" * (b * c" * (a * c)))) * ((c" * a" *
c) * f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * a" * c"" * (b * c" * (a * c))) * (c" * a" * c *
f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * a" * c"" * (b * (c" * (a * c)))) * (c" * a" * c
* f * a) by GROUP_1:def 3
.= ((a" * b" * a) * c" * a" * c"" * b * (c" * (a * c))) * (c" * a" * c *
f * a) by GROUP_1:def 3
.= (((a" * b" * a) * c" * a" * c"") * b * c" * (a * c)) * (c" * a" * c *
f * a) by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((a * c) * (c" * a" * c
* f * a)) by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((a * c) * (c" * a" * c
* (f * a))) by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((a * c) * (c" * a" * (c
* (f * a)))) by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((a * c) * (c" * a") * (
c * (f * a))) by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((a * c) * (a * c)" * (c
* (f * a))) by GROUP_1:17
.= (((a" * b") * a * c") * a" * c"" * b * c") * (1_G * (c * (f * a))) by
GROUP_1:def 5
.= (((a" * b") * a * c") * a" * c"" * b * c") * ((c * (f * a))) by
GROUP_1:def 4
.= (((a" * b") * a * c") * a" * c"" * b * c") * c * (f * a) by
GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b) * (f * a) by GROUP_3:1
.= (((a" * b") * a * c") * a" * c"" * b) * (b" * [.c,a".] * (b * a)) by
GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b) * (b" * ([.c,a".] * (b * a)))
by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"" * b) * b" * ([.c,a".] * (b * a)) by
GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"") * ([.c,a".] * (b * a)) by GROUP_3:1
.= (((a" * b") * a * c") * a" * c"") * (c" * (a"" * c * a") * (b * a))
by Th16
.= (((a" * b") * a * c") * a" * c"") * (c" * ((a"" * c * a") * (b * a)))
by GROUP_1:def 3
.= (((a" * b") * a * c") * a" * c"") * c" * ((a"" * c * a") * (b * a))
by GROUP_1:def 3
.= (((a" * b") * a * c") * a") * ((a"" * c * a") * (b * a)) by GROUP_3:1
.= (((a" * b") * a * c") * a") * (a"" * (c * a") * (b * a)) by
GROUP_1:def 3
.= (((a" * b") * a * c") * a") * (a"" * ((c * a") * (b * a))) by
GROUP_1:def 3
.= (((a" * b") * a * c") * a") * a"" * ((c * a") * (b * a)) by
GROUP_1:def 3
.= ((a" * b") * a * c") * ((c * a") * (b * a)) by GROUP_3:1
.= ((a" * b") * a * c") * (c * a") * (b * a) by GROUP_1:def 3
.= (a" * b") * (a * c") * (c * a") * (b * a) by GROUP_1:def 3
.= (a" * b") * (a * c") * (c"" * a") * (b * a)
.= (a" * b") * (a * c") * (a * c")" * (b * a) by GROUP_1:17
.= (a" * b") * ((a * c") * (a * c")") * (b * a) by GROUP_1:def 3
.= (a" * b") * 1_G * (b * a) by GROUP_1:def 5
.= (a" * b") * (b * a) by GROUP_1:def 4
.= (b * a)" * (b * a) by GROUP_1:17;
hence thesis by GROUP_1:def 5;
end;
definition
let G,A,B;
func commutators(A,B) -> Subset of G equals
{[.a,b.] : a in A & b in B};
coherence
proof
defpred P[Element of G,Element of G] means $1 in A & $2 in B;
deffunc F(Element of G,Element of G) = [.$1,$2.];
{F(a,b) : P[a,b]} is Subset of G from DOMAIN_1:sch 9;
hence thesis;
end;
end;
theorem Th47:
x in commutators(A,B) iff ex a,b st x = [.a,b.] & a in A & b in B;
theorem
commutators({} the carrier of G,A) = {} & commutators(A,{} the carrier
of G) = {}
proof
commutators({} the carrier of G,A) c= {}
proof
let x be object;
assume x in commutators({} the carrier of G,A);
then ex a,b st x = [.a,b.] & a in {} the carrier of G & b in A;
hence thesis;
end;
hence commutators({} the carrier of G,A) = {};
thus commutators(A,{} the carrier of G) c= {}
proof
let x be object;
assume x in commutators(A,{} the carrier of G);
then ex a,b st x = [.a,b.] & a in A & b in {} the carrier of G;
hence thesis;
end;
thus thesis;
end;
theorem
commutators({a},{b}) = {[.a,b.]}
proof
thus commutators({a},{b}) c= {[.a,b.]}
proof
let x be object;
assume x in commutators({a},{b});
then consider c,d such that
A1: x = [.c,d.] and
A2: c in {a} & d in {b};
c = a & b = d by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {[.a,b.]};
then
A3: x = [.a,b.] by TARSKI:def 1;
a in {a} & b in {b} by TARSKI:def 1;
hence thesis by A3;
end;
theorem Th50:
A c= B & C c= D implies commutators(A,C) c= commutators(B,D)
proof
assume
A1: A c= B & C c= D;
let x be object;
assume x in commutators(A,C);
then ex a,c st x = [.a,c.] & a in A & c in C;
hence thesis by A1;
end;
theorem Th51:
G is commutative Group iff for A,B st A <> {} & B <> {} holds
commutators(A,B) = {1_G}
proof
thus G is commutative Group implies for A,B st A <> {} & B <> {} holds
commutators(A,B) = {1_G}
proof
assume
A1: G is commutative Group;
let A,B;
assume
A2: A <> {} & B <> {};
thus commutators(A,B) c= {1_G}
proof
let x be object;
assume x in commutators(A,B);
then consider a,b such that
A3: x = [.a,b.] and
a in A and
b in B;
x = a" * (b" * a) * b by A3,Th16
.= a" * (a * b") * b by A1,Lm1
.= b" * b by GROUP_3:1
.= 1_G by GROUP_1:def 5;
hence thesis by TARSKI:def 1;
end;
set b = the Element of B;
set a = the Element of A;
reconsider a,b as Element of G by A2,TARSKI:def 3;
let x be object;
assume x in {1_G};
then
A4: x = 1_G by TARSKI:def 1;
[.a,b.] = a" * (b" * a) * b by Th16
.= a" * (a * b") * b by A1,Lm1
.= b" * b by GROUP_3:1
.= x by A4,GROUP_1:def 5;
hence thesis by A2;
end;
assume
A5: for A,B st A <> {} & B <> {} holds commutators(A,B) = {1_G};
G is commutative
proof
let a,b;
a in {a} & b in {b} by TARSKI:def 1;
then
A6: [.a,b.] in commutators({a},{b});
commutators({a},{b}) ={1_G} by A5;
then [.a,b.] = 1_G by A6,TARSKI:def 1;
then (a" * b") * (a * b) = 1_G by Th16;
then (b * a)" * (a * b) = 1_G by GROUP_1:17;
then a * b = (b * a)"" by GROUP_1:12;
hence thesis;
end;
hence thesis;
end;
definition
let G,H1,H2;
func commutators(H1,H2) -> Subset of G equals
commutators(carr H1,carr H2);
correctness;
end;
theorem Th52:
x in commutators(H1,H2) iff ex a,b st x = [.a,b.] & a in H1 & b in H2
proof
thus x in commutators(H1,H2) implies ex a,b st x = [.a,b.] & a in H1 & b in
H2
proof
assume x in commutators(H1,H2);
then consider a,b such that
A1: x = [.a,b.] and
A2: a in carr H1 & b in carr H2;
a in H1 & b in H2 by A2,STRUCT_0:def 5;
hence thesis by A1;
end;
given a,b such that
A3: x = [.a,b.] and
A4: a in H1 & b in H2;
a in carr H1 & b in carr H2 by A4,STRUCT_0:def 5;
hence thesis by A3;
end;
theorem Th53:
1_G in commutators(H1,H2)
proof
A1: 1_G in H2 by GROUP_2:46;
[.1_G,1_G.] = 1_G & 1_G in H1 by Th19,GROUP_2:46;
hence thesis by A1,Th52;
end;
theorem
commutators((1).G,H) = {1_G} & commutators(H,(1).G) = {1_G}
proof
A1: commutators((1).G,H) c= {1_G}
proof
let x be object;
assume x in commutators((1).G,H);
then consider a,b such that
A2: x = [.a,b.] and
A3: a in (1).G and
b in H by Th52;
a = 1_G by A3,Th1;
then x = 1_G by A2,Th19;
hence thesis by TARSKI:def 1;
end;
1_G in commutators((1).G,H) by Th53;
hence commutators((1).G,H) = {1_G} by A1,ZFMISC_1:33;
thus commutators(H,(1).G) c= {1_G}
proof
let x be object;
assume x in commutators(H,(1).G);
then consider a,b such that
A4: x = [.a,b.] and
a in H and
A5: b in (1).G by Th52;
b = 1_G by A5,Th1;
then x = 1_G by A4,Th19;
hence thesis by TARSKI:def 1;
end;
1_G in commutators(H,(1).G) by Th53;
hence thesis by ZFMISC_1:31;
end;
theorem Th55:
for N being strict normal Subgroup of G holds commutators(H,N)
c= carr N & commutators(N,H) c= carr N
proof
let N be strict normal Subgroup of G;
thus commutators(H,N) c= carr N
proof
let x be object;
assume x in commutators(H,N);
then consider a,b such that
A1: x = [.a,b.] and
a in H and
A2: b in N by Th52;
b" in N by A2,GROUP_2:51;
then b" |^ a in N |^ a by GROUP_3:58;
then b" |^ a in N by GROUP_3:def 13;
then x in N by A1,A2,GROUP_2:50;
hence thesis by STRUCT_0:def 5;
end;
let x be object;
assume x in commutators(N,H);
then consider a,b such that
A3: x = [.a,b.] and
A4: a in N and
b in H by Th52;
a |^ b in N |^ b by A4,GROUP_3:58;
then
A5: a |^ b in N by GROUP_3:def 13;
x = a" * (a |^ b) & a" in N by A3,A4,Th16,GROUP_2:51;
then x in N by A5,GROUP_2:50;
hence thesis by STRUCT_0:def 5;
end;
theorem Th56:
H1 is Subgroup of H2 & H3 is Subgroup of H4 implies commutators(
H1,H3) c= commutators(H2,H4)
proof
assume H1 is Subgroup of H2 & H3 is Subgroup of H4;
then the carrier of H1 c= the carrier of H2 & the carrier of H3 c= the
carrier of H4 by GROUP_2:def 5;
hence thesis by Th50;
end;
theorem Th57:
G is commutative Group iff for H1,H2 holds commutators(H1,H2) = {1_G}
proof
thus G is commutative Group implies for H1,H2 holds commutators(H1,H2) = {
1_G} by Th51;
assume
A1: for H1,H2 holds commutators(H1,H2) = {1_G};
G is commutative
proof
let a,b;
b in {b} by TARSKI:def 1;
then
A2: b in gr{b} by GROUP_4:29;
a in {a} by TARSKI:def 1;
then a in gr{a} by GROUP_4:29;
then [.a,b.] in commutators(gr{a},gr{b}) by A2,Th52;
then [.a,b.] in {1_G} by A1;
then [.a,b.] = 1_G by TARSKI:def 1;
hence thesis by Th36;
end;
hence thesis;
end;
definition
let G;
func commutators G -> Subset of G equals
commutators((Omega).G,(Omega).G);
correctness;
end;
theorem Th58:
x in commutators G iff ex a,b st x = [.a,b.]
proof
thus x in commutators G implies ex a,b st x = [.a,b.]
proof
assume x in commutators G;
then ex a,b st x = [.a,b.] & a in (Omega).G & b in (Omega).G by Th52;
hence thesis;
end;
given a,b such that
A1: x = [.a,b.];
thus thesis by A1;
end;
theorem
G is commutative Group iff commutators G = {1_G}
proof
thus G is commutative Group implies commutators G = {1_G} by Th57;
assume
A1: commutators G = {1_G};
G is commutative
proof
let a,b;
[.a,b.] in {1_G} by A1;
then [.a,b.] = 1_G by TARSKI:def 1;
hence thesis by Th36;
end;
hence thesis;
end;
definition
let G,A,B;
func [.A,B.] -> strict Subgroup of G equals
gr commutators(A,B);
correctness;
end;
theorem Th60:
a in A & b in B implies [.a,b.] in [.A,B.]
proof
assume a in A & b in B;
then [.a,b.] in commutators(A,B);
hence thesis by GROUP_4:29;
end;
theorem Th61:
x in [.A,B.] iff ex F,I st len F = len I & rng F c= commutators(
A,B) & x = Product(F |^ I)
proof
thus x in [.A,B.] implies ex F,I st len F = len I & rng F c= commutators(A,B
) & x = Product(F |^ I)
proof
assume
A1: x in [.A,B.];
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def 5;
a in gr commutators(A,B) by A1;
hence thesis by GROUP_4:28;
end;
thus thesis by GROUP_4:28;
end;
theorem
A c= C & B c= D implies [.A,B.] is Subgroup of [.C,D.] by Th50,GROUP_4:32;
definition
let G,H1,H2;
func [.H1,H2.] -> strict Subgroup of G equals
[.carr H1,carr H2.];
correctness;
end;
theorem
[.H1,H2.] = gr commutators(H1,H2);
theorem
x in [.H1,H2.] iff ex F,I st len F = len I & rng F c= commutators(H1,
H2) & x = Product(F |^ I) by Th61;
theorem Th65:
a in H1 & b in H2 implies [.a,b.] in [.H1,H2.]
proof
assume a in H1 & b in H2;
then a in carr H1 & b in carr H2 by STRUCT_0:def 5;
hence thesis by Th60;
end;
theorem
H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1,H3.] is
Subgroup of [.H2,H4.]
proof
assume H1 is Subgroup of H2 & H3 is Subgroup of H4;
then commutators(H1,H3) c= commutators(H2,H4) by Th56;
hence thesis by GROUP_4:32;
end;
theorem
for N being strict normal Subgroup of G holds [.N,H.] is Subgroup of N
& [.H,N.] is Subgroup of N
proof
let N be strict normal Subgroup of G;
now
let a;
assume a in [.N,H.];
then consider F,I such that
A1: len F = len I and
A2: rng F c= commutators(N,H) and
A3: a = Product(F |^ I) by Th61;
commutators(N,H) c= carr N by Th55;
then rng F c= carr N by A2;
then a in gr carr N by A1,A3,GROUP_4:28;
hence a in N by GROUP_4:31;
end;
hence [.N,H.] is Subgroup of N by GROUP_2:58;
now
let a;
assume a in [.H,N.];
then consider F,I such that
A4: len F = len I and
A5: rng F c= commutators(H,N) and
A6: a = Product(F |^ I) by Th61;
commutators(H,N) c= carr N by Th55;
then rng F c= carr N by A5;
then a in gr carr N by A4,A6,GROUP_4:28;
hence a in N by GROUP_4:31;
end;
hence thesis by GROUP_2:58;
end;
theorem Th68:
for N1,N2 being strict normal Subgroup of G holds [.N1,N2.] is
normal Subgroup of G
proof
let N1,N2 be strict normal Subgroup of G;
now
let a;
now
let b;
assume b in [.N1,N2.] |^ a;
then consider c such that
A1: b = c |^ a and
A2: c in [.N1,N2.] by GROUP_3:58;
consider F,I such that
A3: len F = len I and
A4: rng F c= commutators(carr N1,carr N2) and
A5: c = Product(F |^ I) by A2,GROUP_4:28;
A6: len(F |^ a) = len F by Def1;
A7: rng(F |^ a) c= commutators(carr N1,carr N2)
proof
let x be object;
assume x in rng(F |^ a);
then consider y being object such that
A8: y in dom(F |^ a) and
A9: (F |^ a).y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A8;
A10: y in dom F by A6,A8,FINSEQ_3:29;
then
A11: F.y = (F/.y) by PARTFUN1:def 6;
y in dom F by A6,A8,FINSEQ_3:29;
then F.y in rng F by FUNCT_1:def 3;
then consider d,e such that
A12: F.y = [.d,e.] and
A13: d in carr N1 and
A14: e in carr N2 by A4,Th47;
d in N1 by A13,STRUCT_0:def 5;
then d |^ a in N1 |^ a by GROUP_3:58;
then d |^ a in N1 by GROUP_3:def 13;
then
A15: d |^ a in carr N1 by STRUCT_0:def 5;
e in N2 by A14,STRUCT_0:def 5;
then e |^ a in N2 |^ a by GROUP_3:58;
then e |^ a in N2 by GROUP_3:def 13;
then
A16: e |^ a in carr N2 by STRUCT_0:def 5;
x = (F/.y) |^ a by A9,A10,Def1;
then x = [.d |^ a,e |^ a.] by A12,A11,Th23;
hence thesis by A15,A16;
end;
b = Product(F |^ I |^ a) by A1,A5,Th14
.= Product((F |^ a) |^ I) by Th15;
hence b in [.N1,N2.] by A3,A6,A7,GROUP_4:28;
end;
hence [.N1,N2.] |^ a is Subgroup of [.N1,N2.] by GROUP_2:58;
end;
hence thesis by GROUP_3:122;
end;
Lm2: [.N1,N2.] is Subgroup of [.N2,N1.]
proof
now
let a;
assume a in [.N1,N2.];
then consider F,I such that
len F = len I and
A1: rng F c= commutators(N1,N2) and
A2: a = Product(F |^ I) by Th61;
deffunc F(Nat) = (F/.$1)";
consider F1 such that
A3: len F1 = len F and
A4: for k be Nat st k in dom F1 holds F1.k = F(k) from FINSEQ_2:sch 1;
A5: dom F = Seg len F by FINSEQ_1:def 3;
A6: rng F1 c= commutators(N2,N1)
proof
let x be object;
assume x in rng F1;
then consider y being object such that
A7: y in dom F1 and
A8: F1.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A7;
y in dom F by A3,A7,FINSEQ_3:29;
then
A9: F/.y = F.y by PARTFUN1:def 6;
y in dom F by A3,A7,FINSEQ_3:29;
then F.y in rng F by FUNCT_1:def 3;
then consider b,c such that
A10: F.y = [.b,c.] and
A11: b in N1 & c in N2 by A1,Th52;
x = (F/.y)" by A4,A7,A8;
then x = [.c,b.] by A10,A9,Th22;
hence thesis by A11,Th52;
end;
A12: len(F |^ I) = len F by GROUP_4:def 3;
then
A13: dom(F |^ I) = Seg len F by FINSEQ_1:def 3;
deffunc F(Nat) = @(- @(I/.$1));
consider I1 such that
A14: len I1 = len F and
A15: for k be Nat st k in dom I1 holds I1.k = F(k) from FINSEQ_2:sch 1;
set J = F1 |^ I1;
A16: dom F1 = dom F by A3,FINSEQ_3:29;
A17: dom I1 = dom F by A14,FINSEQ_3:29;
A18: now
let k be Nat;
assume
A19: k in dom(F |^ I);
then
A20: k in dom F by A13,FINSEQ_1:def 3;
A21: J.k = (F1/.k) |^ @(I1/.k) & F1/.k = F1.k by A5,A16,A13,A19,GROUP_4:def 3
,PARTFUN1:def 6;
A22: I1.k = @(- @(I/.k)) by A15,A5,A17,A13,A19;
F1.k = (F/.k)" & I1.k = (I1/.k) by A4,A5,A16,A17,A13,A19,PARTFUN1:def 6;
then J.k = ((F/.k)" |^ @(I/.k))" by A21,A22,GROUP_1:36
.= ((F/.k) |^ @(I/.k))"" by GROUP_1:37
.= (F/.k) |^ @(I/.k);
hence (F |^ I).k = J.k by A20,GROUP_4:def 3;
end;
len J = len F by A3,GROUP_4:def 3;
then J = F |^ I by A12,A18,FINSEQ_2:9;
hence a in [.N2,N1.] by A2,A3,A14,A6,Th61;
end;
hence thesis by GROUP_2:58;
end;
theorem Th69:
[.N1,N2.] = [.N2,N1.]
proof
[.N1,N2.] is Subgroup of [.N2,N1.] & [.N2,N1.] is Subgroup of [.N1,N2.]
by Lm2;
hence thesis by GROUP_2:55;
end;
theorem Th70:
for N1,N2,N3 being strict normal Subgroup of G holds [.N1 "\/"
N2,N3.] = [.N1,N3.] "\/" [.N2,N3.]
proof
let N1,N2,N3 be strict normal Subgroup of G;
A1: [.N1,N3.] is normal Subgroup of G by Th68;
A2: [.N2,N3.] is normal Subgroup of G by Th68;
now
let a;
A3: N3 is Subgroup of N3 by GROUP_2:54;
N2 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then
A4: commutators(N2,N3) c= commutators(N1 "\/" N2,N3) by A3,Th56;
assume a in [.N1,N3.] "\/" [.N2,N3.];
then consider b,c such that
A5: a = b * c and
A6: b in [.N1,N3.] and
A7: c in [.N2,N3.] by A1,A2,Th7;
consider F1,I1 such that
A8: len F1 = len I1 and
A9: rng F1 c= commutators(N1,N3) and
A10: b = Product (F1 |^ I1) by A6,Th61;
consider F2,I2 such that
A11: len F2 = len I2 and
A12: rng F2 c= commutators(N2,N3) and
A13: c = Product (F2 |^ I2) by A7,Th61;
A14: len(F1 ^ F2) = len I1 + len I2 by A8,A11,FINSEQ_1:22
.= len(I1 ^ I2) by FINSEQ_1:22;
rng(F1 ^ F2) = rng F1 \/ rng F2 by FINSEQ_1:31;
then
A15: rng(F1 ^ F2) c= commutators(N1,N3) \/ commutators(N2,N3) by A9,A12,
XBOOLE_1:13;
N1 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then commutators(N1,N3) c= commutators(N1 "\/" N2,N3) by A3,Th56;
then
commutators(N1,N3) \/ commutators(N2,N3) c= commutators(N1 "\/" N2,N3
) by A4,XBOOLE_1:8;
then
A16: rng(F1 ^ F2) c= commutators(N1 "\/" N2,N3) by A15;
Product((F1 ^ F2) |^ (I1 ^ I2)) = Product((F1 |^ I1) ^ (F2 |^ I2)) by A8
,A11,GROUP_4:19
.= a by A5,A10,A13,GROUP_4:5;
hence a in [.N1 "\/" N2,N3.] by A16,A14,Th61;
end;
then
A17: [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.N1 "\/" N2,N3.] by GROUP_2:58;
commutators(N1 "\/" N2,N3) c= [.N1,N3.] * [.N2,N3.]
proof
let x be object;
assume x in commutators(N1 "\/" N2,N3);
then consider a,b such that
A18: x = [.a,b.] and
A19: a in N1 "\/" N2 and
A20: b in N3 by Th52;
consider c,d such that
A21: a = c * d and
A22: c in N1 and
A23: d in N2 by A19,Th7;
[.c,b.] in [.N1,N3.] by A20,A22,Th65;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;
then
A24: [.c,b.] |^ d in [.N1,N3.] by A1,GROUP_3:def 13;
x = [.c,b.] |^ d * [.d,b.] & [.d,b.] in [.N2,N3.] by A18,A20,A21,A23,Th25
,Th65;
hence thesis by A24,Th4;
end;
then
gr commutators(N1 "\/" N2,N3) is Subgroup of gr ([.N1,N3.] * [.N2,N3.])
by GROUP_4:32;
then [.N1 "\/" N2,N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;
hence thesis by A17,GROUP_2:55;
end;
theorem
for N1,N2,N3 being strict normal Subgroup of G holds [.N1,N2 "\/" N3.]
= [.N1,N2.] "\/" [.N1,N3.]
proof
let N1,N2,N3 be strict normal Subgroup of G;
N2 "\/" N3 is normal Subgroup of G by GROUP_4:54;
hence [.N1,N2 "\/" N3.] = [.N2 "\/" N3,N1.] by Th69
.= [.N2,N1.] "\/" [.N3,N1.] by Th70
.= [.N1,N2.] "\/" [.N3,N1.] by Th69
.= [.N1,N2.] "\/" [.N1,N3.] by Th69;
end;
definition
let G be Group;
func G` -> strict normal Subgroup of G equals
[.(Omega).G,(Omega).G.];
coherence
proof
(Omega).G is normal Subgroup of G by GROUP_3:114;
hence thesis by Th68;
end;
end;
theorem
for G being Group holds G` = gr commutators G;
theorem Th73:
for G being Group holds x in G` iff ex F being FinSequence of
the carrier of G,I st len F = len I & rng F c= commutators G & x = Product(F |^
I)
proof
let G be Group;
thus x in G` implies ex F being FinSequence of the carrier of G,I st len F =
len I & rng F c= commutators G & x = Product(F |^ I)
proof
assume
A1: x in G`;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def 5;
ex F being FinSequence of the carrier of G,I st len F = len I & rng F
c= commutators G & a = Product(F |^ I) by A1,GROUP_4:28;
hence thesis;
end;
given F being FinSequence of the carrier of G,I such that
A2: len F = len I & rng F c= commutators G & x = Product(F |^ I);
thus thesis by A2,GROUP_4:28;
end;
theorem Th74:
for G being strict Group, a,b be Element of G holds [.a,b.] in G `
proof
let G be strict Group, a,b be Element of G;
a in (Omega).G & b in (Omega).G by STRUCT_0:def 5;
hence thesis by Th65;
end;
theorem
for G being strict Group holds G is commutative Group iff G` = (1).G
proof
let G be strict Group;
thus G is commutative Group implies G` = (1).G
proof
assume
A1: G is commutative Group;
now
let a be Element of G;
assume a in G`;
then a in gr {1_G} by A1,Th51;
then a in gr({1_G} \ {1_G}) by GROUP_4:35;
then a in gr {} the carrier of G by XBOOLE_1:37;
hence a in (1).G by GROUP_4:30;
end;
then
A2: G` is Subgroup of (1).G by GROUP_2:58;
(1).G is Subgroup of G` by GROUP_2:65;
hence thesis by A2,GROUP_2:55;
end;
assume
A3: G` = (1).G;
G is commutative
proof
let a,b be Element of G;
[.a,b.] in G` by Th74;
then [.a,b.] = 1_G by A3,Th1;
hence thesis by Th36;
end;
hence thesis;
end;
theorem
for G being Group, H being strict Subgroup of G holds Left_Cosets H is
finite & index H = 2 implies G` is Subgroup of H
proof
let G be Group, H be strict Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: index H = 2;
A3: H is normal Subgroup of G by A1,A2,GROUP_3:128;
now
let a be Element of G;
assume a in G`;
then consider F being FinSequence of the carrier of G,I such that
A4: len F = len I and
A5: rng F c= commutators G and
A6: a = Product(F |^ I) by Th73;
rng F c= carr H
proof
ex B being finite set st B = Left_Cosets H & index H = card B by A1,
GROUP_2:146;
then consider x,y being object such that
x <> y and
A7: Left_Cosets H = {x,y} by A2,CARD_2:60;
x in Left_Cosets H by A7,TARSKI:def 2;
then consider d being Element of G such that
A8: x = d * H by GROUP_2:def 15;
y in Left_Cosets H by A7,TARSKI:def 2;
then consider e being Element of G such that
A9: y = e * H by GROUP_2:def 15;
carr H in Left_Cosets H by GROUP_2:135;
then
Left_Cosets H = {carr H,e * H} or Left_Cosets H = {d * H,carr H} by A7,A8
,A9,TARSKI:def 2;
then consider c being Element of G such that
A10: Left_Cosets H = {carr H,c * H};
let X be object;
assume X in rng F;
then consider a,b being Element of G such that
A11: X = [.a,b.] by A5,Th58;
b in the carrier of G;
then b in union Left_Cosets H by GROUP_2:137;
then
A12: b in carr H \/ c * H by A10,ZFMISC_1:75;
a in the carrier of G;
then a in union Left_Cosets H by GROUP_2:137;
then
A13: a in carr H \/ c * H by A10,ZFMISC_1:75;
now
per cases by A13,A12,XBOOLE_0:def 3;
suppose
a in carr H & b in carr H;
then a in H & b in H by STRUCT_0:def 5;
then X in H by A11,Th38;
hence thesis by STRUCT_0:def 5;
end;
suppose
a in carr H & b in c * H;
then a in H by STRUCT_0:def 5;
then a |^ b in H & a" in H by A3,Th3,GROUP_2:51;
then a" * (a |^ b) in H by GROUP_2:50;
then X in H by A11,Th16;
hence thesis by STRUCT_0:def 5;
end;
suppose
a in c * H & b in carr H;
then
A14: b in H by STRUCT_0:def 5;
then b" in H by GROUP_2:51;
then b" |^ a in H by A3,Th3;
then b" |^ a * b in H by A14,GROUP_2:50;
hence thesis by A11,STRUCT_0:def 5;
end;
suppose
A15: a in c * H & b in c * H;
then consider d being Element of G such that
A16: a = c * d and
A17: d in H by GROUP_2:103;
consider e being Element of G such that
A18: b = c * e and
A19: e in H by A15,GROUP_2:103;
e" in H by A19,GROUP_2:51;
then
A20: e" |^ c in H by A3,Th3;
d" in H by A17,GROUP_2:51;
then
A21: d" * (e" |^ c) in H by A20,GROUP_2:50;
d |^ c in H by A3,A17,Th3;
then
A22: d |^ c * e in H by A19,GROUP_2:50;
[.a,b.] = (a" * b") * (a * b) by Th16
.= (d" * c" * b") * (c * d * (c * e)) by A16,A18,GROUP_1:17
.= (d" * c" * (e" * c")) * (c * d * (c * e)) by A18,GROUP_1:17
.= (d" * c" * e" * c") * (c * d * (c * e)) by GROUP_1:def 3
.= (d" * c" * e" * c") * (c * (d * (c * e))) by GROUP_1:def 3
.= ((d" * c" * e") * c") * c * (d * (c * e)) by GROUP_1:def 3
.= (d" * c" * e") * (c" * c) * (d * (c * e)) by GROUP_1:def 3
.= (d" * c" * e") * (1_G) * (d * (c * e)) by GROUP_1:def 5
.= (d" * c" * e") * (c * c") * (d * (c * e)) by GROUP_1:def 5
.= (d" * c" * e") * c * c" * (d * (c * e)) by GROUP_1:def 3
.= (d" * (c" * e")) * c * c" * (d * (c * e)) by GROUP_1:def 3
.= d" * (e" |^ c) * c" * (d * (c * e)) by GROUP_1:def 3
.= d" * (e" |^ c) * c" * (d * c * e) by GROUP_1:def 3
.= d" * (e" |^ c) * (c" * (d * c * e)) by GROUP_1:def 3
.= d" * (e" |^ c) * (c" * (d * (c * e))) by GROUP_1:def 3
.= d" * (e" |^ c) * (c" * d * (c * e)) by GROUP_1:def 3
.= d" * (e" |^ c) * (d |^ c * e) by GROUP_1:def 3;
then X in H by A11,A21,A22,GROUP_2:50;
hence thesis by STRUCT_0:def 5;
end;
end;
hence thesis;
end;
then a in gr carr H by A4,A6,GROUP_4:28;
hence a in H by GROUP_4:31;
end;
hence thesis by GROUP_2:58;
end;
begin :: Center of a Group.
definition
let G;
func center G -> strict Subgroup of G means
:Def10:
the carrier of it = {a : for b holds a * b = b * a};
existence
proof
defpred P[Element of G] means for b holds $1 * b = b * $1;
reconsider A = {a : P[a]} as Subset of G from DOMAIN_1:sch 7;
A1: now
let a,b;
assume that
A2: a in A and
A3: b in A;
consider c such that
A4: c = a and
A5: for b holds c * b = b * c by A2;
consider d such that
A6: d = b and
A7: for a holds d * a = a * d by A3;
now
let e;
thus a * b * e = a * (b * e) by GROUP_1:def 3
.= a * (e * d) by A6,A7
.= a * e * b by A6,GROUP_1:def 3
.= e * c * b by A4,A5
.= e * (a * b) by A4,GROUP_1:def 3;
end;
hence a * b in A;
end;
A8: now
let a;
assume a in A;
then consider b such that
A9: b = a and
A10: for c holds b * c = c * b;
now
let c;
thus a" * c = (a" * c)"" .= (c" * a"")" by GROUP_1:17
.= (c" * b)" by A9
.= (b * c")" by A10
.= (a"" * c")" by A9
.= (c * a")"" by GROUP_1:17
.= c * a";
end;
hence a" in A;
end;
now
let b;
1_G * b = b by GROUP_1:def 4;
hence 1_G * b = b * 1_G by GROUP_1:def 4;
end;
then 1_G in A;
hence thesis by A1,A8,GROUP_2:52;
end;
uniqueness by GROUP_2:59;
end;
theorem Th77:
a in center G iff for b holds a * b = b * a
proof
thus a in center G implies for b holds a * b = b * a
proof
assume a in center G;
then a in the carrier of center G by STRUCT_0:def 5;
then a in {b : for c holds b * c = c * b} by Def10;
then ex b st a = b & for c holds b * c = c * b;
hence thesis;
end;
assume for b holds a * b = b * a;
then a in {c : for b holds c * b = b * c};
then a in the carrier of center G by Def10;
hence thesis by STRUCT_0:def 5;
end;
theorem
center G is normal Subgroup of G
proof
now
let a;
thus a * center G c= center G * a
proof
let x be object;
assume x in a * center G;
then consider b such that
A1: x = a * b and
A2: b in center G by GROUP_2:103;
x = b * a by A1,A2,Th77;
hence thesis by A2,GROUP_2:104;
end;
end;
hence thesis by GROUP_3:118;
end;
theorem
for H being Subgroup of G holds H is Subgroup of center G implies H is
normal Subgroup of G
proof
let H be Subgroup of G;
assume
A1: H is Subgroup of center G;
now
let a;
thus H * a c= a * H
proof
let x be object;
assume x in H * a;
then consider b such that
A2: x = b * a and
A3: b in H by GROUP_2:104;
b in center G by A1,A3,GROUP_2:40;
then x = a * b by A2,Th77;
hence thesis by A3,GROUP_2:103;
end;
end;
hence thesis by GROUP_3:119;
end;
theorem
center G is commutative
proof
let a,b be Element of center G;
reconsider x = a, y = b as Element of G by GROUP_2:42;
A1: a in center G by STRUCT_0:def 5;
thus a * b = x * y by GROUP_2:43
.= y * x by A1,Th77
.= b * a by GROUP_2:43;
end;
theorem
a in center G iff con_class a = {a}
proof
thus a in center G implies con_class a = {a}
proof
assume
A1: a in center G;
thus con_class a c= {a}
proof
let x be object;
assume x in con_class a;
then consider b such that
A2: b = x and
A3: a,b are_conjugated by GROUP_3:80;
consider c such that
A4: a = b |^ c by A3;
a = c" * (b * c) by A4,GROUP_1:def 3;
then c * a = b * c by GROUP_1:13;
then a * c = b * c by A1,Th77;
then a = b by GROUP_1:6;
hence thesis by A2,TARSKI:def 1;
end;
a in con_class a by GROUP_3:83;
hence thesis by ZFMISC_1:31;
end;
assume
A5: con_class a = {a};
now
let b;
a |^ b in con_class a by GROUP_3:82;
then a |^ b = a by A5,TARSKI:def 1;
then b" * (a * b) = a by GROUP_1:def 3;
hence a * b = b * a by GROUP_1:13;
end;
hence thesis by Th77;
end;
theorem
for G being strict Group holds G is commutative Group iff center G = G
proof
let G be strict Group;
thus G is commutative Group implies center G = G
proof
assume
A1: G is commutative Group;
now
let a be Element of G;
for b being Element of G holds a * b = b * a by A1,Lm1;
hence a in center G by Th77;
end;
hence thesis by GROUP_2:62;
end;
assume
A2: center G = G;
G is commutative
by STRUCT_0:def 5,A2,Th77;
hence thesis;
end;