:: by Wojciech A. Trybulec

::

:: Received July 23, 1990

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

begin

Lm1: for x being set

for G being non empty 1-sorted

for A being Subset of G st x in A holds

x is Element of G

;

theorem :: GROUP_2:1

definition

let G be Group;

let A be Subset of G;

coherence

{ (g ") where g is Element of G : g in A } is Subset of G

for b_{1}, b_{2} being Subset of G st b_{1} = { (g ") where g is Element of G : g in b_{2} } holds

b_{2} = { (g ") where g is Element of G : g in b_{1} }

end;
let A be Subset of G;

coherence

{ (g ") where g is Element of G : g in A } is Subset of G

proof end;

involutiveness for b

b

proof end;

:: deftheorem defines " GROUP_2:def 1 :

for G being Group

for A being Subset of G holds A " = { (g ") where g is Element of G : g in A } ;

for G being Group

for A being Subset of G holds A " = { (g ") where g is Element of G : g in A } ;

registration
end;

definition

let G be non empty multMagma ;

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_2:def 2

{ (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_2:def 2 :

for G being non empty multMagma

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 non empty multMagma

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

definition

let G be non empty commutative multMagma ;

let A, B be Subset of G;

:: original: *

redefine func A * B -> Subset of G;

commutativity

for A, B being Subset of G holds A * B = B * A

end;
let A, B be Subset of G;

:: original: *

redefine func A * B -> Subset of G;

commutativity

for A, B being Subset of G holds A * B = B * A

proof end;

theorem Th9: :: GROUP_2:9

for G being non empty multMagma

for A, B being Subset of G holds

( ( A <> {} & B <> {} ) iff A * B <> {} )

for A, B being Subset of G holds

( ( A <> {} & B <> {} ) iff A * B <> {} )

proof end;

theorem Th10: :: GROUP_2:10

for G being non empty multMagma

for A, B, C being Subset of G st G is associative holds

(A * B) * C = A * (B * C)

for A, B, C being Subset of G st G is associative holds

(A * B) * C = A * (B * C)

proof end;

theorem :: GROUP_2:12

for G being non empty multMagma

for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C)

for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C)

proof end;

theorem :: GROUP_2:13

for G being non empty multMagma

for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)

for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)

proof end;

theorem :: GROUP_2:14

for G being non empty multMagma

for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C)

for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C)

proof end;

theorem :: GROUP_2:15

for G being non empty multMagma

for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)

for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)

proof end;

theorem Th16: :: GROUP_2:16

for G being non empty multMagma

for A being Subset of G holds

( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

for A being Subset of G holds

( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

proof end;

theorem Th17: :: GROUP_2:17

for G being Group

for A being Subset of G st A <> {} holds

( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )

for A being Subset of G st A <> {} holds

( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )

proof end;

theorem :: GROUP_2:19

for G being non empty multMagma

for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}

for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}

proof end;

theorem :: GROUP_2:20

for G being non empty multMagma

for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}

for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}

proof end;

theorem :: GROUP_2:21

for G being non empty multMagma

for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}

for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}

proof end;

theorem Th22: :: GROUP_2:22

for G being Group

for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) holds

A * A = A

for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) holds

A * A = A

proof end;

theorem Th23: :: GROUP_2:23

for G being Group

for A being Subset of G st ( for g being Element of G st g in A holds

g " in A ) holds

A " = A

for A being Subset of G st ( for g being Element of G st g in A holds

g " in A ) holds

A " = A

proof end;

theorem :: GROUP_2:24

for G being non empty multMagma

for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds

a * b = b * a ) holds

A * B = B * A

for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds

a * b = b * a ) holds

A * B = B * A

proof end;

Lm2: for A being commutative Group

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

;

theorem Th25: :: GROUP_2:25

for G being non empty multMagma

for A, B being Subset of G st G is commutative Group holds

A * B = B * A

for A, B being Subset of G st G is commutative Group holds

A * B = B * A

proof end;

definition

let G be non empty multMagma ;

let g be Element of G;

let A be Subset of G;

correctness

coherence

{g} * A is Subset of G;

;

correctness

coherence

A * {g} is Subset of G;

;

end;
let g be Element of G;

let A be Subset of G;

correctness

coherence

{g} * A is Subset of G;

;

correctness

coherence

A * {g} is Subset of G;

;

:: deftheorem defines * GROUP_2:def 3 :

