:: by Wojciech A. Trybulec

::

:: Received August 10, 1990

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

begin

theorem Th1: :: GROUP_3:1

for G being Group

for a, b being Element of G holds

( (a * b) * (b ") = a & (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )

for a, b being Element of G holds

( (a * b) * (b ") = a & (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )

proof end;

Lm1: for A being commutative Group

for a, b being Element of A holds a * b = b * a

;

theorem :: GROUP_3:5

theorem Th6: :: GROUP_3:6

for G being Group

for a being Element of G

for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds

( a * H1 c= a * H2 & H1 * a c= H2 * a )

for a being Element of G

for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds

( a * H1 c= a * H2 & H1 * a c= H2 * a )

proof end;

theorem :: GROUP_3:7

theorem :: GROUP_3:8

theorem Th9: :: GROUP_3:9

for G being Group

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (A * a) * H = A * (a * H)

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (A * a) * H = A * (a * H)

proof end;

theorem :: GROUP_3:10

for G being Group

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (a * H) * A = a * (H * A)

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (a * H) * A = a * (H * A)

proof end;

theorem :: GROUP_3:11

for G being Group

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (A * H) * a = A * (H * a)

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (A * H) * a = A * (H * a)

proof end;

theorem :: GROUP_3:12

for G being Group

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (H * a) * A = H * (a * A)

for a being Element of G

for A being Subset of G

for H being Subgroup of G holds (H * a) * A = H * (a * A)

proof end;

theorem :: GROUP_3:13

definition

let G be Group;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is strict Subgroup of G )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is strict Subgroup of G ) ) & ( for x being set holds

( x in b_{2} iff x is strict Subgroup of G ) ) holds

b_{1} = b_{2}

end;
func Subgroups G -> set means :Def1: :: GROUP_3:def 1

for x being set holds

( x in it iff x is strict Subgroup of G );

existence for x being set holds

( x in it iff x is strict Subgroup of G );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :

for G being Group

for b_{2} being set holds

( b_{2} = Subgroups G iff for x being set holds

( x in b_{2} iff x is strict Subgroup of G ) );

for G being Group

for b

( b

( x in b

registration
end;

definition
end;

:: deftheorem defines |^ GROUP_3:def 2 :

for G being Group

for a, b being Element of G holds a |^ b = ((b ") * a) * b;

for G being Group

for a, b being Element of G holds a |^ b = ((b ") * a) * b;

theorem :: GROUP_3:21

theorem Th25: :: GROUP_3:25

for G being Group

for a, b being Element of G holds

( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )

for a, b being Element of G holds

( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )

proof end;

Lm2: now :: thesis: for G being Group

for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0

for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0

let G be Group; :: thesis: for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0

let a, b be Element of G; :: thesis: (a |^ 0) |^ b = (a |^ b) |^ 0

thus (a |^ 0) |^ b = (1_ G) |^ b by GROUP_1:25

.= 1_ G by Th17

.= (a |^ b) |^ 0 by GROUP_1:25 ; :: thesis: verum

end;
let a, b be Element of G; :: thesis: (a |^ 0) |^ b = (a |^ b) |^ 0

thus (a |^ 0) |^ b = (1_ G) |^ b by GROUP_1:25

.= 1_ G by Th17

.= (a |^ b) |^ 0 by GROUP_1:25 ; :: thesis: verum

Lm3: now :: thesis: for n being Nat st ( for G being Group

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) holds

for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) holds

for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let n be Nat; :: thesis: ( ( for G being Group

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) implies for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) )

assume A1: for G being Group

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; :: thesis: for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let G be Group; :: thesis: for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let a, b be Element of G; :: thesis: (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:34

.= ((a |^ n) |^ b) * (a |^ b) by Th23

.= ((a |^ b) |^ n) * (a |^ b) by A1

.= (a |^ b) |^ (n + 1) by GROUP_1:34 ; :: thesis: verum

end;
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) implies for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) )

assume A1: for G being Group

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; :: thesis: for G being Group

for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let G be Group; :: thesis: for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let a, b be Element of G; :: thesis: (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:34

.= ((a |^ n) |^ b) * (a |^ b) by Th23

.= ((a |^ b) |^ n) * (a |^ b) by A1

.= (a |^ b) |^ (n + 1) by GROUP_1:34 ; :: thesis: verum

Lm4: for n being Nat

for G being Group

for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n

proof end;

theorem :: GROUP_3:27

theorem :: GROUP_3:28

for G being Group

for a, b being Element of G

for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i

for a, b being Element of G

for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i

proof end;

definition

let G be Group;

let A, B be Subset of G;

{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G

end;
let A, B be Subset of G;

func A |^ B -> Subset of G equals :: GROUP_3:def 3

{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

coherence { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G

proof end;

:: deftheorem defines |^ GROUP_3:def 3 :

for G being Group

for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

for G being Group

for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

theorem :: GROUP_3:40

for G being Group

for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}

for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}

proof end;

definition

let G be Group;

let A be Subset of G;

let g be Element of G;

correctness

coherence

A |^ {g} is Subset of G;

;

correctness

coherence

{g} |^ A is Subset of G;

;

end;
let A be Subset of G;

let g be Element of G;

correctness

coherence

A |^ {g} is Subset of G;

;

correctness

coherence

{g} |^ A is Subset of G;

;

:: deftheorem defines |^ GROUP_3:def 4 :

for G being Group

for A being Subset of G

for g being Element of G holds A |^ g = A |^ {g};

for G being Group

for A being Subset of G

for g being Element of G holds A |^ g = A |^ {g};

:: deftheorem defines |^ GROUP_3:def 5 :

for G being Group

for A being Subset of G

for g being Element of G holds g |^ A = {g} |^ A;

for G being Group

for A being Subset of G

for g being Element of G holds g |^ A = {g} |^ A;

theorem Th41: :: GROUP_3:41

for x being set

for G being Group

for g being Element of G

for A being Subset of G holds

( x in A |^ g iff ex h being Element of G st

( x = h |^ g & h in A ) )

for G being Group

for g being Element of G

for A being Subset of G holds

( x in A |^ g iff ex h being Element of G st

( x = h |^ g & h in A ) )

proof end;

theorem Th42: :: GROUP_3:42

for x being set

for G being Group

for g being Element of G

for A being Subset of G holds

( x in g |^ A iff ex h being Element of G st

( x = g |^ h & h in A ) )

for G being Group

for g being Element of G

for A being Subset of G holds

( x in g |^ A iff ex h being Element of G st

( x = g |^ h & h in A ) )

proof end;

theorem :: GROUP_3:44

theorem :: GROUP_3:45

theorem :: GROUP_3:46

theorem Th47: :: GROUP_3:47

for G being Group

for a, b being Element of G

for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)

for a, b being Element of G

for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)

proof end;

theorem :: GROUP_3:48

theorem :: GROUP_3:49

for G being Group

for a, b being Element of G

for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)

for a, b being Element of G

for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)

proof end;

theorem :: GROUP_3:51

theorem Th54: :: GROUP_3:54

for G being Group

for a being Element of G

for A being Subset of G holds

( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )

for a being Element of G

for A being Subset of G holds

( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )

proof end;

theorem Th55: :: GROUP_3:55

for G being Group holds

( G is commutative Group iff for A, B being Subset of G st B <> {} holds

A |^ B = A )

( G is commutative Group iff for A, B being Subset of G st B <> {} holds

A |^ B = A )

proof end;

theorem :: GROUP_3:56

for G being Group holds

( G is commutative Group iff for A being Subset of G

for g being Element of G holds A |^ g = A )

( G is commutative Group iff for A being Subset of G

for g being Element of G holds A |^ g = A )

proof end;

theorem :: GROUP_3:57

for G being Group holds

( G is commutative Group iff for A being Subset of G

for g being Element of G st A <> {} holds

g |^ A = {g} )

( G is commutative Group iff for A being Subset of G

for g being Element of G st A <> {} holds

g |^ A = {g} )

proof end;

definition

let G be Group;

let H be Subgroup of G;

let a be Element of G;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = (carr H) |^ a

uniqueness

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = (carr H) |^ a & the carrier of b_{2} = (carr H) |^ a holds

b_{1} = b_{2};

by GROUP_2:59;

end;
let H be Subgroup of G;

let a be Element of G;

func H |^ a -> strict Subgroup of G means :Def6: :: GROUP_3:def 6

the carrier of it = (carr H) |^ a;

existence the carrier of it = (carr H) |^ a;

ex b

proof end;

correctness uniqueness

for b

b

by GROUP_2:59;

:: deftheorem Def6 defines |^ GROUP_3:def 6 :

for G being Group

for H being Subgroup of G

for a being Element of G

for b_{4} being strict Subgroup of G holds

( b_{4} = H |^ a iff the carrier of b_{4} = (carr H) |^ a );

for G being Group

for H being Subgroup of G

for a being Element of G

for b

( b

theorem Th58: :: GROUP_3:58

for x being set

for G being Group

for a being Element of G

for H being Subgroup of G holds

( x in H |^ a iff ex g being Element of G st

( x = g |^ a & g in H ) )

for G being Group

for a being Element of G

for H being Subgroup of G holds

( x in H |^ a iff ex g being Element of G st

( x = g |^ a & g in H ) )

proof end;

theorem Th59: :: GROUP_3:59

for G being Group

for a being Element of G

for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a

for a being Element of G

for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a

proof end;

theorem Th60: :: GROUP_3:60

for G being Group

for a, b being Element of G

for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)

for a, b being Element of G

for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)

