:: Witt's Proof of the {W}edderburn Theorem
:: by Broderick Arneson , Matthias Baaz and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: WEDDWITT:1
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))
theorem Th3: :: WEDDWITT:3
theorem Th4: :: WEDDWITT:4
theorem Th5: :: WEDDWITT:5
theorem Th6: :: WEDDWITT:6
:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :
theorem Th7: :: WEDDWITT:7
theorem Th8: :: WEDDWITT:8
:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :
theorem Th9: :: WEDDWITT:9
theorem Th10: :: WEDDWITT:10
theorem Th11: :: WEDDWITT:11
theorem Th12: :: WEDDWITT:12
theorem Th13: :: WEDDWITT:13
:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :
theorem :: WEDDWITT:14
canceled;
theorem :: WEDDWITT:15
theorem Th16: :: WEDDWITT:16
:: deftheorem Def4 defines center WEDDWITT:def 4 :
theorem Th17: :: WEDDWITT:17
theorem Th18: :: WEDDWITT:18
theorem Th19: :: WEDDWITT:19
theorem Th20: :: WEDDWITT:20
theorem Th21: :: WEDDWITT:21
theorem Th22: :: WEDDWITT:22
theorem Th23: :: WEDDWITT:23
:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :
theorem Th24: :: WEDDWITT:24
theorem Th25: :: WEDDWITT:25
theorem :: WEDDWITT:26
theorem Th27: :: WEDDWITT:27
theorem Th28: :: WEDDWITT:28
theorem Th29: :: WEDDWITT:29
theorem Th30: :: WEDDWITT:30
theorem Th31: :: WEDDWITT:31
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
U2 of
it #)
= addLoopStr(# the
carrier of
R,the
addF of
R,the
U2 of
R #) & 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 U2 of b1 #) = addLoopStr(# the carrier of R,the addF of R,the U2 of R #) & the lmult of b1 = the multF of R | [:the carrier of (center R),the carrier of R:] )
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1,the addF of b1,the U2 of b1 #) = addLoopStr(# the carrier of R,the addF of R,the U2 of R #) & the lmult of b1 = the multF of R | [:the carrier of (center R),the carrier of R:] & addLoopStr(# the carrier of b2,the addF of b2,the U2 of b2 #) = addLoopStr(# the carrier of R,the addF of R,the U2 of R #) & 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 :
theorem Th32: :: WEDDWITT:32
theorem Th33: :: WEDDWITT:33
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
U2 of
it #)
= addLoopStr(# the
carrier of
(centralizer s),the
addF of
(centralizer s),the
U2 of
(centralizer s) #) & 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 U2 of b1 #) = addLoopStr(# the carrier of (centralizer s),the addF of (centralizer s),the U2 of (centralizer s) #) & the lmult of b1 = the multF of R | [:the carrier of (center R),the carrier of (centralizer s):] )
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1,the addF of b1,the U2 of b1 #) = addLoopStr(# the carrier of (centralizer s),the addF of (centralizer s),the U2 of (centralizer s) #) & the lmult of b1 = the multF of R | [:the carrier of (center R),the carrier of (centralizer s):] & addLoopStr(# the carrier of b2,the addF of b2,the U2 of b2 #) = addLoopStr(# the carrier of (centralizer s),the addF of (centralizer s),the U2 of (centralizer s) #) & 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 :
theorem Th34: :: WEDDWITT:34
theorem Th35: :: WEDDWITT:35
theorem Th36: :: WEDDWITT:36
theorem Th37: :: WEDDWITT:37
theorem Th38: :: WEDDWITT:38
theorem :: WEDDWITT:39
theorem :: WEDDWITT:40
theorem :: WEDDWITT:41