begin
theorem Th1:
theorem Th2:
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:
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :
theorem Th7:
theorem Th8:
:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :
theorem
canceled;
theorem
begin
theorem Th16:
:: deftheorem Def4 defines center WEDDWITT:def 4 :
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
definition
let R be
Skew-Field;
func VectSp_over_center R -> strict VectSp of
strict means :
Def6:
(
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
ex b1 being strict VectSp of strict 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 #) & 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 strict 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 #) & 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 ZeroF of b2 #) = addLoopStr(# the carrier of R,the addF of R,the ZeroF 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:
theorem Th33:
definition
let R be
Skew-Field;
let s be
Element of ;
func VectSp_over_center s -> strict VectSp of
strict means :
Def7:
(
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
ex b1 being strict VectSp of strict 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) #) & 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 strict 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) #) & 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 ZeroF of b2 #) = addLoopStr(# the carrier of (centralizer s),the addF of (centralizer s),the ZeroF 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:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
begin
theorem
theorem
theorem