let F be Field; for E being FieldExtension of F
for a being F -algebraic Element of E
for l being Linear_Combination of Base a st Sum l = 0. F holds
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
let E be FieldExtension of F; for a being F -algebraic Element of E
for l being Linear_Combination of Base a st Sum l = 0. F holds
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
let a be F -algebraic Element of E; for l being Linear_Combination of Base a st Sum l = 0. F holds
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
let l be Linear_Combination of Base a; ( Sum l = 0. F implies l = ZeroLC (VecSp ((FAdj (F,{a})),F)) )
assume AS:
Sum l = 0. F
; l = ZeroLC (VecSp ((FAdj (F,{a})),F))
set V = VecSp ((FAdj (F,{a})),F);
set ma = MinPoly (a,F);
H:
F is Subring of E
by FIELD_4:def 1;
consider p being Polynomial of F such that
A2:
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
by lembas2a;
now not Carrier l <> {} assume A3:
Carrier l <> {}
;
contradictionset x = the
Element of
Carrier l;
consider v being
Element of
(VecSp ((FAdj (F,{a})),F)) such that A5:
( the
Element of
Carrier l = v &
l . v <> 0. F )
by A3, VECTSP_6:1;
Carrier l c= Base a
by VECTSP_6:def 4;
then
v in Base a
by A3, A5;
then consider i being
Element of
NAT such that A6:
(
v = a |^ i &
i < deg (MinPoly (a,F)) )
;
p . i <> 0. F
by A2, A6, A5;
then
p <> 0_. F
;
then reconsider p =
p as non
zero Polynomial of
F by UPROOTS:def 5;
reconsider pp =
p as non
zero Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
Ext_eval (
pp,
a) =
0. F
by A2, AS, lembas2b
.=
0. E
by H, C0SP1:def 3
;
hence
contradiction
by mpol4, A2, RING_5:13;
verum end;
hence
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
by VECTSP_6:def 3; verum