:: Witt's Proof of the {W}edderburn Theorem
:: by Broderick Arneson , Matthias Baaz and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: WEDDWITT:1
for a being Element of NAT
for q being Real st 1 < q &amp; q |^ a = 1 holds
a = 0
proofend;

theorem Th2: :: WEDDWITT:2
for a, k, r being Nat
for x being Real st 1 < x &amp; 0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
proofend;

theorem Th3: :: WEDDWITT:3
for q, a, b being Element of NAT st 0 < a &amp; 1 < q &amp; (q |^ a) -' 1 divides (q |^ b) -' 1 holds
a divides b
proofend;

theorem Th4: :: WEDDWITT:4
for n, q being Nat st 0 < q holds
card (Funcs (n,q)) = q |^ n
proofend;

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

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 &amp; rng f = Y holds
for c being FinSequence of NAT st len c = len f &amp; ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c
proofend;

begin

registration
let G be finite Group;
cluster center G ->  finite ;
correctness
coherence
center G is finite ;
;
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
 ex b1 being strict Subgroup of G st the carrier of b1 =  {  b where b is Element of G : a * b = b * a  }
proofend;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 =  {  b where b is Element of G : a * b = b * a  }  &amp; the carrier of b2 =  {  b where b is Element of G : a * b = b * a  }  holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def_1_:_
 for G being Group
for a being Element of G
for b3 being strict Subgroup of G holds
( b3 = Centralizer a iff the carrier of b3 =  {  b where b is Element of G : a * b = b * a  }  );

registration
let G be finite Group;
let a be Element of G;
cluster Centralizer a ->  finite strict ;
correctness
coherence
Centralizer a is finite ;
;
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
proofend;

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

registration
let G be Group;
let a be Element of G;
cluster con_class a ->  non empty ;
correctness
coherence
not con_class a is empty ;
by GROUP_3:83;
end;

definition
let G be Group;
let a be Element of G;
funca -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
 ex b1 being Function of the carrier of G,(con_class a) st
for x being Element of G holds b1 . x = a |^ x
proofend;
uniqueness
 for b1, b2 being Function of the carrier of G,(con_class a) st ( for x being Element of G holds b1 . x = a |^ x ) &amp; ( for x being Element of G holds b2 . x = a |^ x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines -con_map WEDDWITT:def_2_:_
 for G being Group
for a being Element of G
for b3 being Function of the carrier of G,(con_class a) holds
( b3 = a -con_map iff for x being Element of G holds b3 . x = a |^ x );

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

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

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

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

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

definition
let G be Group;
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
coherence
{  (con_class a) where a is Element of G : verum  }  is a_partition of the carrier of G;
proofend;
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  }  ;

theorem :: WEDDWITT:14
for G being finite Group
for f being FinSequence of conjugate_Classes G st f is one-to-one &amp; rng f = conjugate_Classes G holds
for c being FinSequence of NAT st len c = len f &amp; ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card G = Sum c by Th6;

begin

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 &amp; n = dim V &amp; q = card the carrier of F holds
card the carrier of V = q |^ n
proofend;

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  }  &amp; the addF of it = the addF of R || the carrier of it &amp; the multF of it = the multF of R || the carrier of it &amp; 0. it = 0. R &amp; 1. it = 1. R );
existence
 ex b1 being strict Field st
( the carrier of b1 =  {  x where x is Element of R : for s being Element of R holds x * s = s * x  }  &amp; the addF of b1 = the addF of R || the carrier of b1 &amp; the multF of b1 = the multF of R || the carrier of b1 &amp; 0. b1 = 0. R &amp; 1. b1 = 1. R )
proofend;
uniqueness
 for b1, b2 being strict Field st the carrier of b1 =  {  x where x is Element of R : for s being Element of R holds x * s = s * x  }  &amp; the addF of b1 = the addF of R || the carrier of b1 &amp; the multF of b1 = the multF of R || the carrier of b1 &amp; 0. b1 = 0. R &amp; 1. b1 = 1. R &amp; the carrier of b2 =  {  x where x is Element of R : for s being Element of R holds x * s = s * x  }  &amp; the addF of b2 = the addF of R || the carrier of b2 &amp; the multF of b2 = the multF of R || the carrier of b2 &amp; 0. b2 = 0. R &amp; 1. b2 = 1. R holds
b1 = b2 ;
end;

:: deftheorem Def4 defines center WEDDWITT:def_4_:_
 for R being Skew-Field
for b2 being strict Field holds
( b2 = center R iff ( the carrier of b2 =  {  x where x is Element of R : for s being Element of R holds x * s = s * x  }  &amp; the addF of b2 = the addF of R || the carrier of b2 &amp; the multF of b2 = the multF of R || the carrier of b2 &amp; 0. b2 = 0. R &amp; 1. b2 = 1. R ) );

