:: GROUP_5 semantic presentation

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

{ F₄(b₁,b₂,b₃) where B is Element of F₁(), B is Element of F₂(), B is Element of F₃() : P₁[b₁,b₂,b₃] } is Subset of F₂()

proof end;

theorem Th1: :: GROUP_5:1

for b₁ being set
for b₂ being Group holds
( b₁ in (1). b₂ iff b₁ = 1. b₂ )

proof end;

theorem Th2: :: GROUP_5:2

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ |^ b₃ in b₄

proof end;

theorem Th3: :: GROUP_5:3

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being strict normal Subgroup of b₁ st b₂ in b₄ holds
b₂ |^ b₃ in b₄

proof end;

theorem Th4: :: GROUP_5:4

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ holds
( b₁ in b₃ * b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = b₅ * b₆ & b₅ in b₃ & b₆ in b₄ ) )

proof end;

theorem Th5: :: GROUP_5:5

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ st b₃ * b₄ = b₄ * b₃ holds
( b₁ in b₃ "\/" b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = b₅ * b₆ & b₅ in b₃ & b₆ in b₄ ) )

proof end;

theorem Th6: :: GROUP_5:6

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ st b₂ is commutative Group holds
( b₁ in b₃ "\/" b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = b₅ * b₆ & b₅ in b₃ & b₆ in b₄ ) )

proof end;

theorem Th7: :: GROUP_5:7

for b₁ being set
for b₂ being Group
for b₃, b₄ being strict normal Subgroup of b₂ holds
( b₁ in b₃ "\/" b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = b₅ * b₆ & b₅ in b₃ & b₆ in b₄ ) )

proof end;

theorem Th8: :: GROUP_5:8

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being normal Subgroup of b₁ holds b₂ * b₃ = b₃ * b₂

proof end;

definition

let c₁ be Group;
let c₂ be FinSequence of the carrier of c₁;
let c₃ be Element of c₁;
func c₂ |^ c₃ -> FinSequence of the carrier of a₁ means :Def1: :: GROUP_5:def 1
( len a₄ = len a₂ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₄ . b₁ = (a₂ /. b₁) |^ a₃ ) );
existence

proof end;

correctness

proof end;

end;

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

theorem Th9: :: GROUP_5:9

canceled;

theorem Th10: :: GROUP_5:10

canceled;

theorem Th11: :: GROUP_5:11

canceled;

theorem Th12: :: GROUP_5:12

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being FinSequence of the carrier of b₁ holds (b₃ |^ b₂) ^ (b₄ |^ b₂) = (b₃ ^ b₄) |^ b₂

proof end;

theorem Th13: :: GROUP_5:13

for b₁ being Group
for b₂ being Element of b₁ holds (<*> the carrier of b₁) |^ b₂ = {}

proof end;

theorem Th14: :: GROUP_5:14

for b₁ being Group
for b₂, b₃ being Element of b₁ holds <*b₂*> |^ b₃ = <*(b₂ |^ b₃)*>

proof end;

theorem Th15: :: GROUP_5:15

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds <*b₂,b₃*> |^ b₄ = <*(b₂ |^ b₄),(b₃ |^ b₄)*>

proof end;

theorem Th16: :: GROUP_5:16

for b₁ being Group
for b₂, b₃, b₄, b₅ being Element of b₁ holds <*b₂,b₃,b₄*> |^ b₅ = <*(b₂ |^ b₅),(b₃ |^ b₅),(b₄ |^ b₅)*>

proof end;

theorem Th17: :: GROUP_5:17

for b₁ being Group
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Product (b₃ |^ b₂) = (Product b₃) |^ b₂

proof end;

theorem Th18: :: GROUP_5:18

for b₁ being Group
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁
for b₄ being FinSequence of INT holds (b₃ |^ b₂) |^ b₄ = (b₃ |^ b₄) |^ b₂

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Element of c₁;
func [.c₂,c₃.] -> Element of a₁ equals :: GROUP_5:def 2
(((a₂ " ) * (a₃ " )) * a₂) * a₃;
correctness ;

end;

