:: by Broderick Arneson , Matthias Baaz and Piotr Rudnicki

::

:: Received December 30, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

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

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 Element of NAT st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b) -' 1 holds

a divides b

a divides b

proof end;

theorem Th5: :: WEDDWITT:5

for f being FinSequence of NAT

for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

for i being Element of NAT st ( for j being Element of 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 Element of NAT st i in dom c holds

c . i = card (f . i) ) holds

card X = Sum c

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 Element of NAT st i in dom c holds

c . i = card (f . i) ) holds

card X = Sum c

proof end;

registration
end;

definition

let G be Group;

let a be Element of G;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { b where b is Element of G : a * b = b * a }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { b where b is Element of G : a * b = b * a } & the carrier of b_{2} = { b where b is Element of G : a * b = b * a } holds

b_{1} = b_{2}

end;
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 the carrier of it = { b where b is Element of G : a * b = b * a } ;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :

for G being Group

for a being Element of G

for b_{3} being strict Subgroup of G holds

( b_{3} = Centralizer a iff the carrier of b_{3} = { b where b is Element of G : a * b = b * a } );

for G being Group

for a being Element of G

for b

( b

registration
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) )

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;

correctness

coherence

not con_class a is empty ;

by GROUP_3:83;

end;
let a be Element of G;

correctness

coherence

not con_class a is empty ;

by GROUP_3:83;

definition

let G be Group;

let a be Element of G;

ex b_{1} being Function of the carrier of G,(con_class a) st

for x being Element of G holds b_{1} . x = a |^ x

for b_{1}, b_{2} being Function of the carrier of G,(con_class a) st ( for x being Element of G holds b_{1} . x = a |^ x ) & ( for x being Element of G holds b_{2} . x = a |^ x ) holds

b_{1} = b_{2}

end;
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 for x being Element of G holds it . x = a |^ x;

ex b

for x being Element of G holds b

proof end;

uniqueness for b

b

proof end;

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

for G being Group

for a being Element of G

for b_{3} being Function of the carrier of G,(con_class a) holds

( b_{3} = a -con_map iff for x being Element of G holds b_{3} . x = a |^ x );

for G being Group

for a being Element of G

for b

( b

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}) = card (Centralizer a)

for a being Element of G

for x being Element of con_class a holds card ((a -con_map) " {x}) = card (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}

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

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)

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 card G = (card (con_class a)) * (card (Centralizer a))

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

proof end;

definition

let G be Group;

coherence

{ (con_class a) where a is Element of G : verum } is a_partition of the carrier of G;

end;
func conjugate_Classes G -> a_partition of the carrier of G equals :: WEDDWITT:def 3

{ (con_class a) where a is Element of G : verum } ;

correctness { (con_class a) where a is Element of G : verum } ;

coherence

{ (con_class a) where a is Element of G : verum } is a_partition of the carrier of G;

proof end;

:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :

for G being Group holds conjugate_Classes G = { (con_class a) where a is Element of G : verum } ;

for G being Group holds conjugate_Classes G = { (con_class a) where a is Element of G : verum } ;

theorem :: WEDDWITT:14

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 Element of NAT st i in dom c holds

c . i = card (f . i) ) holds

card G = Sum c by Th6;

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 Element of NAT st i in dom c holds

c . i = card (f . i) ) holds

card G = Sum c by Th6;

theorem Th15: :: WEDDWITT:15

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

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;

ex b_{1} being strict Field st

( the carrier of b_{1} = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b_{1} = the addF of R || the carrier of b_{1} & the multF of b_{1} = the multF of R || the carrier of b_{1} & 0. b_{1} = 0. R & 1. b_{1} = 1. R )

for b_{1}, b_{2} being strict Field st the carrier of b_{1} = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b_{1} = the addF of R || the carrier of b_{1} & the multF of b_{1} = the multF of R || the carrier of b_{1} & 0. b_{1} = 0. R & 1. b_{1} = 1. R & the carrier of b_{2} = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b_{2} = the addF of R || the carrier of b_{2} & the multF of b_{2} = the multF of R || the carrier of b_{2} & 0. b_{2} = 0. R & 1. b_{2} = 1. R holds

b_{1} = b_{2}
;

end;
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 addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );

existence ( the carrier of it = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines center WEDDWITT:def 4 :

for R being Skew-Field

for b_{2} being strict Field holds

( b_{2} = center R iff ( the carrier of b_{2} = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b_{2} = the addF of R || the carrier of b_{2} & the multF of b_{2} = the multF of R || the carrier of b_{2} & 0. b_{2} = 0. R & 1. b_{2} = 1. R ) );

for R being Skew-Field

for b

( b

theorem Th17: :: WEDDWITT:17

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 )

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 Th21: :: WEDDWITT:21

for R being finite Skew-Field holds

( card the carrier of (center R) = card the carrier of R iff R is commutative )

( card the carrier of (center R) = card the carrier of R iff R is commutative )

proof end;

theorem Th22: :: WEDDWITT:22

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;

A1: 1. R = 1_ R ;

ex b_{1} being strict Skew-Field st

( the carrier of b_{1} = { x where x is Element of R : x * s = s * x } & the addF of b_{1} = the addF of R || the carrier of b_{1} & the multF of b_{1} = the multF of R || the carrier of b_{1} & 0. b_{1} = 0. R & 1. b_{1} = 1. R )

for b_{1}, b_{2} being strict Skew-Field st the carrier of b_{1} = { x where x is Element of R : x * s = s * x } & the addF of b_{1} = the addF of R || the carrier of b_{1} & the multF of b_{1} = the multF of R || the carrier of b_{1} & 0. b_{1} = 0. R & 1. b_{1} = 1. R & the carrier of b_{2} = { x where x is Element of R : x * s = s * x } & the addF of b_{2} = the addF of R || the carrier of b_{2} & the multF of b_{2} = the multF of R || the carrier of b_{2} & 0. b_{2} = 0. R & 1. b_{2} = 1. R holds

b_{1} = b_{2}
;

end;
let s be Element of R;

A1: 1. R = 1_ 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 addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );

existence ( the carrier of it = { x where x is Element of R : x * s = s * x } & the addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :

for R being Skew-Field

for s being Element of R

for b_{3} being strict Skew-Field holds

( b_{3} = centralizer s iff ( the carrier of b_{3} = { x where x is Element of R : x * s = s * x } & the addF of b_{3} = the addF of R || the carrier of b_{3} & the multF of b_{3} = the multF of R || the carrier of b_{3} & 0. b_{3} = 0. R & 1. b_{3} = 1. R ) );

for R being Skew-Field

for s being Element of R

for b

( b

theorem Th23: :: WEDDWITT:23

for R being Skew-Field

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

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

proof end;

theorem Th24: :: WEDDWITT:24

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 )

for s, a being Element of R holds

( a in the carrier of (centralizer s) iff a * s = s * a )

proof end;

theorem :: WEDDWITT:25

for R being Skew-Field

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

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

proof end;

theorem Th26: :: WEDDWITT:26

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)

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 Th27: :: WEDDWITT:27

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

for s being Element of R holds

( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) )

proof end;

registration

let R be finite Skew-Field;

let s be Element of R;

correctness

coherence

centralizer s is finite ;

by Th23, FINSET_1:1;

end;
let s be Element of R;

correctness

coherence

centralizer s is finite ;

by Th23, FINSET_1:1;

theorem Th28: :: WEDDWITT:28

for R being finite Skew-Field

for s being Element of R holds 1 < card the carrier of (centralizer s)

for s being Element of R holds 1 < card the carrier of (centralizer s)

proof end;

theorem Th29: :: WEDDWITT:29

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

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 Th30: :: WEDDWITT:30

for R being finite Skew-Field

for s being Element of R

for t being Element of (MultGroup R) st t = s holds

card (Centralizer t) = (card the carrier of (centralizer s)) - 1

for s being Element of R

for t being Element of (MultGroup R) st t = s holds

card (Centralizer t) = (card the carrier of (centralizer s)) - 1

proof end;

definition

let R be Skew-Field;

ex b_{1} being strict VectSp of center R st

( addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b_{1} = the multF of R | [: the carrier of (center R), the carrier of R:] )

for b_{1}, b_{2} being strict VectSp of center R st addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b_{1} = the multF of R | [: the carrier of (center R), the carrier of R:] & addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b_{2} = the multF of R | [: the carrier of (center R), the carrier of R:] holds

b_{1} = b_{2}
;

end;
func VectSp_over_center R -> strict VectSp of center R means :Def6: :: WEDDWITT:def 6

( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of R:] );

existence ( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of R:] );

ex b

( addLoopStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def 6 :

for R being Skew-Field

for b_{2} being strict VectSp of center R holds

( b_{2} = VectSp_over_center R iff ( addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b_{2} = the multF of R | [: the carrier of (center R), the carrier of R:] ) );

for R being Skew-Field

for b

( b

theorem Th31: :: WEDDWITT:31

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;

definition

let R be Skew-Field;

let s be Element of R;

ex b_{1} being strict VectSp of center R st

( addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b_{1} = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )

for b_{1}, b_{2} being strict VectSp of center R st addLoopStr(# the carrier of b_{1}, the addF of b_{1}, the ZeroF of b_{1} #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b_{1} = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] & addLoopStr(# the carrier of b_{2}, the addF of b_{2}, the ZeroF of b_{2} #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b_{2} = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] holds

b_{1} = b_{2}
;

end;
let s be Element of R;

func VectSp_over_center s -> strict VectSp of center R means :Def7: :: WEDDWITT:def 7

( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] );

existence ( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] );

ex b

( addLoopStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :

for R being Skew-Field

for s being Element of R

for b_{3} being strict VectSp of center R holds

( b_{3} = VectSp_over_center s iff ( addLoopStr(# the carrier of b_{3}, the addF of b_{3}, the ZeroF of b_{3} #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b_{3} = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) );

for R being Skew-Field

for s being Element of R

for b

( b

theorem Th33: :: WEDDWITT:33

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

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 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

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 Th36: :: WEDDWITT:36

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)

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 Th37: :: WEDDWITT:37

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

proof end;

:: Wedderburn Theorem

theorem :: WEDDWITT:40