:: Commutator and Center of a Group
:: by Wojciech A. Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem Th1: :: GROUP_5:1
for x being set
for G being Group holds
( x in (1). G iff x = 1_ G )
proof end;

theorem :: GROUP_5:2
for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
a |^ b in H
proof end;

theorem Th3: :: GROUP_5:3
for G being Group
for a, b being Element of G
for N being strict normal Subgroup of G st a in N holds
a |^ b in N
proof end;

theorem Th4: :: GROUP_5:4
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof end;

theorem Th5: :: GROUP_5:5
for x being set
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof end;

theorem :: GROUP_5:6
for x being set
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof end;

theorem Th7: :: GROUP_5:7
for x being set
for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
proof end;

theorem :: GROUP_5:8
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds H * N = N * H
proof end;

definition
let G be Group;
let F be FinSequence of the carrier of G;
let a be Element of G;
func F |^ a -> FinSequence of the carrier of G means :Def1: :: GROUP_5:def 1
( len it = len F & ( for k being Nat st k in dom F holds
it . k = (F /. k) |^ a ) );
existence
ex b1 being FinSequence of the carrier of G st
( len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ a ) )
proof end;
correctness
uniqueness
for b1, b2 being FinSequence of the carrier of G st len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ a ) & len b2 = len F & ( for k being Nat st k in dom F holds
b2 . k = (F /. k) |^ a ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def1 defines |^ GROUP_5:def 1 :
for G being Group
for F being FinSequence of the carrier of G
for a being Element of G
for b4 being FinSequence of the carrier of G holds
( b4 = F |^ a iff ( len b4 = len F & ( for k being Nat st k in dom F holds
b4 . k = (F /. k) |^ a ) ) );

theorem Th9: :: GROUP_5:9
for G being Group
for a being Element of G
for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
proof end;

theorem Th10: :: GROUP_5:10
for G being Group
for a being Element of G holds (<*> the carrier of G) |^ a = {}
proof end;

theorem Th11: :: GROUP_5:11
for G being Group
for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>
proof end;

theorem Th12: :: GROUP_5:12
for G being Group
for a, b, c being Element of G holds <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
proof end;

theorem :: GROUP_5:13
for G being Group
for a, b, c, d being Element of G holds <*a,b,c*> |^ d = <*(a |^ d),(b |^ d),(c |^ d)*>
proof end;

theorem Th14: :: GROUP_5:14
for G being Group
for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
proof end;

theorem Th15: :: GROUP_5:15
for G being Group
for a being Element of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
proof end;

begin

definition
let G be Group;
let a, b be Element of G;
func [.a,b.] -> Element of G equals :: GROUP_5:def 2
(((a ") * (b ")) * a) * b;
correctness
coherence
(((a ") * (b ")) * a) * b is Element of G;
;
end;

:: deftheorem defines [. GROUP_5:def 2 :
for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") * (b ")) * a) * b;

theorem Th16: :: GROUP_5:16
for G being Group
for a, b being Element of G holds
( [.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 end;

theorem Th17: :: GROUP_5:17
for G being Group
for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)
proof end;

theorem :: GROUP_5:18
for G being Group
for a, b being Element of G holds
( [.a,b.] = ((b ") |^ a) * b & [.a,b.] = (a ") * (a |^ b) ) by Th16;

theorem Th19: :: GROUP_5:19
for G being Group
for a being Element of G holds
( [.(1_ G),a.] = 1_ G & [.a,(1_ G).] = 1_ G )
proof end;

theorem Th20: :: GROUP_5:20
for G being Group
for a being Element of G holds [.a,a.] = 1_ G
proof end;

theorem :: GROUP_5:21
for G being Group
for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
proof end;

theorem Th22: :: GROUP_5:22
for G being Group
for a, b being Element of G holds [.a,b.] " = [.b,a.]
proof end;

theorem Th23: :: GROUP_5:23
for G being Group
for a, b, c being Element of G holds [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
proof end;

theorem :: GROUP_5:24
for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)
proof end;

theorem Th25: :: GROUP_5:25
for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] |^ b) * [.b,c.]
proof end;

theorem :: GROUP_5:26
for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
proof end;