:: deftheorem Def2 defines [. GROUP_5:def 2 :

theorem Th19: :: GROUP_5:19

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( [.b₂,b₃.] = (((b₂ " ) * (b₃ " )) * b₂) * b₃ & [.b₂,b₃.] = ((b₂ " ) * ((b₃ " ) * b₂)) * b₃ & [.b₂,b₃.] = (b₂ " ) * (((b₃ " ) * b₂) * b₃) & [.b₂,b₃.] = (b₂ " ) * ((b₃ " ) * (b₂ * b₃)) & [.b₂,b₃.] = ((b₂ " ) * (b₃ " )) * (b₂ * b₃) )

proof end;

theorem Th20: :: GROUP_5:20

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃.] = ((b₃ * b₂) " ) * (b₂ * b₃)

proof end;

theorem Th21: :: GROUP_5:21

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( [.b₂,b₃.] = ((b₃ " ) |^ b₂) * b₃ & [.b₂,b₃.] = (b₂ " ) * (b₂ |^ b₃) )

proof end;

theorem Th22: :: GROUP_5:22

for b₁ being Group
for b₂ being Element of b₁ holds
( [.(1. b₁),b₂.] = 1. b₁ & [.b₂,(1. b₁).] = 1. b₁ )

proof end;

theorem Th23: :: GROUP_5:23

for b₁ being Group
for b₂ being Element of b₁ holds [.b₂,b₂.] = 1. b₁

proof end;

theorem Th24: :: GROUP_5:24

for b₁ being Group
for b₂ being Element of b₁ holds
( [.b₂,(b₂ " ).] = 1. b₁ & [.(b₂ " ),b₂.] = 1. b₁ )

proof end;

theorem Th25: :: GROUP_5:25

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃.] " = [.b₃,b₂.]

proof end;

theorem Th26: :: GROUP_5:26

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds [.b₂,b₃.] |^ b₄ = [.(b₂ |^ b₄),(b₃ |^ b₄).]

proof end;

theorem Th27: :: GROUP_5:27

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃.] = (((b₂ " ) |^ 2) * ((b₂ * (b₃ " )) |^ 2)) * (b₃ |^ 2)

proof end;

theorem Th28: :: GROUP_5:28

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds [.(b₂ * b₃),b₄.] = ([.b₂,b₄.] |^ b₃) * [.b₃,b₄.]

proof end;

theorem Th29: :: GROUP_5:29

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds [.b₂,(b₃ * b₄).] = [.b₂,b₄.] * ([.b₂,b₃.] |^ b₄)

proof end;

theorem Th30: :: GROUP_5:30

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.(b₂ " ),b₃.] = [.b₃,b₂.] |^ (b₂ " )

proof end;

theorem Th31: :: GROUP_5:31

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,(b₃ " ).] = [.b₃,b₂.] |^ (b₃ " )

proof end;

theorem Th32: :: GROUP_5:32

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( [.(b₂ " ),(b₃ " ).] = [.b₂,b₃.] |^ ((b₂ * b₃) " ) & [.(b₂ " ),(b₃ " ).] = [.b₂,b₃.] |^ ((b₃ * b₂) " ) )

proof end;

theorem Th33: :: GROUP_5:33

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,(b₃ |^ (b₂ " )).] = [.b₃,(b₂ " ).]

proof end;

theorem Th34: :: GROUP_5:34

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.(b₂ |^ (b₃ " )),b₃.] = [.(b₃ " ),b₂.]

proof end;

theorem Th35: :: GROUP_5:35

for b₁ being Nat
for b₂ being Group
for b₃, b₄ being Element of b₂ holds [.(b₃ |^ b₁),b₄.] = (b₃ |^ (- b₁)) * ((b₃ |^ b₄) |^ b₁)

proof end;

theorem Th36: :: GROUP_5:36

for b₁ being Nat
for b₂ being Group
for b₃, b₄ being Element of b₂ holds [.b₃,(b₄ |^ b₁).] = ((b₄ |^ b₃) |^ (- b₁)) * (b₄ |^ b₁)

proof end;

theorem Th37: :: GROUP_5:37

for b₁ being Integer
for b₂ being Group
for b₃, b₄ being Element of b₂ holds [.(b₃ |^ b₁),b₄.] = (b₃ |^ (- b₁)) * ((b₃ |^ b₄) |^ b₁)

proof end;

theorem Th38: :: GROUP_5:38