proof end;

theorem Th62: :: GROUP_3:62

for G being Group

for a being Element of G

for H being strict Subgroup of G holds

( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )

for a being Element of G

for H being strict Subgroup of G holds

( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )

proof end;

theorem Th63: :: GROUP_3:63

for G being Group

for a being Element of G

for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)

for a being Element of G

for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)

proof end;

theorem Th65: :: GROUP_3:65

for G being Group

for a being Element of G

for H being Subgroup of G holds

( H is finite iff H |^ a is finite )

for a being Element of G

for H being Subgroup of G holds

( H is finite iff H |^ a is finite )

proof end;

registration

let G be Group;

let a be Element of G;

let H be finite Subgroup of G;

coherence

H |^ a is finite by Th65;

end;
let a be Element of G;

let H be finite Subgroup of G;

coherence

H |^ a is finite by Th65;

theorem :: GROUP_3:66

theorem :: GROUP_3:68

for G being Group

for a being Element of G

for H being strict Subgroup of G st H |^ a = (1). G holds

H = (1). G

for a being Element of G

for H being strict Subgroup of G st H |^ a = (1). G holds

H = (1). G

proof end;

theorem :: GROUP_3:70

for G being Group

for a being Element of G

for H being strict Subgroup of G st H |^ a = G holds

