:: GROUP_5 semantic presentation

scheme :: GROUP_5:sch 1
SubsetFD3{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set , set ) -> Element of F₂(), P₁[ set , set , set ] } :

{ F₄(c,d,e) where c is Element of F₁(), d is Element of F₂(), e is Element of F₃() : P₁[c,d,e] } is Subset of F₂()

proof end;

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

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines |^ GROUP_5:def 1 :

theorem :: GROUP_5:9

canceled;

theorem :: GROUP_5:10

canceled;

theorem :: GROUP_5:11

canceled;

theorem Th12: :: GROUP_5:12

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 Th13: :: GROUP_5:13

for G being Group
for a being Element of G holds (<*> the carrier of G) |^ a = {}

proof end;

theorem Th14: :: GROUP_5:14

for G being Group
for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>

proof end;

theorem Th15: :: GROUP_5:15

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

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 Th17: :: GROUP_5:17

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

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;

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 ;

end;

:: deftheorem defines [. GROUP_5:def 2 :

theorem Th19: :: GROUP_5:19

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 Th20: :: GROUP_5:20

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

proof end;

theorem Th21: :: GROUP_5:21

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

proof end;

theorem Th22: :: GROUP_5:22

for G being Group
for a being Element of G holds
( [.(1. G),a.] = 1. G & [.a,(1. G).] = 1. G )

proof end;

theorem Th23: :: GROUP_5:23

for G being Group
for a being Element of G holds [.a,a.] = 1. G

proof end;

theorem :: GROUP_5:24

for G being Group
for a being Element of G holds
( [.a,(a " ).] = 1. G & [.(a " ),a.] = 1. G )

proof end;

theorem Th25: :: GROUP_5:25

for G being Group
for a, b being Element of G holds [.a,b.] " = [.b,a.]

proof end;

theorem Th26: :: GROUP_5:26

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

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

proof end;

theorem Th28: :: GROUP_5:28

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

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

proof end;

theorem Th30: :: GROUP_5:30

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

proof end;

theorem Th31: :: GROUP_5:31

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

proof end;

theorem :: GROUP_5:32

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

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

proof end;

theorem :: GROUP_5:34

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

proof end;

theorem :: GROUP_5:35

for n being 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:36

for n being 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:37

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

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 Th39: :: GROUP_5:39

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

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 Th41: :: GROUP_5:41

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 ;

end;

:: deftheorem defines [. GROUP_5:def 3 :

theorem :: GROUP_5:42

canceled;

theorem :: GROUP_5:43

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

for G being Group
for a, b being Element of G holds [.a,a,b.] = 1. G

proof end;

theorem :: GROUP_5:45

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

proof end;

theorem :: GROUP_5:46

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

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

proof end;

theorem :: GROUP_5:48

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

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;

theorem :: GROUP_5:50

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

proof end;

end;

:: deftheorem defines commutators GROUP_5:def 4 :

theorem :: GROUP_5:51

canceled;

theorem Th52: :: GROUP_5:52

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

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

for G being Group
for a, b being Element of G holds commutators {a},{b} = {[.a,b.]}

proof end;

theorem Th55: :: GROUP_5:55

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 Th56: :: GROUP_5:56

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 ;

end;

:: deftheorem defines commutators GROUP_5:def 5 :

theorem :: GROUP_5:57

canceled;

theorem Th58: :: GROUP_5:58

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 Th59: :: GROUP_5:59

for G being Group
for H1, H2 being Subgroup of G holds 1. G in commutators H1,H2

proof end;

theorem :: GROUP_5:60

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 Th61: :: GROUP_5:61

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 Th62: :: GROUP_5:62

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 Th63: :: GROUP_5:63

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 ;

end;

:: deftheorem defines commutators GROUP_5:def 6 :

theorem :: GROUP_5:64

canceled;

theorem Th65: :: GROUP_5:65

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

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 ;

end;

:: deftheorem defines [. GROUP_5:def 7 :

theorem :: GROUP_5:67

canceled;

theorem Th68: :: GROUP_5:68

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 Th69: :: GROUP_5:69

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

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

proof end;

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 ;

end;

:: deftheorem defines [. GROUP_5:def 8 :

theorem :: GROUP_5:71

canceled;

theorem :: GROUP_5:72

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

theorem Th73: :: GROUP_5:73

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

theorem Th74: :: GROUP_5:74

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

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

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 Th77: :: GROUP_5:77

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 Th78: :: GROUP_5:78

for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]

proof end;

theorem Th79: :: GROUP_5:79

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

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

proof end;

end;

:: deftheorem defines ` GROUP_5:def 9 :

theorem :: GROUP_5:81

canceled;

theorem :: GROUP_5:82

for G being Group holds G ` = gr (commutators G) ;

theorem Th83: :: GROUP_5:83

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 Th84: :: GROUP_5:84

for G being strict Group
for a, b being Element of G holds [.a,b.] in G `

proof end;

theorem :: GROUP_5:85

for G being strict Group holds
( G is commutative Group iff G ` = (1). G )

proof end;

theorem :: GROUP_5:86

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;

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

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def10 defines center GROUP_5:def 10 :

theorem :: GROUP_5:87

canceled;

theorem :: GROUP_5:88

canceled;

theorem Th89: :: GROUP_5:89

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

for G being Group holds center G is normal Subgroup of G

proof end;

theorem :: GROUP_5:91

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

for G being Group holds center G is commutative

proof end;

theorem :: GROUP_5:93

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

for G being strict Group holds
( G is commutative Group iff center G = G )

proof end;