for b₁ being Integer
for b₂ being Group
for b₃, b₄ being Element of b₂ holds [.b₃,(b₄ |^ b₁).] = ((b₄ |^ b₃) |^ (- b₁)) * (b₄ |^ b₁)

proof end;

theorem Th39: :: GROUP_5:39

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( [.b₂,b₃.] = 1. b₁ iff b₂ * b₃ = b₃ * b₂ )

proof end;

Lemma24: for b₁ being commutative Group
for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂
;

theorem Th40: :: GROUP_5:40

for b₁ being Group holds
( b₁ is commutative Group iff for b₂, b₃ being Element of b₁ holds [.b₂,b₃.] = 1. b₁ )

proof end;

theorem Th41: :: GROUP_5:41

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ st b₂ in b₄ & b₃ in b₄ holds
[.b₂,b₃.] in b₄

proof end;

definition

let c₁ be Group;
let c₂, c₃, c₄ be Element of c₁;
func [.c₂,c₃,c₄.] -> Element of a₁ equals :: GROUP_5:def 3
[.[.a₂,a₃.],a₄.];
correctness ;

end;

:: deftheorem Def3 defines [. GROUP_5:def 3 :

theorem Th42: :: GROUP_5:42

canceled;

theorem Th43: :: GROUP_5:43

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( [.b₂,b₃,(1. b₁).] = 1. b₁ & [.b₂,(1. b₁),b₃.] = 1. b₁ & [.(1. b₁),b₂,b₃.] = 1. b₁ )

proof end;

theorem Th44: :: GROUP_5:44

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₂,b₃.] = 1. b₁

proof end;

theorem Th45: :: GROUP_5:45

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃,b₂.] = [.(b₂ |^ b₃),b₂.]

proof end;