H = G

for a being Element of G

for H being strict Subgroup of G st H |^ a = G holds

H = G

proof end;

theorem :: GROUP_3:72

for G being Group

for a being Element of G

for H being Subgroup of G st Left_Cosets H is finite holds

index H = index (H |^ a)

for a being Element of G

for H being Subgroup of G st Left_Cosets H is finite holds

index H = index (H |^ a)

proof end;

theorem Th73: :: GROUP_3:73

for G being Group st G is commutative Group holds

for H being strict Subgroup of G

for a being Element of G holds H |^ a = H

for H being strict Subgroup of G

for a being Element of G holds H |^ a = H

proof end;

:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :

for G being Group

for a, b being Element of G holds

( a,b are_conjugated iff ex g being Element of G st a = b |^ g );

for G being Group

for a, b being Element of G holds

( a,b are_conjugated iff ex g being Element of G st a = b |^ g );

notation
end;

theorem Th74: :: GROUP_3:74

for G being Group

for a, b being Element of G holds

( a,b are_conjugated iff ex g being Element of G st b = a |^ g )

for a, b being Element of G holds

( a,b are_conjugated iff ex g being Element of G st b = a |^ g )

proof end;

definition

let G be Group;

let a, b be Element of G;

:: original: are_conjugated

redefine pred a,b are_conjugated ;

reflexivity

for a being Element of G holds (G,b_{1},b_{1})
by Th75;

symmetry

for a, b being Element of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by Th76;

end;
let a, b be Element of G;

:: original: are_conjugated

redefine pred a,b are_conjugated ;

reflexivity

