let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for l being Linear_Combination of Base a ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for l being Linear_Combination of Base a ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
let a be F -algebraic Element of E; :: thesis: for l being Linear_Combination of Base a ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
let l be Linear_Combination of Base a; :: thesis: ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
not deg (MinPoly (a,F)) <= 0 by RING_4:def 4;
then reconsider n = (deg (MinPoly (a,F))) - 1 as Element of NAT by INT_1:3;
E is FAdj (F,{a}) -extending by FIELD_4:7;
then B: VecSp ((FAdj (F,{a})),F) is Subspace of VecSp (E,F) by FIELD_5:14;
consider l2 being Linear_Combination of VecSp (E,F) such that
K: ( Carrier l2 = Carrier l & ( for v being Element of (VecSp (E,F)) st v in Carrier l2 holds
l2 . v = l . v ) ) by B, lcsub;
consider p being Polynomial of F such that
A: ( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l2 . (a |^ i) ) ) by lembasx2;
take p ; :: thesis: ( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
(deg p) + 0 < ((deg (MinPoly (a,F))) - 1) + 1 by A, XREAL_1:8;
hence deg p < deg (MinPoly (a,F)) ; :: thesis: for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i)

now :: thesis: for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i)

let i be Element of NAT ; :: thesis: ( i < deg (MinPoly (a,F)) implies p . i = l . (a |^ i) )
assume i < deg (MinPoly (a,F)) ; :: thesis: p . i = l . (a |^ i)
then i < n + 1 ;
then B: i <= n by NAT_1:13;
the carrier of (VecSp ((FAdj (F,{a})),F)) = the carrier of (FAdj (F,{a})) by FIELD_4:def 6;
then V1: a |^ i is Element of (VecSp ((FAdj (F,{a})),F)) by lcsub1;
V2: a |^ i is Element of (VecSp (E,F)) by FIELD_4:def 6;
thus p . i = l . (a |^ i) :: thesis: verum

proof

per cases ( a |^ i in Carrier l2 or not a |^ i in Carrier l2 ) ;

suppose a |^ i in Carrier l2 ; :: thesis: p . i = l . (a |^ i)

then l2 . (a |^ i) = l . (a |^ i) by K;
hence p . i = l . (a |^ i) by A, B; :: thesis: verum

end;

suppose C: not a |^ i in Carrier l2 ; :: thesis: p . i = l . (a |^ i)

then l2 . (a |^ i) = 0. F by V2, VECTSP_6:2
.= l . (a |^ i) by V1, C, K, VECTSP_6:2 ;
hence p . i = l . (a |^ i) by A, B; :: thesis: verum

end;

end;

end;

end;

hence for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ; :: thesis: verum