:: by Wojciech A. Trybulec

::

:: Received May 15, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

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

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

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 ) )

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 ) )

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 ) )

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 ) )

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;

definition

let G be Group;

let F be FinSequence of the carrier of G;

let a be Element of G;

ex b_{1} being FinSequence of the carrier of G st

( len b_{1} = len F & ( for k being Nat st k in dom F holds

b_{1} . k = (F /. k) |^ a ) )

uniqueness

for b_{1}, b_{2} being FinSequence of the carrier of G st len b_{1} = len F & ( for k being Nat st k in dom F holds

b_{1} . k = (F /. k) |^ a ) & len b_{2} = len F & ( for k being Nat st k in dom F holds

b_{2} . k = (F /. k) |^ a ) holds

b_{1} = b_{2};

end;
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 ( len it = len F & ( for k being Nat st k in dom F holds

it . k = (F /. k) |^ a ) );

ex b

( len b

b

proof end;

correctness uniqueness

for b

b

b

b

proof 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 b_{4} being FinSequence of the carrier of G holds

( b_{4} = F |^ a iff ( len b_{4} = len F & ( for k being Nat st k in dom F holds

b_{4} . k = (F /. k) |^ a ) ) );

for G being Group

for F being FinSequence of the carrier of G

for a being Element of G

for b

( b

b

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

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 :: 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)*>

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

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

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;

correctness

coherence

(((a ") * (b ")) * a) * b is Element of G;

;

end;
let a, b be Element of G;

correctness

coherence

(((a ") * (b ")) * a) * b is Element of G;

;

:: deftheorem defines [. GROUP_5:def 2 :

for G being Group

for a, b being Element of G holds [.a,b.] = (((a ") * (b ")) * a) * b;

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) )

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 :: GROUP_5:18

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)

for a, b being Element of G holds [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)

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) ") )

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: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)

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)

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)

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)

for G being Group

for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)

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 )

( 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

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
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.];

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 )

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:44

for G being Group

for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]

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.]

for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]

proof end;

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

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;

{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G

end;
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 ) } ;

{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G

proof 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 ) } ;

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 :: 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)) = {} )

for A being Subset of G holds

( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )

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)

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)} )

( 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;

correctness

coherence

commutators ((carr H1),(carr H2)) is Subset of G;

;

end;
let H1, H2 be Subgroup of G;

correctness

coherence

commutators ((carr H1),(carr H2)) is Subset of G;

;

:: 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));

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 ) )

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 :: 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)} )

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 )

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)

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)} )

( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )

proof end;

definition
end;

:: deftheorem defines commutators GROUP_5:def 6 :

for G being Group holds commutators G = commutators (((Omega). G),((Omega). G));

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.] )

for G being Group holds

( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )

proof end;

definition

let G be Group;

let A, B be Subset of G;

correctness

coherence

gr (commutators (A,B)) is strict Subgroup of G;

;

end;
let A, B be Subset of G;

correctness

coherence

gr (commutators (A,B)) is strict Subgroup of G;

;

:: deftheorem defines [. GROUP_5:def 7 :

for G being Group

for A, B being Subset of G holds [.A,B.] = gr (commutators (A,B));

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.]

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) ) )

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

definition

let G be Group;

let H1, H2 be Subgroup of G;

correctness

coherence

[.(carr H1),(carr H2).] is strict Subgroup of G;

;

end;
let H1, H2 be Subgroup of G;

correctness

coherence

[.(carr H1),(carr H2).] is strict Subgroup of G;

;

:: deftheorem defines [. GROUP_5:def 8 :

for G being Group

for H1, H2 being Subgroup of G holds [.H1,H2.] = [.(carr H1),(carr H2).];

for G being Group

for H1, H2 being Subgroup of G holds [.H1,H2.] = [.(carr H1),(carr H2).];

theorem :: GROUP_5:63

theorem :: GROUP_5:64

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.]

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.]

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 )

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

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 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.]

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.]

for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]

proof end;

definition
end;

:: deftheorem defines ` GROUP_5:def 9 :

for G being Group holds G ` = [.((Omega). G),((Omega). G).];

for G being Group holds G ` = [.((Omega). G),((Omega). 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) ) )

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 :: 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

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;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { a where a is Element of G : for b being Element of G holds a * b = b * a }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { a where a is Element of G : for b being Element of G holds a * b = b * a } & the carrier of b_{2} = { a where a is Element of G : for b being Element of G holds a * b = b * a } holds

b_{1} = b_{2}
by GROUP_2:59;

end;
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 the carrier of it = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines center GROUP_5:def 10 :

for G being Group

for b_{2} being strict Subgroup of G holds

( b_{2} = center G iff the carrier of b_{2} = { a where a is Element of G : for b being Element of G holds a * b = b * a } );

for G being Group

for b

( b

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 )

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: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

for H being Subgroup of G st H is Subgroup of center G holds

H is normal Subgroup of G

proof end;

:: P. Hall Identity.

::