for a being Element of G holds (G,b

symmetry

for a, b being Element of G st (G,b

(G,b

theorem Th77: :: GROUP_3:77

for G being Group

for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds

a,c are_conjugated

for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds

a,c are_conjugated

proof end;

theorem Th78: :: GROUP_3:78

for G being Group

for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds

a = 1_ G

for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds

a = 1_ G

proof end;

theorem Th79: :: GROUP_3:79

for G being Group

for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }

for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }

proof end;

definition

let G be Group;

let a be Element of G;

correctness

coherence

a |^ (carr ((Omega). G)) is Subset of G;

;

end;
let a be Element of G;

correctness

coherence

a |^ (carr ((Omega). G)) is Subset of G;

;

:: deftheorem defines con_class GROUP_3:def 8 :

for G being Group

for a being Element of G holds con_class a = a |^ (carr ((Omega). G));

for G being Group

for a being Element of G holds con_class a = a |^ (carr ((Omega). G));

theorem Th80: :: GROUP_3:80

for x being set

for G being Group

for a being Element of G holds

( x in con_class a iff ex b being Element of G st

( b = x & a,b are_conjugated ) )

for G being Group

for a being Element of G holds

( x in con_class a iff ex b being Element of G st

( b = x & a,b are_conjugated ) )

proof end;

theorem :: GROUP_3:85

for G being Group

for a, b being Element of G holds

( con_class a = con_class b iff con_class a meets con_class b )

for a, b being Element of G holds

( con_class a = con_class b iff con_class a meets con_class b )

proof end;

theorem :: GROUP_3:87

for G being Group

for a being Element of G

for A being Subset of G holds (con_class a) * A = A * (con_class a)

for a being Element of G

for A being Subset of G holds (con_class a) * A = A * (con_class a)

proof end;

:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :

for G being Group

for A, B being Subset of G holds

( A,B are_conjugated iff ex g being Element of G st A = B |^ g );

for G being Group

for A, B being Subset of G holds

( A,B are_conjugated iff ex g being Element of G st A = B |^ g );

notation
end;

theorem Th88: :: GROUP_3:88

for G being Group

for A, B being Subset of G holds

( A,B are_conjugated iff ex g being Element of G st B = A |^ g )

for A, B being Subset of G holds

( A,B are_conjugated iff ex g being Element of G st B = A |^ g )

proof end;

definition

let G be Group;

let A, B be Subset of G;

:: original: are_conjugated

redefine pred A,B are_conjugated ;

reflexivity

for A being Subset of G holds (G,b_{1},b_{1})
by Th89;

symmetry

for A, B being Subset of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by Th90;

end;
let A, B be Subset of G;

:: original: are_conjugated

redefine pred A,B are_conjugated ;

reflexivity

for A being Subset of G holds (G,b

symmetry

for A, B being Subset of G st (G,b

(G,b

theorem Th91: :: GROUP_3:91

for G being Group

for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds

A,C are_conjugated

for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds

A,C are_conjugated

proof end;

theorem Th92: :: GROUP_3:92

for G being Group

for a, b being Element of G holds

( {a},{b} are_conjugated iff a,b are_conjugated )

for a, b being Element of G holds

( {a},{b} are_conjugated iff a,b are_conjugated )

proof end;

theorem Th93: :: GROUP_3:93

for G being Group

for A being Subset of G

for H1 being Subgroup of G st A, carr H1 are_conjugated holds

ex H2 being strict Subgroup of G st the carrier of H2 = A

for A being Subset of G

for H1 being Subgroup of G st A, carr H1 are_conjugated holds

ex H2 being strict Subgroup of G st the carrier of H2 = A

proof end;

definition

let G be Group;

let A be Subset of G;

{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G

end;
let A be Subset of G;

func con_class A -> Subset-Family of G equals :: GROUP_3:def 10

{ B where B is Subset of G : A,B are_conjugated } ;

coherence { B where B is Subset of G : A,B are_conjugated } ;

{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G

proof end;

:: deftheorem defines con_class GROUP_3:def 10 :

for G being Group

for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;

for G being Group

for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;

theorem :: GROUP_3:94

theorem :: GROUP_3:99

for G being Group

for A, B being Subset of G holds

( con_class A = con_class B iff con_class A meets con_class B )

for A, B being Subset of G holds

( con_class A = con_class B iff con_class A meets con_class B )

proof end;

theorem Th100: :: GROUP_3:100

for G being Group

for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }

for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }

proof end;

theorem :: GROUP_3:101

definition

let G be Group;

let H1, H2 be Subgroup of G;

end;
let H1, H2 be Subgroup of G;

pred H1,H2 are_conjugated means :Def11: :: GROUP_3:def 11

ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g;

ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g;

:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :

for G being Group

for H1, H2 being Subgroup of G holds

( H1,H2 are_conjugated iff ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g );

for G being Group

for H1, H2 being Subgroup of G holds

( H1,H2 are_conjugated iff ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g );

notation

let G be Group;

let H1, H2 be Subgroup of G;

antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;

end;
let H1, H2 be Subgroup of G;

antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;

theorem Th102: :: GROUP_3:102

for G being Group

for H1, H2 being strict Subgroup of G holds

( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )

for H1, H2 being strict Subgroup of G holds

( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )

proof end;

theorem Th104: :: GROUP_3:104

for G being Group

for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds

H2,H1 are_conjugated

for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds

H2,H1 are_conjugated

proof end;

definition

let G be Group;

let H1, H2 be strict Subgroup of G;

:: original: are_conjugated

redefine pred H1,H2 are_conjugated ;

reflexivity

for H1 being strict Subgroup of G holds (G,b_{1},b_{1})
by Th103;

symmetry

for H1, H2 being strict Subgroup of G st (G,b_{1},b_{2}) holds

(G,b_{2},b_{1})
by Th104;

end;
let H1, H2 be strict Subgroup of G;

:: original: are_conjugated

redefine pred H1,H2 are_conjugated ;

reflexivity

for H1 being strict Subgroup of G holds (G,b

symmetry

for H1, H2 being strict Subgroup of G st (G,b

(G,b

theorem Th105: :: GROUP_3:105

for G being Group

for H3 being Subgroup of G

for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds

H1,H3 are_conjugated

for H3 being Subgroup of G

for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds

H1,H3 are_conjugated

proof end;

definition

let G be Group;

let H be Subgroup of G;

ex b_{1} being Subset of (Subgroups G) st

for x being set holds

( x in b_{1} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) )

for b_{1}, b_{2} being Subset of (Subgroups G) st ( for x being set holds

( x in b_{1} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds

( x in b_{2} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) ) holds

b_{1} = b_{2}

end;
let H be Subgroup of G;

func con_class H -> Subset of (Subgroups G) means :Def12: :: GROUP_3:def 12

for x being set holds

( x in it iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) );

existence for x being set holds

( x in it iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) );

ex b

for x being set holds

( x in b

( x = H1 & H,H1 are_conjugated ) )

proof end;

uniqueness for b

( x in b

( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds

( x in b

( x = H1 & H,H1 are_conjugated ) ) ) holds

b

proof end;

:: deftheorem Def12 defines con_class GROUP_3:def 12 :

for G being Group

for H being Subgroup of G

for b_{3} being Subset of (Subgroups G) holds

( b_{3} = con_class H iff for x being set holds

( x in b_{3} iff ex H1 being strict Subgroup of G st

( x = H1 & H,H1 are_conjugated ) ) );

for G being Group

for H being Subgroup of G

for b

( b

( x in b

( x = H1 & H,H1 are_conjugated ) ) );

theorem Th106: :: GROUP_3:106

for x being set

for G being Group

for H being Subgroup of G st x in con_class H holds

x is strict Subgroup of G

for G being Group

for H being Subgroup of G st x in con_class H holds

x is strict Subgroup of G

proof end;

theorem Th107: :: GROUP_3:107

for G being Group

for H1, H2 being strict Subgroup of G holds

( H1 in con_class H2 iff H1,H2 are_conjugated )

for H1, H2 being strict Subgroup of G holds

( H1 in con_class H2 iff H1,H2 are_conjugated )

proof end;

theorem Th108: :: GROUP_3:108

for G being Group

for g being Element of G

for H being strict Subgroup of G holds H |^ g in con_class H

for g being Element of G

for H being strict Subgroup of G holds H |^ g in con_class H

proof end;

theorem :: GROUP_3:110

for G being Group

for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds

H2 in con_class H1

for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds

H2 in con_class H1

proof end;

theorem :: GROUP_3:111

for G being Group

for H1, H2 being strict Subgroup of G holds

( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )

for H1, H2 being strict Subgroup of G holds

( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )

proof end;

theorem :: GROUP_3:112

theorem Th113: :: GROUP_3:113

for G being Group

for H2 being Subgroup of G

for H1 being strict Subgroup of G holds

( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )

for H2 being Subgroup of G

for H1 being strict Subgroup of G holds

( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )

proof end;

:: deftheorem Def13 defines normal GROUP_3:def 13 :

for G being Group

for IT being Subgroup of G holds

( IT is normal iff for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #) );

for G being Group

for IT being Subgroup of G holds

( IT is normal iff for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #) );

registration

let G be Group;

existence

ex b_{1} being Subgroup of G st

( b_{1} is strict & b_{1} is normal )

end;
existence

ex b

( b

proof end;

theorem Th117: :: GROUP_3:117

for G being Group

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )

proof end;

theorem Th118: :: GROUP_3:118

for G being Group

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a )

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a )

proof end;

theorem Th119: :: GROUP_3:119

for G being Group

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )

for H being Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )

proof end;

theorem :: GROUP_3:120

for G being Group

for H being Subgroup of G holds

( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )

for H being Subgroup of G holds

( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )

proof end;

theorem :: GROUP_3:121

for G being Group

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )

proof end;

theorem :: GROUP_3:122

for G being Group

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H )

proof end;

theorem :: GROUP_3:123

for G being Group

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff con_class H = {H} )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff con_class H = {H} )