theorem Th27: :: GROUP_5:27
for G being Group
for a, b being Element of G holds [.(a "),b.] = [.b,a.] |^ (a ")
proof end;

theorem Th28: :: GROUP_5:28
for G being Group
for a, b being Element of G holds [.a,(b ").] = [.b,a.] |^ (b ")
proof end;

theorem :: GROUP_5:29
for G being Group
for a, b being Element of G holds
( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
proof end;

theorem :: GROUP_5:30
for G being Group
for a, b being Element of G holds [.a,(b |^ (a ")).] = [.b,(a ").]
proof end;

theorem :: GROUP_5:31
for G being Group
for a, b being Element of G holds [.(a |^ (b ")),b.] = [.(b "),a.]
proof end;

theorem :: GROUP_5:32
for n being Element of NAT
for G being Group
for a, b being Element of G holds [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)
proof end;

theorem :: GROUP_5:33
for n being Element of NAT
for G being Group
for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)
proof end;

theorem :: GROUP_5:34
for i being Integer
for G being Group
for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)
proof end;

theorem :: GROUP_5:35
for i being Integer
for G being Group
for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
proof end;

theorem Th36: :: GROUP_5:36
for G being Group
for a, b being Element of G holds
( [.a,b.] = 1_ G iff a * b = b * a )
proof end;

Lm1: for G being commutative Group
for a, b being Element of G holds a * b = b * a
;

theorem :: GROUP_5:37
for G being Group holds
( G is commutative Group iff for a, b being Element of G holds [.a,b.] = 1_ G )
proof end;

theorem Th38: :: GROUP_5:38
for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
[.a,b.] in H
proof end;

definition
let G be Group;
let a, b, c be Element of G;
func [.a,b,c.] -> Element of G equals :: GROUP_5:def 3
[.[.a,b.],c.];
correctness
coherence
[.[.a,b.],c.] is Element of G;
;
end;

:: deftheorem defines [. GROUP_5:def 3 :
for G being Group
for a, b, c being Element of G holds [.a,b,c.] = [.[.a,b.],c.];

theorem :: GROUP_5:39
for G being Group
for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
proof end;

theorem :: GROUP_5:40
for G being Group
for a, b being Element of G holds [.a,a,b.] = 1_ G
proof end;

theorem :: GROUP_5:41
for G being Group
for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]
proof end;

theorem :: GROUP_5:42
for G being Group
for b, a being Element of G holds [.b,a,a.] = ([.b,(a ").] * [.b,a.]) |^ a
proof end;

theorem :: GROUP_5:43
for G being Group
for a, b being Element of G holds [.a,b,(b |^ a).] = [.b,[.b,a.].]
proof end;

theorem :: GROUP_5:44
for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]
proof end;

theorem :: GROUP_5:45
for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
proof end;

::
:: P. Hall Identity.
::
theorem :: GROUP_5:46
for G being Group
for a, b, c being Element of G holds (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
proof end;

definition
let G be Group;
let A, B be Subset of G;
func commutators (A,B) -> Subset of G equals :: GROUP_5:def 4
 { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;
coherence
{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G
proof end;
end;

:: deftheorem defines commutators GROUP_5:def 4 :
for G being Group
for A, B being Subset of G holds commutators (A,B) = { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;

theorem Th47: :: GROUP_5:47
for x being set
for G being Group
for A, B being Subset of G holds
( x in commutators (A,B) iff ex a, b being Element of G st
( x = [.a,b.] & a in A & b in B ) ) ;

theorem :: GROUP_5:48
for G being Group
for A being Subset of G holds
( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )
proof end;

theorem :: GROUP_5:49
for G being Group
for a, b being Element of G holds commutators ({a},{b}) = {[.a,b.]}
proof end;

theorem Th50: :: GROUP_5:50
for G being Group
for A, B, C, D being Subset of G st A c= B & C c= D holds
commutators (A,C) c= commutators (B,D)
proof end;

theorem Th51: :: GROUP_5:51
for G being Group holds
( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} )
proof end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
func commutators (H1,H2) -> Subset of G equals :: GROUP_5:def 5
 commutators ((carr H1),(carr H2));
correctness
coherence
commutators ((carr H1),(carr H2)) is Subset of G;
;
end;

:: deftheorem defines commutators GROUP_5:def 5 :
for G being Group
for H1, H2 being Subgroup of G holds commutators (H1,H2) = commutators ((carr H1),(carr H2));

theorem Th52: :: GROUP_5:52
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )
proof end;

theorem Th53: :: GROUP_5:53
for G being Group
for H1, H2 being Subgroup of G holds 1_ G in commutators (H1,H2)
proof end;

theorem :: GROUP_5:54
for G being Group
for H being Subgroup of G holds
( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )
proof end;

theorem Th55: :: GROUP_5:55
for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
proof end;

theorem Th56: :: GROUP_5:56
for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
commutators (H1,H3) c= commutators (H2,H4)
proof end;

theorem Th57: :: GROUP_5:57
for G being Group holds
( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )
proof end;

definition
let G be Group;
func commutators G -> Subset of G equals :: GROUP_5:def 6
 commutators (((Omega). G),((Omega). G));
correctness
coherence
commutators (((Omega). G),((Omega). G)) is Subset of G;
;
end;

:: deftheorem defines commutators GROUP_5:def 6 :
for G being Group holds commutators G = commutators (((Omega). G),((Omega). G));

theorem Th58: :: GROUP_5:58
for x being set
for G being Group holds
( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
proof end;

theorem :: GROUP_5:59
for G being Group holds
( G is commutative Group iff commutators G = {(1_ G)} )
proof end;

definition
let G be Group;
let A, B be Subset of G;
func [.A,B.] -> strict Subgroup of G equals :: GROUP_5:def 7
 gr (commutators (A,B));
correctness
coherence
gr (commutators (A,B)) is strict Subgroup of G;
;
end;

:: deftheorem defines [. GROUP_5:def 7 :
for G being Group
for A, B being Subset of G holds [.A,B.] = gr (commutators (A,B));

theorem Th60: :: GROUP_5:60
for G being Group
for a, b being Element of G
for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
proof end;

theorem Th61: :: GROUP_5:61
for x being set
for G being Group
for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )
proof end;

theorem :: GROUP_5:62
for G being Group
for A, C, B, D being Subset of G st A c= C & B c= D holds
[.A,B.] is Subgroup of [.C,D.] by Th50, GROUP_4:32;

definition
let G be Group;
let H1, H2 be Subgroup of G;
func [.H1,H2.] -> strict Subgroup of G equals :: GROUP_5:def 8
[.(carr H1),(carr H2).];
correctness
coherence
[.(carr H1),(carr H2).] is strict Subgroup of G;
;
end;

:: deftheorem defines [. GROUP_5:def 8 :
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = [.(carr H1),(carr H2).];

theorem :: GROUP_5:63
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = gr (commutators (H1,H2)) ;

theorem :: GROUP_5:64
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in [.H1,H2.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (H1,H2) & x = Product (F |^ I) ) ) by Th61;

theorem Th65: :: GROUP_5:65
for G being Group
for a, b being Element of G
for H1, H2 being Subgroup of G st a in H1 & b in H2 holds
[.a,b.] in [.H1,H2.]
proof end;

theorem :: GROUP_5:66
for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
[.H1,H3.] is Subgroup of [.H2,H4.]
proof end;

theorem :: GROUP_5:67
for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
proof end;

theorem Th68: :: GROUP_5:68
for G being Group
for N1, N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G
proof end;

Lm2: for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
proof end;

theorem Th69: :: GROUP_5:69
for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]
proof end;

theorem Th70: :: GROUP_5:70
for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
proof end;

theorem :: GROUP_5:71
for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
proof end;

definition
let G be Group;
func G ` -> strict normal Subgroup of G equals :: GROUP_5:def 9
[.((Omega). G),((Omega). G).];
coherence
[.((Omega). G),((Omega). G).] is strict normal Subgroup of G
proof end;
end;

:: deftheorem defines ` GROUP_5:def 9 :
for G being Group holds G ` = [.((Omega). G),((Omega). G).];

theorem :: GROUP_5:72
for G being Group holds G ` = gr (commutators G) ;

theorem Th73: :: GROUP_5:73
for x being set
for G being Group holds
( x in G ` iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) )
proof end;

theorem Th74: :: GROUP_5:74
for G being strict Group
for a, b being Element of G holds [.a,b.] in G `
proof end;

theorem :: GROUP_5:75
for G being strict Group holds
( G is commutative Group iff G ` = (1). G )
proof end;

theorem :: GROUP_5:76
for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 2 holds
G ` is Subgroup of H
proof end;

begin

definition
let G be Group;
func center G -> strict Subgroup of G means :Def10: :: GROUP_5:def 10
 the carrier of it = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a } & the carrier of b2 = { a where a is Element of G : for b being Element of G holds a * b = b * a } holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def10 defines center GROUP_5:def 10 :
for G being Group
for b2 being strict Subgroup of G holds
( b2 = center G iff the carrier of b2 = { a where a is Element of G : for b being Element of G holds a * b = b * a } );

theorem Th77: :: GROUP_5:77
for G being Group
for a being Element of G holds
( a in center G iff for b being Element of G holds a * b = b * a )
proof end;

theorem :: GROUP_5:78
for G being Group holds center G is normal Subgroup of G
proof end;

theorem :: GROUP_5:79
for G being Group
for H being Subgroup of G st H is Subgroup of center G holds
H is normal Subgroup of G
proof end;

theorem :: GROUP_5:80
for G being Group holds center G is commutative
proof end;

theorem :: GROUP_5:81
for G being Group
for a being Element of G holds
( a in center G iff con_class a = {a} )
proof end;

theorem :: GROUP_5:82
for G being strict Group holds
( G is commutative Group iff center G = G )
proof end;