for G being non empty multMagma

for g being Element of G

for A being Subset of G holds g * A = {g} * A;

for G being non empty multMagma

for g being Element of G

for A being Subset of G holds g * A = {g} * A;

:: deftheorem defines * GROUP_2:def 4 :

for G being non empty multMagma

for g being Element of G

for A being Subset of G holds A * g = A * {g};

for G being non empty multMagma

for g being Element of G

for A being Subset of G holds A * g = A * {g};

theorem Th27: :: GROUP_2:27

for x being set

for G being non empty multMagma

for A being Subset of G

for g being Element of G holds

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

( x = g * h & h in A ) )

for G being non empty multMagma

for A being Subset of G

for g being Element of G holds

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

( x = g * h & h in A ) )

proof end;

theorem Th28: :: GROUP_2:28

for x being set

for G being non empty multMagma

for A being Subset of G

for g being Element of G holds

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

( x = h * g & h in A ) )

for G being non empty multMagma

for A being Subset of G

for g being Element of G holds

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

( x = h * g & h in A ) )

proof end;

theorem :: GROUP_2:29

theorem :: GROUP_2:30

theorem :: GROUP_2:31

theorem Th32: :: GROUP_2:32

for G being non empty multMagma

for A being Subset of G

for g, h being Element of G st G is associative holds

(g * h) * A = g * (h * A)

for A being Subset of G

for g, h being Element of G st G is associative holds

(g * h) * A = g * (h * A)

proof end;

theorem :: GROUP_2:33

theorem Th34: :: GROUP_2:34

for G being non empty multMagma

for A being Subset of G

for g, h being Element of G st G is associative holds

(A * g) * h = A * (g * h)

for A being Subset of G

for g, h being Element of G st G is associative holds

(A * g) * h = A * (g * h)

proof end;

theorem :: GROUP_2:35

theorem :: GROUP_2:36

theorem Th37: :: GROUP_2:37

for G being non empty Group-like multMagma

for A being Subset of G holds

( (1_ G) * A = A & A * (1_ G) = A )

for A being Subset of G holds

( (1_ G) * A = A & A * (1_ G) = A )

proof end;

theorem :: GROUP_2:38

definition

let G be non empty Group-like multMagma ;

ex b_{1} being non empty Group-like multMagma st

( the carrier of b_{1} c= the carrier of G & the multF of b_{1} = the multF of G || the carrier of b_{1} )

end;
mode Subgroup of G -> non empty Group-like multMagma means :Def5: :: GROUP_2:def 5

( the carrier of it c= the carrier of G & the multF of it = the multF of G || the carrier of it );

existence ( the carrier of it c= the carrier of G & the multF of it = the multF of G || the carrier of it );

ex b

( the carrier of b

proof end;

:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :

for G, b_{2} being non empty Group-like multMagma holds

( b_{2} is Subgroup of G iff ( the carrier of b_{2} c= the carrier of G & the multF of b_{2} = the multF of G || the carrier of b_{2} ) );

for G, b

( b

theorem Th39: :: GROUP_2:39

for G being non empty Group-like multMagma

for H being Subgroup of G st G is finite holds

H is finite

for H being Subgroup of G st G is finite holds

H is finite

proof end;

theorem Th40: :: GROUP_2:40

for x being set

for G being non empty Group-like multMagma

for H being Subgroup of G st x in H holds

x in G

for G being non empty Group-like multMagma

for H being Subgroup of G st x in H holds

x in G

proof end;

theorem Th41: :: GROUP_2:41

for G being non empty Group-like multMagma

for H being Subgroup of G

for h being Element of H holds h in G

for H being Subgroup of G

for h being Element of H holds h in G

proof end;

theorem Th42: :: GROUP_2:42

for G being non empty Group-like multMagma

for H being Subgroup of G

for h being Element of H holds h is Element of G

for H being Subgroup of G

for h being Element of H holds h is Element of G

proof end;

theorem Th43: :: GROUP_2:43

for G being non empty Group-like multMagma

for g1, g2 being Element of G

for H being Subgroup of G

for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds

h1 * h2 = g1 * g2

for g1, g2 being Element of G

for H being Subgroup of G

for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds

h1 * h2 = g1 * g2

proof end;

registration
end;

theorem Th48: :: GROUP_2:48

for G being Group

for g being Element of G

for H being Subgroup of G

for h being Element of H st h = g holds

h " = g "

for g being Element of G

for H being Subgroup of G

for h being Element of H st h = g holds

h " = g "

proof end;

theorem Th50: :: GROUP_2:50

for G being Group

for g1, g2 being Element of G

for H being Subgroup of G st g1 in H & g2 in H holds

g1 * g2 in H

for g1, g2 being Element of G

for H being Subgroup of G st g1 in H & g2 in H holds

g1 * g2 in H

proof end;

registration
end;

theorem Th52: :: GROUP_2:52

for G being Group

for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) holds

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

for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) holds

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