proof end;

theorem :: GROUP_3:124

for G being Group

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G st a in H holds

con_class a c= carr H )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff for a being Element of G st a in H holds

con_class a c= carr H )

proof end;

Lm5: for G being Group

for N2 being normal Subgroup of G

for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)

proof end;

theorem Th125: :: GROUP_3:125

for G being Group

for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)

for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)

proof end;

theorem :: GROUP_3:126

for G being Group

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)

proof end;

theorem :: GROUP_3:128

for G being Group

for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds

H is normal Subgroup of G

for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds

H is normal Subgroup of G

proof end;

definition

let G be Group;

let A be Subset of G;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { h where h is Element of G : A |^ h = A }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { h where h is Element of G : A |^ h = A } & the carrier of b_{2} = { h where h is Element of G : A |^ h = A } holds

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

end;
let A be Subset of G;

func Normalizer A -> strict Subgroup of G means :Def14: :: GROUP_3:def 14

the carrier of it = { h where h is Element of G : A |^ h = A } ;

existence the carrier of it = { h where h is Element of G : A |^ h = A } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def14 defines Normalizer GROUP_3:def 14 :

for G being Group

for A being Subset of G

for b_{3} being strict Subgroup of G holds

( b_{3} = Normalizer A iff the carrier of b_{3} = { h where h is Element of G : A |^ h = A } );

