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
for 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) ) holds
Sum l = Ext_eval (p,a)
let E be FieldExtension of F; for a being F -algebraic Element of E
for l being Linear_Combination of Base a
for 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) ) holds
Sum l = Ext_eval (p,a)
let a be F -algebraic Element of E; for l being Linear_Combination of Base a
for 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) ) holds
Sum l = Ext_eval (p,a)
let l be Linear_Combination of Base a; for 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) ) holds
Sum l = Ext_eval (p,a)
let p be Polynomial of F; ( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) implies Sum l = Ext_eval (p,a) )
set V = VecSp ((FAdj (F,{a})),F);
assume AS:
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
; Sum l = Ext_eval (p,a)
defpred S1[ Nat] means for l being Linear_Combination of Base a st card (Carrier l) = $1 holds
for 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) ) holds
Sum l = Ext_eval (p,a);
IA:
S1[ 0 ]
proof
let l be
Linear_Combination of
Base a;
( card (Carrier l) = 0 implies for 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) ) holds
Sum l = Ext_eval (p,a) )
assume
card (Carrier l) = 0
;
for 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) ) holds
Sum l = Ext_eval (p,a)
then
Carrier l = {}
;
then A2:
l = ZeroLC (VecSp ((FAdj (F,{a})),F))
by VECTSP_6:def 3;
let p be
Polynomial of
F;
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) implies Sum l = Ext_eval (p,a) )
assume A4:
(
deg p < deg (MinPoly (a,F)) & ( for
i being
Element of
NAT st
i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )
;
Sum l = Ext_eval (p,a)
then
p = 0_. F
;
hence Ext_eval (
p,
a) =
0. E
by ALGNUM_1:13
.=
0. (FAdj (F,{a}))
by dFA
.=
0. (VecSp ((FAdj (F,{a})),F))
by FIELD_4:def 6
.=
Sum l
by A2, VECTSP_6:15
;
verum
end;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume B0:
S1[
k]
;
S1[k + 1]now for l being Linear_Combination of Base a st card (Carrier l) = k + 1 holds
for pp being Polynomial of F st deg pp < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
pp . i = l . (a |^ i) ) holds
Sum l = Ext_eval (pp,a)let l be
Linear_Combination of
Base a;
( card (Carrier l) = k + 1 implies for pp being Polynomial of F st deg pp < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
pp . i = l . (a |^ i) ) holds
Sum l = Ext_eval (pp,a) )assume B1:
card (Carrier l) = k + 1
;
for pp being Polynomial of F st deg pp < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
pp . i = l . (a |^ i) ) holds
Sum l = Ext_eval (pp,a)let pp be
Polynomial of
F;
( deg pp < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
pp . i = l . (a |^ i) ) implies Sum l = Ext_eval (pp,a) )assume B2:
(
deg pp < deg (MinPoly (a,F)) & ( for
i being
Element of
NAT st
i < deg (MinPoly (a,F)) holds
pp . i = l . (a |^ i) ) )
;
Sum l = Ext_eval (pp,a)then reconsider p =
pp as non
zero Polynomial of
F by UPROOTS:def 5;
defpred S2[
object ,
object ]
means ( ( $1
= a |^ (deg p) & $2
= LC p ) or ( $1
<> a |^ (deg p) & $2
= 0. F ) );
A:
for
x being
object st
x in the
carrier of
(VecSp ((FAdj (F,{a})),F)) holds
ex
y being
object st
(
y in the
carrier of
F &
S2[
x,
y] )
consider lp being
Function of the
carrier of
(VecSp ((FAdj (F,{a})),F)), the
carrier of
F such that L:
for
x being
object st
x in the
carrier of
(VecSp ((FAdj (F,{a})),F)) holds
S2[
x,
lp . x]
from FUNCT_2:sch 1(A);
reconsider lp =
lp as
Element of
Funcs ( the
carrier of
(VecSp ((FAdj (F,{a})),F)), the
carrier of
F)
by FUNCT_2:8;
for
v being
Element of
(VecSp ((FAdj (F,{a})),F)) st not
v in Base a holds
lp . v = 0. F
then reconsider lp =
lp as
Linear_Combination of
VecSp (
(FAdj (F,{a})),
F)
by VECTSP_6:def 1;
then
Carrier lp c= Base a
;
then reconsider lp =
lp as
Linear_Combination of
Base a by VECTSP_6:def 4;
X1:
{a} is
Subset of
(FAdj (F,{a}))
by FAt;
a in {a}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of the
carrier of
(FAdj (F,{a})) by X1;
FAdj (
F,
{a}) is
Subring of
E
by FIELD_5:12;
then
a |^ (deg p) = a1 |^ (deg p)
by pr5;
then X:
a |^ (deg p) is
Element of
(VecSp ((FAdj (F,{a})),F))
by FIELD_4:def 6;
C0:
Carrier lp = {(a |^ (deg p))}
lp . (a |^ (deg p)) = LC p
by X, L;
then C:
Ext_eval (
(LM p),
a)
= Sum lp
by C0, lembas2bb;
set q =
p - (LM p);
reconsider lk =
l - lp as
Linear_Combination of
Base a by VECTSP_6:42;
C2:
l = lk + lp
C3:
Carrier lk = (Carrier l) \ (Carrier lp)
then
Carrier lp c= Carrier l
;
then A:
card ((Carrier l) \ (Carrier lp)) =
(card (Carrier l)) - (card (Carrier lp))
by CARD_2:44
.=
(k + 1) - 1
by B1, C0, CARD_2:42
;
B:
deg (p - (LM p)) < deg (MinPoly (a,F))
by thdLM, B2, XXREAL_0:2;
for
i being
Element of
NAT st
i < deg (MinPoly (a,F)) holds
(p - (LM p)) . i = lk . (a |^ i)
then D:
Ext_eval (
(p - (LM p)),
a)
= Sum lk
by A, C3, B, B0;
(
Sum lk in the
carrier of
(VecSp ((FAdj (F,{a})),F)) &
Sum lp in the
carrier of
(VecSp ((FAdj (F,{a})),F)) )
;
then
(
Sum lk in the
carrier of
(FAdj (F,{a})) &
Sum lp in the
carrier of
(FAdj (F,{a})) )
by FIELD_4:def 6;
then
(
Sum lk in carrierFA {a} &
Sum lp in carrierFA {a} )
by dFA;
then E:
[(Sum lk),(Sum lp)] in [:(carrierFA {a}),(carrierFA {a}):]
by ZFMISC_1:def 2;
thus Sum l =
(Sum lk) + (Sum lp)
by C2, VECTSP_6:44
.=
the
addF of
(FAdj (F,{a})) . (
(Sum lk),
(Sum lp))
by FIELD_4:def 6
.=
( the addF of E || (carrierFA {a})) . (
(Sum lk),
(Sum lp))
by dFA
.=
the
addF of
E . (
(Sum lk),
(Sum lp))
by E, FUNCT_1:49
.=
((Ext_eval (p,a)) - (Ext_eval ((LM p),a))) + (Ext_eval ((LM p),a))
by C, D, exevalminus2
.=
(Ext_eval (p,a)) + ((- (Ext_eval ((LM p),a))) + (Ext_eval ((LM p),a)))
by RLVECT_1:def 3
.=
(Ext_eval (p,a)) + (0. E)
by RLVECT_1:5
.=
Ext_eval (
pp,
a)
;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H:
card (Carrier l) = n
;
thus
Sum l = Ext_eval (p,a)
by AS, I, H; verum