theorem Th16: :: WEDDWITT:16
for R being Skew-Field holds the carrier of (center R) c= the carrier of R
proofend;

registration
let R be finite Skew-Field;
cluster center R ->  finite strict ;
correctness
coherence
center R is finite ;
proofend;
end;

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

theorem Th18: :: WEDDWITT:18
for R being Skew-Field holds 0. R in center R
proofend;

theorem Th19: :: WEDDWITT:19
for R being Skew-Field holds 1_ R in center R
proofend;

theorem Th20: :: WEDDWITT:20
for R being finite Skew-Field holds 1 < card the carrier of (center R)
proofend;

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

theorem Th22: :: WEDDWITT:22
for R being Skew-Field holds the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}
proofend;

definition
let R be Skew-Field;
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  }  &amp; the addF of it = the addF of R || the carrier of it &amp; the multF of it = the multF of R || the carrier of it &amp; 0. it = 0. R &amp; 1. it = 1. R );
existence
 ex b1 being strict Skew-Field st
( the carrier of b1 =  {  x where x is Element of R : x * s = s * x  }  &amp; the addF of b1 = the addF of R || the carrier of b1 &amp; the multF of b1 = the multF of R || the carrier of b1 &amp; 0. b1 = 0. R &amp; 1. b1 = 1. R )
proofend;
uniqueness
 for b1, b2 being strict Skew-Field st the carrier of b1 =  {  x where x is Element of R : x * s = s * x  }  &amp; the addF of b1 = the addF of R || the carrier of b1 &amp; the multF of b1 = the multF of R || the carrier of b1 &amp; 0. b1 = 0. R &amp; 1. b1 = 1. R &amp; the carrier of b2 =  {  x where x is Element of R : x * s = s * x  }  &amp; the addF of b2 = the addF of R || the carrier of b2 &amp; the multF of b2 = the multF of R || the carrier of b2 &amp; 0. b2 = 0. R &amp; 1. b2 = 1. R holds
b1 = b2 ;
end;

:: deftheorem Def5 defines centralizer WEDDWITT:def_5_:_
 for R being Skew-Field
for s being Element of R
for b3 being strict Skew-Field holds
( b3 = centralizer s iff ( the carrier of b3 =  {  x where x is Element of R : x * s = s * x  }  &amp; the addF of b3 = the addF of R || the carrier of b3 &amp; the multF of b3 = the multF of R || the carrier of b3 &amp; 0. b3 = 0. R &amp; 1. b3 = 1. R ) );

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

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

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

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) &amp; b in the carrier of (centralizer s) holds
a * b in the carrier of (centralizer s)
proofend;

theorem Th27: :: WEDDWITT:27
for R being Skew-Field
for s being Element of R holds
( 0. R is Element of (centralizer s) &amp; 1_ R is Element of (centralizer s) )
proofend;

registration
let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s ->  finite strict ;
correctness
coherence
centralizer s is finite ;
by Th23, FINSET_1:1;
end;

theorem Th28: :: WEDDWITT:28
for R being finite Skew-Field
for s being Element of R holds 1 < card the carrier of (centralizer s)
proofend;

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

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

begin

definition
let R be Skew-Field;
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 #) &amp; the lmult of it = the multF of R | [: the carrier of (center R), the carrier of R:] );
existence
 ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) &amp; the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] )
proofend;
uniqueness
 for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) &amp; the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] &amp; addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) &amp; the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] holds
b1 = b2 ;
end;

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def_6_:_
 for R being Skew-Field
for b2 being strict VectSp of center R holds
( b2 = VectSp_over_center R iff ( addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) &amp; the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] ) );

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

theorem Th32: :: WEDDWITT:32
for R being finite Skew-Field holds 0 < dim (VectSp_over_center R)
proofend;

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
( 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) #) &amp; the lmult of it = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] );
existence
 ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) &amp; the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )
proofend;
uniqueness
 for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) &amp; the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] &amp; addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) &amp; the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] holds
b1 = b2 ;
end;

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def_7_:_
 for R being Skew-Field
for s being Element of R
for b3 being strict VectSp of center R holds
( b3 = VectSp_over_center s iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) &amp; the lmult of b3 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) );

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

theorem Th34: :: WEDDWITT:34
for R being finite Skew-Field
for s being Element of R holds 0 < dim (VectSp_over_center s)
proofend;

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

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

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

begin

:: [WP: ] Wedderburn_Theorem
theorem :: WEDDWITT:38
for R being finite Skew-Field holds R is commutative
proofend;

theorem :: WEDDWITT:39
for R being Skew-Field holds 1. (center R) = 1. R by Def4;

theorem :: WEDDWITT:40
for R being Skew-Field
for s being Element of R holds 1. (centralizer s) = 1. R by Def5;