:: WEDDWITT semantic presentation

theorem Th1: :: WEDDWITT:1

for b₁ being Nat
for b₂ being Real st 1 < b₂ & b₂ |^ b₁ = 1 holds
b₁ = 0

proof end;

theorem Th2: :: WEDDWITT:2

for b₁, b₂, b₃ being Nat
for b₄ being Real st 1 < b₄ & 0 < b₂ holds
b₄ |^ ((b₁ * b₂) + b₃) = (b₄ |^ b₁) * (b₄ |^ ((b₁ * (b₂ -' 1)) + b₃))

proof end;

theorem Th3: :: WEDDWITT:3

for b₁, b₂, b₃ being Nat st 0 < b₂ & 1 < b₁ & (b₁ |^ b₂) -' 1 divides (b₁ |^ b₃) -' 1 holds
b₂ divides b₃

proof end;

theorem Th4: :: WEDDWITT:4

for b₁, b₂ being Nat st 0 < b₂ holds
Card (Funcs b₁,b₂) = b₂ |^ b₁

proof end;

theorem Th5: :: WEDDWITT:5

for b₁ being FinSequence of NAT
for b₂ being Nat st ( for b₃ being Nat st b₃ in dom b₁ holds
b₂ divides b₁ /. b₃ ) holds
b₂ divides Sum b₁

proof end;

theorem Th6: :: WEDDWITT:6

for b₁ being finite set
for b₂ being a_partition of b₁
for b₃ being FinSequence of b₂ st b₃ is one-to-one & rng b₃ = b₂ holds
for b₄ being FinSequence of NAT st len b₄ = len b₃ & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = Card (b₃ . b₅) ) holds
card b₁ = Sum b₄

proof end;

registration

cluster finite HGrStr ;
existence

proof end;

end;

registration

let c₁ be finite Group;
cluster center a₁ -> finite ;
correctness by GROUP_2:48;

end;

definition

let c₁ be Group;
let c₂ be Element of c₁;
func Centralizer c₂ -> strict Subgroup of a₁ means :Def1: :: WEDDWITT:def 1
the carrier of a₃ = { b₁ where B is Element of a₁ : a₂ * b₁ = b₁ * a₂ } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :

registration

let c₁ be finite Group;
let c₂ be Element of c₁;
cluster Centralizer a₂ -> strict finite ;
correctness by GROUP_2:48;

end;

theorem Th7: :: WEDDWITT:7

for b₁ being Group
for b₂ being Element of b₁
for b₃ being set st b₃ in Centralizer b₂ holds
b₃ in b₁

proof end;

theorem Th8: :: WEDDWITT:8

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ * b₃ = b₃ * b₂ iff b₃ is Element of (Centralizer b₂) )

proof end;

registration

let c₁ be Group;
let c₂ be Element of c₁;
cluster con_class a₂ -> non empty ;
correctness by GROUP_3:98;

end;

definition

let c₁ be Group;
let c₂ be Element of c₁;
func c₂ -con_map -> Function of the carrier of a₁, con_class a₂ means :Def2: :: WEDDWITT:def 2
for b₁ being Element of a₁ holds a₃ . b₁ = a₂ |^ b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :

theorem Th9: :: WEDDWITT:9

for b₁ being finite Group
for b₂ being Element of b₁
for b₃ being Element of con_class b₂ holds card ((b₂ -con_map ) " {b₃}) = ord (Centralizer b₂)

proof end;

theorem Th10: :: WEDDWITT:10

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Element of con_class b₂ st b₃ <> b₄ holds
(b₂ -con_map ) " {b₃} misses (b₂ -con_map ) " {b₄}

proof end;

theorem Th11: :: WEDDWITT:11

for b₁ being Group
for b₂ being Element of b₁ holds { ((b₂ -con_map ) " {b₃}) where B is Element of con_class b₂ : verum } is a_partition of the carrier of b₁

proof end;

theorem Th12: :: WEDDWITT:12

for b₁ being finite Group
for b₂ being Element of b₁ holds Card { ((b₂ -con_map ) " {b₃}) where B is Element of con_class b₂ : verum } = card (con_class b₂)

proof end;

theorem Th13: :: WEDDWITT:13

for b₁ being finite Group
for b₂ being Element of b₁ holds ord b₁ = (card (con_class b₂)) * (ord (Centralizer b₂))

proof end;

definition

let c₁ be Group;
func conjugate_Classes c₁ -> a_partition of the carrier of a₁ equals :: WEDDWITT:def 3
{ b₁ where B is Subset of a₁ : ex b₁ being Element of a₁ st b₁ = con_class b₂ } ;
correctness

proof end;

end;

:: deftheorem Def3 defines conjugate_Classes WEDDWITT:def 3 :

theorem Th14: :: WEDDWITT:14

for b₁ being Group
for b₂ being set holds
( b₂ in conjugate_Classes b₁ iff ex b₃ being Element of b₁ st con_class b₃ = b₂ )

proof end;

theorem Th15: :: WEDDWITT:15

for b₁ being finite Group
for b₂ being FinSequence of conjugate_Classes b₁ st b₂ is one-to-one & rng b₂ = conjugate_Classes b₁ holds
for b₃ being FinSequence of NAT st len b₃ = len b₂ & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = Card (b₂ . b₄) ) holds
ord b₁ = Sum b₃

proof end;

theorem Th16: :: WEDDWITT:16

for b₁ being finite Field
for b₂ being VectSp of b₁
for b₃, b₄ being Nat st b₂ is finite-dimensional & b₃ = dim b₂ & b₄ = Card the carrier of b₁ holds
Card the carrier of b₂ = b₄ |^ b₃

proof end;

definition

let c₁ be Skew-Field;
func center c₁ -> strict Field means :Def4: :: WEDDWITT:def 4
( the carrier of a₂ = { b₁ where B is Element of a₁ : for b₁ being Element of a₁ holds b₁ * b₂ = b₂ * b₁ } & the add of a₂ = the add of a₁ || the carrier of a₂ & the mult of a₂ = the mult of a₁ || the carrier of a₂ & the Zero of a₂ = the Zero of a₁ & the unity of a₂ = 1. a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines center WEDDWITT:def 4 :

theorem Th17: :: WEDDWITT:17

for b₁ being Skew-Field holds the carrier of (center b₁) c= the carrier of b₁

proof end;

E21: now

let c₁ be Skew-Field;
set c₂ = center c₁;
let c₃, c₄ be Element of (center c₁);
assume E22: c₄ = 1. c₁ ;
E23: [c₃,c₄] in [:the carrier of (center c₁),the carrier of (center c₁):] by ZFMISC_1:106;
E24: the carrier of (center c₁) c= the carrier of c₁ by Th17;
c₃ in the carrier of (center c₁) ;
then reconsider c₅ = c₃ as Element of c₁ by E24;
E25: the mult of (center c₁) = the mult of c₁ || the carrier of (center c₁) by Def4;
thus c₃ * c₄ = the mult of (center c₁) . c₃,c₄
.= the mult of (center c₁) . [c₃,c₄]
.= the mult of c₁ . [c₃,c₄] by E25, E23, FUNCT_1:72
.= the mult of c₁ . c₃,(1. c₁) by E22
.= c₅ * (1. c₁)
.= c₃ by GROUP_1:def 5 ;
hence c₄ * c₃ = c₃ ;

end;

Lemma22: for b₁ being Skew-Field holds 1. (center b₁) = 1. b₁

proof end;

registration

let c₁ be finite Skew-Field;
cluster center a₁ -> finite strict ;
correctness

proof end;

end;

theorem Th18: :: WEDDWITT:18

for b₁ being Skew-Field
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 Th19: :: WEDDWITT:19

for b₁ being Skew-Field holds 0. b₁ in center b₁

proof end;

theorem Th20: :: WEDDWITT:20

for b₁ being Skew-Field holds 1. b₁ in center b₁

proof end;

theorem Th21: :: WEDDWITT:21

for b₁ being finite Skew-Field holds 1 < card the carrier of (center b₁)

proof end;

theorem Th22: :: WEDDWITT:22

for b₁ being finite Skew-Field holds
( card the carrier of (center b₁) = card the carrier of b₁ iff b₁ is commutative )

proof end;

theorem Th23: :: WEDDWITT:23

for b₁ being Skew-Field holds the carrier of (center b₁) = the carrier of (center (MultGroup b₁)) \/ {(0. b₁)}

proof end;

definition

let c₁ be Skew-Field;
let c₂ be Element of c₁;
func centralizer c₂ -> strict Skew-Field means :Def5: :: WEDDWITT:def 5
( the carrier of a₃ = { b₁ where B is Element of a₁ : b₁ * a₂ = a₂ * b₁ } & the add of a₃ = the add of a₁ || the carrier of a₃ & the mult of a₃ = the mult of a₁ || the carrier of a₃ & the Zero of a₃ = the Zero of a₁ & the unity of a₃ = 1. a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :

theorem Th24: :: WEDDWITT:24

for b₁ being Skew-Field
for b₂ being Element of b₁ holds the carrier of (centralizer b₂) c= the carrier of b₁

proof end;

theorem Th25: :: WEDDWITT:25

for b₁ being Skew-Field
for b₂, b₃ being Element of b₁ holds
( b₃ in the carrier of (centralizer b₂) iff b₃ * b₂ = b₂ * b₃ )

proof end;

theorem Th26: :: WEDDWITT:26

for b₁ being Skew-Field
for b₂ being Element of b₁ holds the carrier of (center b₁) c= the carrier of (centralizer b₂)

proof end;

theorem Th27: :: WEDDWITT:27

for b₁ being Skew-Field
for b₂, b₃, b₄ being Element of b₁ st b₃ in the carrier of (center b₁) & b₄ in the carrier of (centralizer b₂) holds
b₃ * b₄ in the carrier of (centralizer b₂)

proof end;

theorem Th28: :: WEDDWITT:28

for b₁ being Skew-Field
for b₂ being Element of b₁ holds
( 0. b₁ is Element of (centralizer b₂) & 1. b₁ is Element of (centralizer b₂) ) by Def5;

registration

let c₁ be finite Skew-Field;
let c₂ be Element of c₁;
cluster centralizer a₂ -> finite strict ;
correctness

proof end;

end;

theorem Th29: :: WEDDWITT:29

for b₁ being finite Skew-Field
for b₂ being Element of b₁ holds 1 < card the carrier of (centralizer b₂)

proof end;

theorem Th30: :: WEDDWITT:30

for b₁ being Skew-Field
for b₂ being Element of b₁
for b₃ being Element of (MultGroup b₁) st b₃ = b₂ holds
the carrier of (centralizer b₂) = the carrier of (Centralizer b₃) \/ {(0. b₁)}

proof end;

theorem Th31: :: WEDDWITT:31

for b₁ being finite Skew-Field
for b₂ being Element of b₁
for b₃ being Element of (MultGroup b₁) st b₃ = b₂ holds
ord (Centralizer b₃) = (card the carrier of (centralizer b₂)) - 1

proof end;

definition

let c₁ be Skew-Field;
func VectSp_over_center c₁ -> strict VectSp of center a₁ means :Def6: :: WEDDWITT:def 6
( LoopStr(# the carrier of a₂,the add of a₂,the Zero of a₂ #) = LoopStr(# the carrier of a₁,the add of a₁,the Zero of a₁ #) & the lmult of a₂ = the mult of a₁ | [:the carrier of (center a₁),the carrier of a₁:] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def 6 :

theorem Th32: :: WEDDWITT:32

for b₁ being finite Skew-Field holds card the carrier of b₁ = (card the carrier of (center b₁)) |^ (dim (VectSp_over_center b₁))

proof end;

theorem Th33: :: WEDDWITT:33

for b₁ being finite Skew-Field holds 0 < dim (VectSp_over_center b₁)

proof end;

definition

let c₁ be Skew-Field;
let c₂ be Element of c₁;
func VectSp_over_center c₂ -> strict VectSp of center a₁ means :Def7: :: WEDDWITT:def 7
( LoopStr(# the carrier of a₃,the add of a₃,the Zero of a₃ #) = LoopStr(# the carrier of (centralizer a₂),the add of (centralizer a₂),the Zero of (centralizer a₂) #) & the lmult of a₃ = the mult of a₁ | [:the carrier of (center a₁),the carrier of (centralizer a₂):] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :

theorem Th34: :: WEDDWITT:34

for b₁ being finite Skew-Field
for b₂ being Element of b₁ holds card the carrier of (centralizer b₂) = (card the carrier of (center b₁)) |^ (dim (VectSp_over_center b₂))

proof end;

theorem Th35: :: WEDDWITT:35

for b₁ being finite Skew-Field
for b₂ being Element of b₁ holds 0 < dim (VectSp_over_center b₂)

proof end;

theorem Th36: :: WEDDWITT:36

for b₁ being finite Skew-Field
for b₂ being Element of b₁ st b₂ is Element of (MultGroup b₁) holds
((card the carrier of (center b₁)) |^ (dim (VectSp_over_center b₂))) - 1 divides ((card the carrier of (center b₁)) |^ (dim (VectSp_over_center b₁))) - 1

proof end;

theorem Th37: :: WEDDWITT:37

for b₁ being finite Skew-Field
for b₂ being Element of b₁ st b₂ is Element of (MultGroup b₁) holds
dim (VectSp_over_center b₂) divides dim (VectSp_over_center b₁)

proof end;

theorem Th38: :: WEDDWITT:38

for b₁ being finite Skew-Field holds card the carrier of (center (MultGroup b₁)) = (card the carrier of (center b₁)) - 1

proof end;

theorem Th39: :: WEDDWITT:39

for b₁ being finite Skew-Field holds b₁ is commutative

proof end;

theorem Th40: :: WEDDWITT:40

for b₁ being Skew-Field holds 1. (center b₁) = 1. b₁ by Lemma22;

E46: now

let c₁ be Skew-Field;
let c₂ be Element of c₁;
set c₃ = centralizer c₂;
let c₄, c₅ be Element of (centralizer c₂);
assume E47: c₅ = 1. c₁ ;
E48: [c₄,c₅] in [:the carrier of (centralizer c₂),the carrier of (centralizer c₂):] by ZFMISC_1:106;
E49: [c₅,c₄] in [:the carrier of (centralizer c₂),the carrier of (centralizer c₂):] by ZFMISC_1:106;
E50: the carrier of (centralizer c₂) c= the carrier of c₁ by Th24;
c₄ in the carrier of (centralizer c₂) ;
then reconsider c₆ = c₄ as Element of c₁ by E50;
E51: the mult of (centralizer c₂) = the mult of c₁ || the carrier of (centralizer c₂) by Def5;
thus c₄ * c₅ = the mult of (centralizer c₂) . c₄,c₅
.= the mult of (centralizer c₂) . [c₄,c₅]
.= the mult of c₁ . [c₄,c₅] by E51, E48, FUNCT_1:72
.= the mult of c₁ . c₄,(1. c₁) by E47
.= c₆ * (1. c₁)
.= c₄ by GROUP_1:def 5 ;
thus c₅ * c₄ = the mult of (centralizer c₂) . c₅,c₄
.= the mult of (centralizer c₂) . [c₅,c₄]
.= the mult of c₁ . [c₅,c₄] by E51, E49, FUNCT_1:72
.= the mult of c₁ . (1. c₁),c₄ by E47
.= (1. c₁) * c₆
.= c₄ by GROUP_1:def 5 ;

end;

theorem Th41: :: WEDDWITT:41

for b₁ being Skew-Field
for b₂ being Element of b₁ holds 1. (centralizer b₂) = 1. b₁

proof end;