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
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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: 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) ) 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) ) ) ; :: thesis: Sum l = Ext_eval (p,a)
defpred S₁[ 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: S₁[ 0 ]

proof

let l be Linear_Combination of Base a; :: thesis: ( 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 ; :: thesis: 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; :: 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) ) 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) ) ) ; :: thesis: Sum l = Ext_eval (p,a)

now :: thesis: for i being Element of NAT holds p . i = (0_. F) . i

let i be Element of NAT ; :: thesis: p . b₁ = (0_. F) . b₁

per cases ( i >= deg (MinPoly (a,F)) or i < deg (MinPoly (a,F)) ) ;

suppose i >= deg (MinPoly (a,F)) ; :: thesis: p . b₁ = (0_. F) . b₁

then A5: i > deg p by A4, XXREAL_0:2;
deg p = (len p) - 1 by HURWITZ:def 2;
then i + 1 > ((len p) - 1) + 1 by A5, XREAL_1:6;
hence p . i = (0_. F) . i by NAT_1:13, ALGSEQ_1:8; :: thesis: verum

end;

suppose A5: i < deg (MinPoly (a,F)) ; :: thesis: p . b₁ = (0_. F) . b₁

then a |^ i in Base a ;
then reconsider v = a |^ i as Element of (VecSp ((FAdj (F,{a})),F)) ;
thus p . i = l . v by A4, A5
.= (0_. F) . i by A2, VECTSP_6:3 ; :: thesis: verum

end;

end;

end;

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 ;
:: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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) ) ) ; :: thesis: Sum l = Ext_eval (pp,a)

now :: thesis: not pp = 0_. F

assume C0: pp = 0_. F ; :: thesis: contradiction

now :: thesis: for o being object holds not o in Carrier l

let o be object ; :: thesis: not o in Carrier l
assume C1: o in Carrier l ; :: thesis: contradiction
Carrier l c= Base a by VECTSP_6:def 4;
then o in Base a by C1;
then consider n being Element of NAT such that
C2: ( o = a |^ n & n < deg (MinPoly (a,F)) ) ;
l . (a |^ n) = pp . n by B2, C2
.= 0. F by C0 ;
hence contradiction by C1, C2, VECTSP_6:2; :: thesis: verum

end;

then Carrier l = {} by XBOOLE_0:def 1;
hence contradiction by B1; :: thesis: verum

end;

then reconsider p = pp as non zero Polynomial of F by UPROOTS:def 5;
defpred S₂[ 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 & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (VecSp ((FAdj (F,{a})),F)) implies ex y being object st
( y in the carrier of F & S₂[x,y] ) )
assume x in the carrier of (VecSp ((FAdj (F,{a})),F)) ; :: thesis: ex y being object st
( y in the carrier of F & S₂[x,y] )

per cases ( x = a |^ (deg p) or x <> a |^ (deg p) ) ;

suppose x = a |^ (deg p) ; :: thesis: ex y being object st
( y in the carrier of F & S₂[x,y] )

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis: verum

end;

suppose x <> a |^ (deg p) ; :: thesis: ex y being object st
( y in the carrier of F & S₂[x,y] )

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis: verum

end;

end;

end;

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
S₂[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

proof

let v be Element of (VecSp ((FAdj (F,{a})),F)); :: thesis: ( not v in Base a implies lp . v = 0. F )
assume not v in Base a ; :: thesis: lp . v = 0. F
then v <> a |^ (deg p) by B2;
hence lp . v = 0. F by L; :: thesis: verum

end;

then reconsider lp = lp as Linear_Combination of VecSp ((FAdj (F,{a})),F) by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier lp holds
o in Base a

let o be object ; :: thesis: ( o in Carrier lp implies o in Base a )
assume o in Carrier lp ; :: thesis: o in Base a
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
A1: ( o = v & lp . v <> 0. F ) by VECTSP_6:1;
( v = a |^ (deg p) & lp . v = LC p ) by L, A1;
hence o in Base a by A1, B2; :: thesis: verum

end;

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))}

proof

C2: now :: thesis: for o being object st o in {(a |^ (deg p))} holds
o in Carrier lp

let o be object ; :: thesis: ( o in {(a |^ (deg p))} implies o in Carrier lp )
assume o in {(a |^ (deg p))} ; :: thesis: o in Carrier lp
then C3: o = a |^ (deg p) by TARSKI:def 1;
then lp . o <> 0. F by X, L;
hence o in Carrier lp by X, C3, VECTSP_6:2; :: thesis: verum

end;

now :: thesis: for o being object st o in Carrier lp holds
o in {(a |^ (deg p))}

let o be object ; :: thesis: ( o in Carrier lp implies o in {(a |^ (deg p))} )
assume C3: o in Carrier lp ; :: thesis: o in {(a |^ (deg p))}
Carrier lp = { v where v is Element of (VecSp ((FAdj (F,{a})),F)) : lp . v <> 0. F } by VECTSP_6:def 2;
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
C4: ( o = v & lp . v <> 0. F ) by C3;
o = a |^ (deg p) by C4, L;
hence o in {(a |^ (deg p))} by TARSKI:def 1; :: thesis: verum

end;

hence Carrier lp = {(a |^ (deg p))} by C2, TARSKI:2; :: thesis: verum

end;

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

proof

thus lk + lp = (l + (- lp)) + lp by VECTSP_6:def 11
.= l + ((- lp) + lp) by VECTSP_6:26
.= l + (lp + (- lp)) by VECTSP_6:25
.= l + (lp - lp) by VECTSP_6:def 11
.= l + (ZeroLC (VecSp ((FAdj (F,{a})),F))) by VECTSP_6:43
.= l by VECTSP_6:27 ; :: thesis: verum

