:: WEDDWITT semantic presentation

theorem Th1: :: WEDDWITT:1

for a being Nat
for q being Real st 1 < q & q |^ a = 1 holds
a = 0

proof end;

theorem Th2: :: WEDDWITT:2

for a, k, r being Nat
for x being Real st 1 < x & 0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))

proof end;

theorem Th3: :: WEDDWITT:3

for q, a, b being Nat st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b) -' 1 holds
a divides b

proof end;

theorem Th4: :: WEDDWITT:4

for n, q being Nat st 0 < q holds
Card (Funcs n,q) = q |^ n

proof end;

theorem Th5: :: WEDDWITT:5

for f being FinSequence of NAT
for i being Nat st ( for j being Nat st j in dom f holds
i divides f /. j ) holds
i divides Sum f

proof end;

theorem Th6: :: WEDDWITT:6

for X being finite set
for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Nat st i in dom c holds
c . i = Card (f . i) ) holds
card X = Sum c

proof end;

registration

cluster finite HGrStr ;
existence

proof end;

end;

registration

let G be finite Group;
cluster center G -> finite ;
correctness by GROUP_2:48;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :

registration

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

end;

theorem Th7: :: WEDDWITT:7

for G being Group
for a being Element of G
for x being set st x in Centralizer a holds
x in G

proof end;

theorem Th8: :: WEDDWITT:8

for G being Group
for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )

proof end;

registration

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

end;

definition

let G be Group;
let a be Element of G;
func a -con_map -> Function of the carrier of G, con_class a means :Def2: :: WEDDWITT:def 2
for x being Element of G holds it . x = a |^ x;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th9: :: WEDDWITT:9