proof end;

registration

let G be commutative Group;

coherence

for b_{1} being Subgroup of G holds b_{1} is commutative
by Th53;

end;
coherence

for b

theorem Th55: :: GROUP_2:55

for G1, G2 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds

multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)

multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)

proof end;

theorem Th56: :: GROUP_2:56

for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds

G1 is Subgroup of G3

G1 is Subgroup of G3

proof end;

theorem Th57: :: GROUP_2:57

for G being Group

for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is Subgroup of H2

for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is Subgroup of H2

proof end;

theorem Th58: :: GROUP_2:58

for G being Group

for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is Subgroup of H2

for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds

g in H2 ) holds

H1 is Subgroup of H2

proof end;

theorem Th59: :: GROUP_2:59

for G being Group

for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

proof end;

theorem Th60: :: GROUP_2:60

for G being Group

for H1, H2 being Subgroup of G st ( for g being Element of G holds

( g in H1 iff g in H2 ) ) holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

for H1, H2 being Subgroup of G st ( for g being Element of G holds

( g in H1 iff g in H2 ) ) holds

multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)

proof end;

definition

let G be Group;

let H1, H2 be strict Subgroup of G;

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) ) by Th60;

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

:: original: =

redefine pred H1 = H2 means :: GROUP_2:def 6

for g being Element of G holds

( g in H1 iff g in H2 );

compatibility redefine pred H1 = H2 means :: GROUP_2:def 6

for g being Element of G holds

( g in H1 iff g in H2 );

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) ) by Th60;

:: deftheorem defines = GROUP_2:def 6 :

for G being Group

for H1, H2 being strict Subgroup of G holds

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) );

for G being Group

for H1, H2 being strict Subgroup of G holds

( H1 = H2 iff for g being Element of G holds

( g in H1 iff g in H2 ) );

theorem Th61: :: GROUP_2:61

for G being Group

for H being Subgroup of G st the carrier of G c= the carrier of H holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

for H being Subgroup of G st the carrier of G c= the carrier of H holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

proof end;

theorem Th62: :: GROUP_2:62

for G being Group

for H being Subgroup of G st ( for g being Element of G holds g in H ) holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

for H being Subgroup of G st ( for g being Element of G holds g in H ) holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

proof end;

definition

let G be Group;

existence

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = {(1_ G)}

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = {(1_ G)} & the carrier of b_{2} = {(1_ G)} holds

b_{1} = b_{2}
by Th59;

end;
existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines (1). GROUP_2:def 7 :

for G being Group

for b_{2} being strict Subgroup of G holds

( b_{2} = (1). G iff the carrier of b_{2} = {(1_ G)} );

for G being Group

for b