end;

C3: Carrier lk = (Carrier l) \ (Carrier lp)

proof

C4: now :: thesis: for o being object st o in Carrier lk holds
o in (Carrier l) \ (Carrier lp)

let o be object ; :: thesis: ( o in Carrier lk implies o in (Carrier l) \ (Carrier lp) )
assume o in Carrier lk ; :: thesis: o in (Carrier l) \ (Carrier lp)
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
C5: ( o = v & lk . v <> 0. F ) by VECTSP_6:1;

C6: now :: thesis: not v = a |^ (deg p)

assume C7: v = a |^ (deg p) ; :: thesis: contradiction
then C9: l . v = p . (deg p) by B2
.= LC p by thLC ;
lk . v = (l . v) - (lp . v) by VECTSP_6:40
.= (LC p) - (LC p) by L, C7, C9 ;
hence contradiction by C5, RLVECT_1:15; :: thesis: verum

end;

then C7: not v in Carrier lp by C0, TARSKI:def 1;
lk . v = (l . v) - (lp . v) by VECTSP_6:40
.= (l . v) - (0. F) by C6, L ;
then v in Carrier l by C5, VECTSP_6:2;
hence o in (Carrier l) \ (Carrier lp) by C7, C5, XBOOLE_0:def 5; :: thesis: verum

end;

now :: thesis: for o being object st o in (Carrier l) \ (Carrier lp) holds
o in Carrier lk

let o be object ; :: thesis: ( o in (Carrier l) \ (Carrier lp) implies o in Carrier lk )
assume o in (Carrier l) \ (Carrier lp) ; :: thesis: o in Carrier lk
then C5: ( o in Carrier l & not o in Carrier lp ) by XBOOLE_0:def 5;
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
C6: ( o = v & l . v <> 0. F ) by VECTSP_6:1;
C7: o <> a |^ (deg p) by C0, C5, TARSKI:def 1;
lk . v = (l . v) - (lp . v) by VECTSP_6:40
.= (l . v) - (0. F) by C6, C7, L ;
hence o in Carrier lk by C6, VECTSP_6:1; :: thesis: verum

end;

hence Carrier lk = (Carrier l) \ (Carrier lp) by C4, TARSKI:2; :: thesis: verum

end;

now :: thesis: for o being object st o in Carrier lp holds
o in Carrier l

let o be object ; :: thesis: ( o in Carrier lp implies o in Carrier l )
assume C5: o in Carrier lp ; :: thesis: o in Carrier l
then C4: o = a |^ (deg p) by C0, TARSKI:def 1;
reconsider v = o as Element of (VecSp ((FAdj (F,{a})),F)) by C5;
lp . v = LC p by L, C4
.= pp . (deg p) by thLC
.= l . v by C4, B2 ;
then l . v <> 0. F by C5, VECTSP_6:2;
hence o in Carrier l by VECTSP_6:2; :: thesis: verum

end;

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)

proof

let i be Element of NAT ; :: thesis: ( i < deg (MinPoly (a,F)) implies (p - (LM p)) . i = lk . (a |^ i) )
assume B1: i < deg (MinPoly (a,F)) ; :: thesis: (p - (LM p)) . i = lk . (a |^ i)
FAdj (F,{a}) is Subring of E by FIELD_5:12;
then a |^ i = a1 |^ i by pr5;
then reconsider v = a |^ i as Element of (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6;

per cases ( i = deg p or i <> deg p ) ;

suppose B3: i = deg p ; :: thesis: (p - (LM p)) . i = lk . (a |^ i)

hence (p - (LM p)) . i = (p . (deg p)) - ((LM p) . (deg p)) by POLYNOM3:27
.= (p . (deg p)) - ((LM p) . (deg (LM p))) by thdegLM
.= (l . v) - ((LM p) . (deg (LM p))) by B3, B2
.= (l . v) - (LC (LM p)) by thLC
.= (l . v) - (LC p) by thdegLC
.= (l . v) - (lp . v) by B3, L
.= lk . (a |^ i) by VECTSP_6:40 ;
:: thesis: verum

end;

suppose D2: i <> deg p ; :: thesis: (p - (LM p)) . i = lk . (a |^ i)

D3: a |^ i <> a |^ (deg p)

proof

per cases ( i < deg p or i > deg p ) by D2, XXREAL_0:1;

suppose i < deg p ; :: thesis: a |^ i <> a |^ (deg p)

hence a |^ i <> a |^ (deg p) by B2, mpol5; :: thesis: verum

end;

suppose i > deg p ; :: thesis: a |^ i <> a |^ (deg p)

hence a |^ i <> a |^ (deg p) by B1, mpol5; :: thesis: verum

end;

end;

end;

p <> 0_. F ;
then len p <> 0 by POLYNOM4:5;
then (len p) + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then D5: (len p) -' 1 = (len p) - 1 by XREAL_0:def 2;
D4: i <> (len p) -' 1 by D5, D2, HURWITZ:def 2;
thus (p - (LM p)) . i = (p . i) - ((LM p) . i) by POLYNOM3:27
.= (p . i) - (0. F) by D4, POLYNOM4:def 1
.= (l . v) - (0. F) by B2, B1
.= (l . v) - (lp . v) by D3, L
.= lk . (a |^ i) by VECTSP_6:40 ; :: thesis: verum

end;

end;

end;

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) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[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; :: thesis: verum