for G being Group

for A being Subset of G

for b

( b

theorem Th129: :: GROUP_3:129

for x being set

for G being Group

for A being Subset of G holds

( x in Normalizer A iff ex h being Element of G st

( x = h & A |^ h = A ) )

for G being Group

for A being Subset of G holds

( x in Normalizer A iff ex h being Element of G st

( x = h & A |^ h = A ) )

proof end;

theorem :: GROUP_3:131

for G being Group

for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds

ex C being finite set st

( C = con_class A & card C = index (Normalizer A) )

for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds

ex C being finite set st

( C = con_class A & card C = index (Normalizer A) )

proof end;

theorem :: GROUP_3:133

for G being Group

for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds

ex C being finite set st

( C = con_class a & card C = index (Normalizer {a}) )

for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds

ex C being finite set st

( C = con_class a & card C = index (Normalizer {a}) )

proof end;

definition

let G be Group;

let H be Subgroup of G;

correctness

coherence

Normalizer (carr H) is strict Subgroup of G;

;

end;
let H be Subgroup of G;

correctness

coherence

Normalizer (carr H) is strict Subgroup of G;

;

:: deftheorem defines Normalizer GROUP_3:def 15 :

for G being Group

for H being Subgroup of G holds Normalizer H = Normalizer (carr H);

for G being Group

for H being Subgroup of G holds Normalizer H = Normalizer (carr H);

theorem Th134: :: GROUP_3:134

for x being set

for G being Group

for H being strict Subgroup of G holds

( x in Normalizer H iff ex h being Element of G st

( x = h & H |^ h = H ) )

for G being Group

for H being strict Subgroup of G holds

( x in Normalizer H iff ex h being Element of G st

( x = h & H |^ h = H ) )

proof end;

theorem :: GROUP_3:136

for G being Group

for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds

ex C being finite set st

( C = con_class H & card C = index (Normalizer H) )

for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds

ex C being finite set st

( C = con_class H & card C = index (Normalizer H) )

proof end;

theorem Th137: :: GROUP_3:137

for G being strict Group

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff Normalizer H = G )

for H being strict Subgroup of G holds

( H is normal Subgroup of G iff Normalizer H = G )

proof end;