theorem Th46: :: GROUP_5:46

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃,b₃.] = ([.b₂,(b₃ " ).] * [.b₂,b₃.]) |^ b₃

proof end;

theorem Th47: :: GROUP_5:47

for b₁ being Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃,(b₃ |^ b₂).] = [.b₃,[.b₃,b₂.].]

proof end;

theorem Th48: :: GROUP_5:48

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds [.(b₂ * b₃),b₄.] = ([.b₂,b₄.] * [.b₂,b₄,b₃.]) * [.b₃,b₄.]

proof end;

theorem Th49: :: GROUP_5:49

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds [.b₂,(b₃ * b₄).] = ([.b₂,b₄.] * [.b₂,b₃.]) * [.b₂,b₃,b₄.]

proof end;

theorem Th50: :: GROUP_5:50

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds (([.b₂,(b₃ " ),b₄.] |^ b₃) * ([.b₃,(b₄ " ),b₂.] |^ b₄)) * ([.b₄,(b₂ " ),b₃.] |^ b₂) = 1. b₁

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
func commutators c₂,c₃ -> Subset of a₁ equals :: GROUP_5:def 4
{ [.b₁,b₂.] where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def4 defines commutators GROUP_5:def 4 :

theorem Th51: :: GROUP_5:51

canceled;

theorem Th52: :: GROUP_5:52

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subset of b₂ holds
( b₁ in commutators b₃,b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = [.b₅,b₆.] & b₅ in b₃ & b₆ in b₄ ) ) ;

theorem Th53: :: GROUP_5:53

for b₁ being Group
for b₂ being Subset of b₁ holds
( commutators ({} the carrier of b₁),b₂ = {} & commutators b₂,({} the carrier of b₁) = {} )

proof end;

theorem Th54: :: GROUP_5:54

for b₁ being Group
for b₂, b₃ being Element of b₁ holds commutators {b₂},{b₃} = {[.b₂,b₃.]}

proof end;

theorem Th55: :: GROUP_5:55

for b₁ being Group
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
commutators b₂,b₄ c= commutators b₃,b₅

proof end;

theorem Th56: :: GROUP_5:56

for b₁ being Group holds
( b₁ is commutative Group iff for b₂, b₃ being Subset of b₁ st b₂ <> {} & b₃ <> {} holds
commutators b₂,b₃ = {(1. b₁)} )

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
func commutators c₂,c₃ -> Subset of a₁ equals :: GROUP_5:def 5
commutators (carr a₂),(carr a₃);
correctness ;

end;

:: deftheorem Def5 defines commutators GROUP_5:def 5 :

theorem Th57: :: GROUP_5:57

canceled;

theorem Th58: :: GROUP_5:58

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ holds
( b₁ in commutators b₃,b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = [.b₅,b₆.] & b₅ in b₃ & b₆ in b₄ ) )

proof end;

theorem Th59: :: GROUP_5:59

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds 1. b₁ in commutators b₂,b₃

proof end;

theorem Th60: :: GROUP_5:60

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( commutators ((1). b₁),b₂ = {(1. b₁)} & commutators b₂,((1). b₁) = {(1. b₁)} )

proof end;

theorem Th61: :: GROUP_5:61

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict normal Subgroup of b₁ holds
( commutators b₂,b₃ c= carr b₃ & commutators b₃,b₂ c= carr b₃ )

proof end;

theorem Th62: :: GROUP_5:62

for b₁ being Group
for b₂, b₃, b₄, b₅ being Subgroup of b₁ st b₂ is Subgroup of b₃ & b₄ is Subgroup of b₅ holds
commutators b₂,b₄ c= commutators b₃,b₅

proof end;

theorem Th63: :: GROUP_5:63

for b₁ being Group holds
( b₁ is commutative Group iff for b₂, b₃ being Subgroup of b₁ holds commutators b₂,b₃ = {(1. b₁)} )

proof end;

definition

let c₁ be Group;
func commutators c₁ -> Subset of a₁ equals :: GROUP_5:def 6
commutators ((Omega). a₁),((Omega). a₁);
correctness ;

end;

:: deftheorem Def6 defines commutators GROUP_5:def 6 :

theorem Th64: :: GROUP_5:64

canceled;

theorem Th65: :: GROUP_5:65

for b₁ being set
for b₂ being Group holds
( b₁ in commutators b₂ iff ex b₃, b₄ being Element of b₂ st b₁ = [.b₃,b₄.] )

proof end;

theorem Th66: :: GROUP_5:66

for b₁ being Group holds
( b₁ is commutative Group iff commutators b₁ = {(1. b₁)} )

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
func [.c₂,c₃.] -> strict Subgroup of a₁ equals :: GROUP_5:def 7
gr (commutators a₂,a₃);
correctness ;

end;

:: deftheorem Def7 defines [. GROUP_5:def 7 :

theorem Th67: :: GROUP_5:67

canceled;

theorem Th68: :: GROUP_5:68

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂ in b₄ & b₃ in b₅ holds
[.b₂,b₃.] in [.b₄,b₅.]

proof end;

theorem Th69: :: GROUP_5:69

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subset of b₂ holds
( b₁ in [.b₃,b₄.] iff ex b₅ being FinSequence of the carrier of b₂ex b₆ being FinSequence of INT st
( len b₅ = len b₆ & rng b₅ c= commutators b₃,b₄ & b₁ = Product (b₅ |^ b₆) ) )

proof end;

theorem Th70: :: GROUP_5:70

for b₁ being Group
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
[.b₂,b₄.] is Subgroup of [.b₃,b₅.]

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
func [.c₂,c₃.] -> strict Subgroup of a₁ equals :: GROUP_5:def 8
[.(carr a₂),(carr a₃).];
correctness ;

end;

:: deftheorem Def8 defines [. GROUP_5:def 8 :

theorem Th71: :: GROUP_5:71

canceled;

theorem Th72: :: GROUP_5:72

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds [.b₂,b₃.] = gr (commutators b₂,b₃) ;

theorem Th73: :: GROUP_5:73

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ holds
( b₁ in [.b₃,b₄.] iff ex b₅ being FinSequence of the carrier of b₂ex b₆ being FinSequence of INT st
( len b₅ = len b₆ & rng b₅ c= commutators b₃,b₄ & b₁ = Product (b₅ |^ b₆) ) ) by Th69;

theorem Th74: :: GROUP_5:74

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subgroup of b₁ st b₂ in b₄ & b₃ in b₅ holds
[.b₂,b₃.] in [.b₄,b₅.]

proof end;

theorem Th75: :: GROUP_5:75

for b₁ being Group
for b₂, b₃, b₄, b₅ being Subgroup of b₁ st b₂ is Subgroup of b₃ & b₄ is Subgroup of b₅ holds
[.b₂,b₄.] is Subgroup of [.b₃,b₅.]

proof end;

theorem Th76: :: GROUP_5:76

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict normal Subgroup of b₁ holds
( [.b₃,b₂.] is Subgroup of b₃ & [.b₂,b₃.] is Subgroup of b₃ )

proof end;

theorem Th77: :: GROUP_5:77

for b₁ being Group
for b₂, b₃ being strict normal Subgroup of b₁ holds [.b₂,b₃.] is normal Subgroup of b₁

proof end;

Lemma40: for b₁ being Group
for b₂, b₃ being normal Subgroup of b₁ holds [.b₂,b₃.] is Subgroup of [.b₃,b₂.]

proof end;

theorem Th78: :: GROUP_5:78

for b₁ being Group
for b₂, b₃ being normal Subgroup of b₁ holds [.b₂,b₃.] = [.b₃,b₂.]

proof end;

theorem Th79: :: GROUP_5:79

for b₁ being Group
for b₂, b₃, b₄ being strict normal Subgroup of b₁ holds [.(b₂ "\/" b₃),b₄.] = [.b₂,b₄.] "\/" [.b₃,b₄.]

proof end;

theorem Th80: :: GROUP_5:80

for b₁ being Group
for b₂, b₃, b₄ being strict normal Subgroup of b₁ holds [.b₂,(b₃ "\/" b₄).] = [.b₂,b₃.] "\/" [.b₂,b₄.]

proof end;

definition

let c₁ be Group;
func c₁ ` -> strict normal Subgroup of a₁ equals :: GROUP_5:def 9
[.((Omega). a₁),((Omega). a₁).];
coherence

proof end;

end;

:: deftheorem Def9 defines ` GROUP_5:def 9 :

theorem Th81: :: GROUP_5:81

canceled;

theorem Th82: :: GROUP_5:82

for b₁ being Group holds b₁ ` = gr (commutators b₁) ;

theorem Th83: :: GROUP_5:83

for b₁ being set
for b₂ being Group holds
( b₁ in b₂ ` iff ex b₃ being FinSequence of the carrier of b₂ex b₄ being FinSequence of INT st
( len b₃ = len b₄ & rng b₃ c= commutators b₂ & b₁ = Product (b₃ |^ b₄) ) )

proof end;

theorem Th84: :: GROUP_5:84

for b₁ being strict Group
for b₂, b₃ being Element of b₁ holds [.b₂,b₃.] in b₁ `

proof end;

theorem Th85: :: GROUP_5:85

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

proof end;

theorem Th86: :: GROUP_5:86

for b₁ being Group
for b₂ being strict Subgroup of b₁ st Left_Cosets b₂ is finite & index b₂ = 2 holds
b₁ ` is Subgroup of b₂

proof end;

definition

let c₁ be Group;
func center c₁ -> strict Subgroup of a₁ means :Def10: :: GROUP_5:def 10
the carrier of a₂ = { b₁ where B is Element of a₁ : for b₁ being Element of a₁ holds b₁ * b₂ = b₂ * b₁ } ;
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def10 defines center GROUP_5:def 10 :

theorem Th87: :: GROUP_5:87

canceled;

theorem Th88: :: GROUP_5:88

canceled;

theorem Th89: :: GROUP_5:89

for b₁ being Group
for b₂ being Element of b₁ holds
( b₂ in center b₁ iff for b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂ )

proof end;

theorem Th90: :: GROUP_5:90

for b₁ being Group holds center b₁ is normal Subgroup of b₁

proof end;

theorem Th91: :: GROUP_5:91

for b₁ being Group
for b₂ being Subgroup of b₁ st b₂ is Subgroup of center b₁ holds
b₂ is normal Subgroup of b₁

proof end;

theorem Th92: :: GROUP_5:92

for b₁ being Group holds center b₁ is commutative

proof end;

theorem Th93: :: GROUP_5:93

for b₁ being Group
for b₂ being Element of b₁ holds
( b₂ in center b₁ iff con_class b₂ = {b₂} )

proof end;

theorem Th94: :: GROUP_5:94

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

proof end;