( b

definition

let G be Group;

multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G

for b_{1} being strict Subgroup of G

for b_{2} being Group st b_{1} = multMagma(# the carrier of b_{2}, the multF of b_{2} #) holds

b_{1} = multMagma(# the carrier of b_{1}, the multF of b_{1} #)
;

end;
func (Omega). G -> strict Subgroup of G equals :: GROUP_2:def 8

multMagma(# the carrier of G, the multF of G #);

coherence multMagma(# the carrier of G, the multF of G #);

multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G

proof end;

projectivity for b

for b

b

:: deftheorem defines (Omega). GROUP_2:def 8 :

for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #);

for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #);

theorem :: GROUP_2:66

registration

let G be Group;

coherence

(1). G is finite by Th68;

existence

ex b_{1} being Subgroup of G st

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

end;
coherence

(1). G is finite by Th68;

existence

ex b

( b

proof end;

registration
end;

registration
end;

theorem :: GROUP_2:73

for G being finite Group

for H being Subgroup of G st card G = card H holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

for H being Subgroup of G st card G = card H holds

multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

proof end;

definition
end;

:: deftheorem defines carr GROUP_2:def 9 :

for G being Group

for H being Subgroup of G holds carr H = the carrier of H;

for G being Group

for H being Subgroup of G holds carr H = the carrier of H;

theorem Th74: :: GROUP_2:74

for G being Group

for g1, g2 being Element of G

for H being Subgroup of G st g1 in carr H & g2 in carr H holds

g1 * g2 in carr H

for g1, g2 being Element of G

for H being Subgroup of G st g1 in carr H & g2 in carr H holds

g1 * g2 in carr H

proof end;

theorem Th75: :: GROUP_2:75

for G being Group

for g being Element of G

for H being Subgroup of G st g in carr H holds

g " in carr H

for g being Element of G

for H being Subgroup of G st g in carr H holds

g " in carr H

proof end;

theorem Th78: :: GROUP_2:78

for G being Group

for H1, H2 being Subgroup of G holds

( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

for H1, H2 being Subgroup of G holds

( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

proof end;

theorem :: GROUP_2:79

for G being Group

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

ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

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

ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

proof end;

definition

let G be Group;

let H1, H2 be Subgroup of G;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2)

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2) & the carrier of b_{2} = (carr H1) /\ (carr H2) holds

b_{1} = b_{2}
by Th59;

end;
let H1, H2 be Subgroup of G;

func H1 /\ H2 -> strict Subgroup of G means :Def10: :: GROUP_2:def 10

the carrier of it = (carr H1) /\ (carr H2);

existence the carrier of it = (carr H1) /\ (carr H2);

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines /\ GROUP_2:def 10 :

for G being Group

for H1, H2 being Subgroup of G

for b_{4} being strict Subgroup of G holds

( b_{4} = H1 /\ H2 iff the carrier of b_{4} = (carr H1) /\ (carr H2) );

for G being Group

for H1, H2 being Subgroup of G

for b

( b

theorem Th80: :: GROUP_2:80

for G being Group

for H1, H2 being Subgroup of G holds

( ( for H being Subgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

for H1, H2 being Subgroup of G holds

( ( for H being Subgroup of G st H = H1 /\ H2 holds

the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds

H = H1 /\ H2 ) )

proof end;

theorem :: GROUP_2:81

theorem Th82: :: GROUP_2:82

for x being set

for G being Group

for H1, H2 being Subgroup of G holds

( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )

for G being Group

for H1, H2 being Subgroup of G holds

( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )

proof end;

definition

let G be Group;

let H1, H2 be Subgroup of G;

:: original: /\

redefine func H1 /\ H2 -> strict Subgroup of G;

commutativity

for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1

end;
let H1, H2 be Subgroup of G;

:: original: /\

redefine func H1 /\ H2 -> strict Subgroup of G;

commutativity

for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1

proof end;

Lm3: for G being Group

for H2, H1 being Subgroup of G holds

( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

proof end;

theorem :: GROUP_2:85

for G being Group

for H being Subgroup of G holds

( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )

for H being Subgroup of G holds

( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )

proof end;

theorem :: GROUP_2:86

Lm4: for G being Group

for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1

proof end;

theorem :: GROUP_2:88

theorem :: GROUP_2:89

theorem :: GROUP_2:90

for G being Group

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

H1 /\ H3 is Subgroup of H2

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

H1 /\ H3 is Subgroup of H2

proof end;

theorem :: GROUP_2:91

for G being Group

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

H1 is Subgroup of H2 /\ H3

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

H1 is Subgroup of H2 /\ H3

proof end;

theorem :: GROUP_2:92

for G being Group

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

H1 /\ H3 is Subgroup of H2 /\ H3

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

H1 /\ H3 is Subgroup of H2 /\ H3

proof end;

theorem :: GROUP_2:93

for G being Group

for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds

H1 /\ H2 is finite

for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds

H1 /\ H2 is finite

proof end;

definition

let G be Group;

let H be Subgroup of G;

let A be Subset of G;

correctness

coherence

A * (carr H) is Subset of G;

;

correctness

coherence

(carr H) * A is Subset of G;

;

end;
let H be Subgroup of G;

let A be Subset of G;

correctness

coherence

A * (carr H) is Subset of G;

;

correctness

coherence

(carr H) * A is Subset of G;

;

:: deftheorem defines * GROUP_2:def 11 :

for G being Group

for H being Subgroup of G

for A being Subset of G holds A * H = A * (carr H);

for G being Group

for H being Subgroup of G

for A being Subset of G holds A * H = A * (carr H);

:: deftheorem defines * GROUP_2:def 12 :

for G being Group

for H being Subgroup of G

for A being Subset of G holds H * A = (carr H) * A;

for G being Group

for H being Subgroup of G

for A being Subset of G holds H * A = (carr H) * A;

theorem :: GROUP_2:94

for x being set

for G being Group

for A being Subset of G

for H being Subgroup of G holds

( x in A * H iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in A & g2 in H ) )

for G being Group

for A being Subset of G

for H being Subgroup of G holds

( x in A * H iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in A & g2 in H ) )

proof end;

theorem :: GROUP_2:95

for x being set

for G being Group

for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

for G being Group

for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

proof end;

theorem :: GROUP_2:96

theorem :: GROUP_2:97

theorem :: GROUP_2:98

theorem :: GROUP_2:99

theorem :: GROUP_2:100

theorem :: GROUP_2:101

theorem :: GROUP_2:102

definition

let G be Group;

let H be Subgroup of G;

let a be Element of G;

correctness

coherence

a * (carr H) is Subset of G;

;

correctness

coherence

(carr H) * a is Subset of G;

;

end;
let H be Subgroup of G;

let a be Element of G;

correctness

coherence

a * (carr H) is Subset of G;

;

correctness

coherence

(carr H) * a is Subset of G;

;

:: deftheorem defines * GROUP_2:def 13 :

for G being Group

for H being Subgroup of G

for a being Element of G holds a * H = a * (carr H);

for G being Group

for H being Subgroup of G

for a being Element of G holds a * H = a * (carr H);

:: deftheorem defines * GROUP_2:def 14 :

for G being Group

for H being Subgroup of G

for a being Element of G holds H * a = (carr H) * a;

for G being Group

for H being Subgroup of G

for a being Element of G holds H * a = (carr H) * a;

theorem Th103: :: GROUP_2:103

for x being set

for G being Group

for a being Element of G

for H being Subgroup of G holds

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

( x = a * g & g in H ) )

for G being Group

for a being Element of G

for H being Subgroup of G holds

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

( x = a * g & g in H ) )

proof end;

theorem Th104: :: GROUP_2:104

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

theorem :: GROUP_2:106

theorem :: GROUP_2:107

theorem Th108: :: GROUP_2:108

for G being Group

for a being Element of G

for H being Subgroup of G holds

( a in a * H & a in H * a )

for a being Element of G

for H being Subgroup of G holds

( a in a * H & a in H * a )

proof end;

theorem :: GROUP_2:109

theorem Th111: :: GROUP_2:111

for G being Group

for a being Element of G holds

( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )

for a being Element of G holds

( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )

proof end;

theorem :: GROUP_2:112

theorem Th113: :: GROUP_2:113

for G being Group

for a being Element of G

for H being Subgroup of G holds

( a in H iff a * H = carr H )

for a being Element of G

for H being Subgroup of G holds

( a in H iff a * H = carr H )

proof end;

theorem Th114: :: GROUP_2:114

for G being Group

for a, b being Element of G

for H being Subgroup of G holds

( a * H = b * H iff (b ") * a in H )

for a, b being Element of G

for H being Subgroup of G holds

( a * H = b * H iff (b ") * a in H )

proof end;

theorem Th115: :: GROUP_2:115

for G being Group

for a, b being Element of G

for H being Subgroup of G holds

( a * H = b * H iff a * H meets b * H )

for a, b being Element of G

for H being Subgroup of G holds

( a * H = b * H iff a * H meets b * H )

proof end;

theorem Th116: :: GROUP_2:116

for G being Group

for a, b being Element of G

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

for a, b being Element of G

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

proof end;

theorem :: GROUP_2:117

for G being Group

for a being Element of G

for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

for a being Element of G

for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

proof end;

theorem :: GROUP_2:118

for G being Group

for a being Element of G

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

for a being Element of G

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

proof end;

theorem Th119: :: GROUP_2:119

for G being Group

for a being Element of G

for H being Subgroup of G holds

( a in H iff H * a = carr H )

for a being Element of G

for H being Subgroup of G holds

( a in H iff H * a = carr H )

proof end;

theorem Th120: :: GROUP_2:120

for G being Group

for a, b being Element of G

for H being Subgroup of G holds

( H * a = H * b iff b * (a ") in H )

for a, b being Element of G

for H being Subgroup of G holds

( H * a = H * b iff b * (a ") in H )

proof end;

theorem :: GROUP_2:121

for G being Group

for a, b being Element of G

for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

for a, b being Element of G

for H being Subgroup of G holds

( H * a = H * b iff H * a meets H * b )

proof end;

theorem Th122: :: GROUP_2:122

for G being Group

for a, b being Element of G

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

for a, b being Element of G

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

proof end;

theorem :: GROUP_2:123

for G being Group

for a being Element of G

for H being Subgroup of G holds

( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )

for a being Element of G

for H being Subgroup of G holds

( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )

proof end;

theorem :: GROUP_2:124

for G being Group

for a being Element of G

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

for a being Element of G

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

proof end;

theorem :: GROUP_2:125

for G being Group

for a being Element of G

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

for a being Element of G

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

proof end;

theorem :: GROUP_2:126

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

for G being Group

for a being Element of G

for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

for a being Element of G

for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

proof end;

theorem Th128: :: GROUP_2:128

for G being Group

for a, b being Element of G

for H being Subgroup of G holds a * H,b * H are_equipotent

for a, b being Element of G

for H being Subgroup of G holds a * H,b * H are_equipotent

proof end;

theorem Th129: :: GROUP_2:129

for G being Group

for a, b being Element of G

for H being Subgroup of G holds a * H,H * b are_equipotent

for a, b being Element of G

for H being Subgroup of G holds a * H,H * b are_equipotent

proof end;

theorem Th130: :: GROUP_2:130

for G being Group

for a, b being Element of G

for H being Subgroup of G holds H * a,H * b are_equipotent

for a, b being Element of G

for H being Subgroup of G holds H * a,H * b are_equipotent

proof end;

theorem Th131: :: GROUP_2:131

for G being Group

for a being Element of G

for H being Subgroup of G holds

( carr H,a * H are_equipotent & carr H,H * a are_equipotent )

for a being Element of G

for H being Subgroup of G holds

( carr H,a * H are_equipotent & carr H,H * a are_equipotent )

proof end;

theorem :: GROUP_2:132

for G being Group

for a being Element of G

for H being Subgroup of G holds

( card H = card (a * H) & card H = card (H * a) )

for a being Element of G

for H being Subgroup of G holds

( card H = card (a * H) & card H = card (H * a) )

proof end;

theorem Th133: :: GROUP_2:133

for G being Group

for a being Element of G

for H being finite Subgroup of G ex B, C being finite set st

( B = a * H & C = H * a & card H = card B & card H = card C )

for a being Element of G

for H being finite Subgroup of G ex B, C being finite set st

( B = a * H & C = H * a & card H = card B & card H = card C )

proof end;

definition

let G be Group;

let H be Subgroup of G;

ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = a * H )

for b_{1}, b_{2} being Subset-Family of G st ( for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds

( A in b_{2} iff ex a being Element of G st A = a * H ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset-Family of G st

for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = H * a )

for b_{1}, b_{2} being Subset-Family of G st ( for A being Subset of G holds

( A in b_{1} iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds

( A in b_{2} iff ex a being Element of G st A = H * a ) ) holds

b_{1} = b_{2}

end;
let H be Subgroup of G;

func Left_Cosets H -> Subset-Family of G means :Def15: :: GROUP_2:def 15

for A being Subset of G holds

( A in it iff ex a being Element of G st A = a * H );

existence for A being Subset of G holds

( A in it iff ex a being Element of G st A = a * H );

ex b

for A being Subset of G holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

func Right_Cosets H -> Subset-Family of G means :Def16: :: GROUP_2:def 16

for A being Subset of G holds

( A in it iff ex a being Element of G st A = H * a );

existence for A being Subset of G holds

( A in it iff ex a being Element of G st A = H * a );

ex b

for A being Subset of G holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :

for G being Group

for H being Subgroup of G

for b_{3} being Subset-Family of G holds

( b_{3} = Left_Cosets H iff for A being Subset of G holds

( A in b_{3} iff ex a being Element of G st A = a * H ) );

for G being Group

for H being Subgroup of G

for b

( b

( A in b

:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :

for G being Group

for H being Subgroup of G

for b_{3} being Subset-Family of G holds

( b_{3} = Right_Cosets H iff for A being Subset of G holds

( A in b_{3} iff ex a being Element of G st A = H * a ) );

for G being Group

for H being Subgroup of G

for b

( b

( A in b

theorem :: GROUP_2:134

for G being Group

for H being Subgroup of G st G is finite holds

( Right_Cosets H is finite & Left_Cosets H is finite ) ;

for H being Subgroup of G st G is finite holds

( Right_Cosets H is finite & Left_Cosets H is finite ) ;

theorem :: GROUP_2:135

for G being Group

for H being Subgroup of G holds

( carr H in Left_Cosets H & carr H in Right_Cosets H )

for H being Subgroup of G holds

( carr H in Left_Cosets H & carr H in Right_Cosets H )

proof end;

theorem Th137: :: GROUP_2:137

for G being Group

for H being Subgroup of G holds

( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )

for H being Subgroup of G holds

( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )

proof end;

theorem :: GROUP_2:140

for G being Group

for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds

H = (1). G

for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds

H = (1). G

proof end;

theorem :: GROUP_2:141

for G being Group

for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds

H = (1). G

for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds

H = (1). G

proof end;

theorem Th142: :: GROUP_2:142

for G being Group holds

( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )

( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )

proof end;

theorem Th143: :: GROUP_2:143

for G being strict Group

for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds

H = G

for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds

H = G

proof end;

theorem :: GROUP_2:144

for G being strict Group

for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds

H = G

for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds

H = G

proof end;

definition
end;

:: deftheorem defines Index GROUP_2:def 17 :

for G being Group

for H being Subgroup of G holds Index H = card (Left_Cosets H);

for G being Group

for H being Subgroup of G holds Index H = card (Left_Cosets H);

theorem :: GROUP_2:145

for G being Group

for H being Subgroup of G holds

( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )

for H being Subgroup of G holds

( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )

proof end;

definition

let G be Group;

let H be Subgroup of G;

assume A1: Left_Cosets H is finite ;

ex b_{1} being Element of NAT ex B being finite set st

( B = Left_Cosets H & b_{1} = card B )

for b_{1}, b_{2} being Element of NAT st ex B being finite set st

( B = Left_Cosets H & b_{1} = card B ) & ex B being finite set st

( B = Left_Cosets H & b_{2} = card B ) holds

b_{1} = b_{2}
;

end;
let H be Subgroup of G;

assume A1: Left_Cosets H is finite ;

func index H -> Element of NAT means :Def18: :: GROUP_2:def 18

ex B being finite set st

( B = Left_Cosets H & it = card B );

existence ex B being finite set st

( B = Left_Cosets H & it = card B );

ex b

( B = Left_Cosets H & b

proof end;

uniqueness for b

( B = Left_Cosets H & b

( B = Left_Cosets H & b

b

:: deftheorem Def18 defines index GROUP_2:def 18 :

for G being Group

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

for b_{3} being Element of NAT holds

( b_{3} = index H iff ex B being finite set st

( B = Left_Cosets H & b_{3} = card B ) );

for G being Group

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

for b

( b

( B = Left_Cosets H & b

theorem :: GROUP_2:146

for G being Group

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

( ex B being finite set st

( B = Left_Cosets H & index H = card B ) & ex C being finite set st

( C = Right_Cosets H & index H = card C ) )

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

( ex B being finite set st

( B = Left_Cosets H & index H = card B ) & ex C being finite set st

( C = Right_Cosets H & index H = card C ) )

proof end;

Lm5: for k being Nat

for X being finite set st ( for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) ) holds

ex C being finite set st

( C = union X & card C = k * (card X) )

proof end;

:: Lagrange Theorem for Groups

theorem :: GROUP_2:149

for G being finite Group

for I, H being Subgroup of G

for J being Subgroup of H st I = J holds

index I = (index J) * (index H)

for I, H being Subgroup of G

for J being Subgroup of H st I = J holds

index I = (index J) * (index H)

proof end;

theorem :: GROUP_2:151

for G being strict Group

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

H = G

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

H = G

proof end;

theorem :: GROUP_2:155

for G being Group

for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds

( G is finite & H = (1). G )

for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds

( G is finite & H = (1). G )

proof end;

::

:: Auxiliary theorems.

::

:: Auxiliary theorems.

::

theorem :: GROUP_2:156