for G being finite Group
for a being Element of G
for x being Element of con_class a holds card ((a -con_map ) " {x}) = ord (Centralizer a)

proof end;

theorem Th10: :: WEDDWITT:10

for G being Group
for a being Element of G
for x, y being Element of con_class a st x <> y holds
(a -con_map ) " {x} misses (a -con_map ) " {y}

proof end;

theorem Th11: :: WEDDWITT:11

for G being Group
for a being Element of G holds { ((a -con_map ) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G

proof end;

theorem Th12: :: WEDDWITT:12

for G being finite Group
for a being Element of G holds Card { ((a -con_map ) " {x}) where x is Element of con_class a : verum } = card (con_class a)

proof end;

theorem Th13: :: WEDDWITT:13

for G being finite Group
for a being Element of G holds ord G = (card (con_class a)) * (ord (Centralizer a))

proof end;

definition

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

proof end;

end;

:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :

theorem Th14: :: WEDDWITT:14

for G being Group
for x being set holds
( x in conjugate_Classes G iff ex a being Element of G st con_class a = x )

proof end;

theorem Th15: :: WEDDWITT:15

for G being finite Group
for f being FinSequence of conjugate_Classes G st f is one-to-one & rng f = conjugate_Classes G holds
for c being FinSequence of NAT st len c = len f & ( for i being Nat st i in dom c holds
c . i = Card (f . i) ) holds
ord G = Sum c

proof end;

theorem Th16: :: WEDDWITT:16

for F being finite Field
for V being VectSp of F
for n, q being Nat st V is finite-dimensional & n = dim V & q = Card the carrier of F holds
Card the carrier of V = q |^ n

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines center WEDDWITT:def 4 :

theorem Th17: :: WEDDWITT:17

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

proof end;

Lm1: now

let R be Skew-Field; :: thesis:
set F = center R;
let x, e be Element of (center R); :: thesis:
assume A1: e = 1. R ; :: thesis:
A2: [x,e] in [:the carrier of (center R),the carrier of (center R):] by ZFMISC_1:106;
A3: the carrier of (center R) c= the carrier of R by Th17;
x in the carrier of (center R) ;
then reconsider y = x as Element of R by A3;
A4: the mult of (center R) = the mult of R || the carrier of (center R) by Def4;
thus x * e = the mult of (center R) . x,e
.= the mult of (center R) . [x,e]
.= the mult of R . [x,e] by A4, A2, FUNCT_1:72
.= the mult of R . x,(1. R) by A1
.= y * (1. R)
.= x by GROUP_1:def 5 ; :: thesis:
hence e * x = x ; :: thesis:

end;

Lm2: for R being Skew-Field holds 1. (center R) = 1. R

proof end;

registration

let R be finite Skew-Field;
cluster center R -> finite strict ;
correctness

proof end;

end;

theorem Th18: :: WEDDWITT:18

for R being Skew-Field
for y being Element of R holds
( y in center R iff for s being Element of R holds y * s = s * y )

proof end;

theorem Th19: :: WEDDWITT:19

for R being Skew-Field holds 0. R in center R

proof end;

theorem Th20: :: WEDDWITT:20

for R being Skew-Field holds 1. R in center R

proof end;

theorem Th21: :: WEDDWITT:21

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

proof end;

theorem Th22: :: WEDDWITT:22

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

proof end;

theorem Th23: :: WEDDWITT:23

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

proof end;

definition

let R be Skew-Field;
let s be Element of R;
func centralizer s -> strict Skew-Field means :Def5: :: WEDDWITT:def 5
( the carrier of it = { x where x is Element of R : x * s = s * x } & the add of it = the add of R || the carrier of it & the mult of it = the mult of R || the carrier of it & the Zero of it = the Zero of R & the unity of it = 1. R );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :

theorem Th24: :: WEDDWITT:24

for R being Skew-Field
for s being Element of R holds the carrier of (centralizer s) c= the carrier of R

proof end;

theorem Th25: :: WEDDWITT:25

for R being Skew-Field
for s, a being Element of R holds
( a in the carrier of (centralizer s) iff a * s = s * a )

proof end;

theorem :: WEDDWITT:26

for R being Skew-Field
for s being Element of R holds the carrier of (center R) c= the carrier of (centralizer s)

proof end;

theorem Th27: :: WEDDWITT:27

for R being Skew-Field
for s, a, b being Element of R st a in the carrier of (center R) & b in the carrier of (centralizer s) holds
a * b in the carrier of (centralizer s)

proof end;

theorem Th28: :: WEDDWITT:28

for R being Skew-Field
for s being Element of R holds
( 0. R is Element of (centralizer s) & 1. R is Element of (centralizer s) ) by Def5;

registration

let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite strict ;
correctness

proof end;

end;

theorem Th29: :: WEDDWITT:29

for R being finite Skew-Field
for s being Element of R holds 1 < card the carrier of (centralizer s)

proof end;

theorem Th30: :: WEDDWITT:30

for R being Skew-Field
for s being Element of R
for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

proof end;

theorem Th31: :: WEDDWITT:31

for R being finite Skew-Field
for s being Element of R
for t being Element of (MultGroup R) st t = s holds
ord (Centralizer t) = (card the carrier of (centralizer s)) - 1

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def 6 :

theorem Th32: :: WEDDWITT:32

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

proof end;

theorem Th33: :: WEDDWITT:33

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

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :

theorem Th34: :: WEDDWITT:34

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

proof end;

theorem Th35: :: WEDDWITT:35

for R being finite Skew-Field
for s being Element of R holds 0 < dim (VectSp_over_center s)

proof end;

theorem Th36: :: WEDDWITT:36

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

proof end;

theorem Th37: :: WEDDWITT:37

for R being finite Skew-Field
for s being Element of R st s is Element of (MultGroup R) holds
dim (VectSp_over_center s) divides dim (VectSp_over_center R)

proof end;

theorem Th38: :: WEDDWITT:38

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

proof end;

theorem :: WEDDWITT:39

for R being finite Skew-Field holds R is commutative

proof end;

theorem :: WEDDWITT:40

for R being Skew-Field holds 1. (center R) = 1. R by Lm2;

Lm3: now

let R be Skew-Field; :: thesis:
let s be Element of R; :: thesis:
set F = centralizer s;
let x, e be Element of (centralizer s); :: thesis:
assume A1: e = 1. R ; :: thesis:
A2: [x,e] in [:the carrier of (centralizer s),the carrier of (centralizer s):] by ZFMISC_1:106;
A3: [e,x] in [:the carrier of (centralizer s),the carrier of (centralizer s):] by ZFMISC_1:106;
A4: the carrier of (centralizer s) c= the carrier of R by Th24;
x in the carrier of (centralizer s) ;
then reconsider y = x as Element of R by A4;
A5: the mult of (centralizer s) = the mult of R || the carrier of (centralizer s) by Def5;
thus x * e = the mult of (centralizer s) . x,e
.= the mult of (centralizer s) . [x,e]
.= the mult of R . [x,e] by A5, A2, FUNCT_1:72
.= the mult of R . x,(1. R) by A1
.= y * (1. R)
.= x by GROUP_1:def 5 ; :: thesis:
thus e * x = the mult of (centralizer s) . e,x
.= the mult of (centralizer s) . [e,x]
.= the mult of R . [e,x] by A5, A3, FUNCT_1:72
.= the mult of R . (1. R),x by A1
.= (1. R) * y
.= x by GROUP_1:def 5 ; :: thesis:

end;

theorem :: WEDDWITT:41

for R being Skew-Field
for s being Element of R holds 1. (centralizer s) = 1. R

proof end;