let F be Field; for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being F -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))
let E be Polynom-Ring F -homomorphic FieldExtension of F; for a being F -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))
let a be F -algebraic Element of E; Base a is Basis of (VecSp ((FAdj (F,{a})),F))
set V = VecSp ((FAdj (F,{a})),F);
set ma = MinPoly (a,F);
H0:
F is Subring of E
by FIELD_4:def 1;
A:
now for l being Linear_Combination of Base a st Sum l = 0. (VecSp ((FAdj (F,{a})),F)) holds
Carrier l = {} let l be
Linear_Combination of
Base a;
( Sum l = 0. (VecSp ((FAdj (F,{a})),F)) implies Carrier l = {} )assume A1:
Sum l = 0. (VecSp ((FAdj (F,{a})),F))
;
Carrier l = {} 0. (VecSp ((FAdj (F,{a})),F)) =
0. (FAdj (F,{a}))
by FIELD_4:def 6
.=
0. E
by dFA
.=
0. F
by H0, C0SP1:def 3
;
then
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
by A1, lembas2;
hence
Carrier l = {}
by VECTSP_6:def 3;
verum end;
E:
now for o being object st o in the carrier of ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) holds
o in the carrier of (Lin (Base a))let o be
object ;
( o in the carrier of ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) implies o in the carrier of (Lin (Base a)) )assume
o in the
carrier of
ModuleStr(# the
carrier of
(VecSp ((FAdj (F,{a})),F)), the
addF of
(VecSp ((FAdj (F,{a})),F)), the
ZeroF of
(VecSp ((FAdj (F,{a})),F)), the
lmult of
(VecSp ((FAdj (F,{a})),F)) #)
;
o in the carrier of (Lin (Base a))then
o in the
carrier of
(FAdj (F,{a}))
by FIELD_4:def 6;
then
o in the
carrier of
(RAdj (F,{a}))
by ch1;
then
o in { (Ext_eval (p,a)) where p is Polynomial of F : verum }
by lemphi5;
then consider p being
Polynomial of
F such that A1:
o = Ext_eval (
p,
a)
;
o in Lin (Base a)
by A1, lembas1;
hence
o in the
carrier of
(Lin (Base a))
;
verum end;
then
Lin (Base a) = ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #)
by VECTSP_4:31, E, TARSKI:2;
hence
Base a is Basis of (VecSp ((FAdj (F,{a})),F))
by A, VECTSP_7:def 3, VECTSP_7:def 1; verum