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 non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM 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 non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)
let a be F -algebraic Element of E; :: thesis: for l being Linear_Combination of Base a
for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)
let l be Linear_Combination of Base a; :: thesis: for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)
let p be non zero Polynomial of F; :: thesis: ( l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} implies Sum l = Ext_eval ((LM p),a) )
F is Subring of E by FIELD_4:def 1;
then H2: the carrier of F c= the carrier of E by C0SP1:def 3;
H3: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of (FAdj (F,{a})) by H3;
H7: FAdj (F,{a}) is Subring of E by FIELD_5:12;
assume A: ( l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} ) ; :: thesis: Sum l = Ext_eval ((LM p),a)
reconsider LCpE = LC p as Element of E by H2;
F is Subfield of FAdj (F,{a}) by FAsub;
then the carrier of F c= the carrier of (FAdj (F,{a})) by EC_PF_1:def 1;
then reconsider LCp = LC p as Element of (FAdj (F,{a})) ;
reconsider degp = deg p as Nat ;
H8: a |^ degp = a1 |^ degp by H7, pr5;
then reconsider adegp = a |^ (deg p) as Element of (FAdj (F,{a})) ;
reconsider v = a |^ (deg p) as Element of (VecSp ((FAdj (F,{a})),F)) by H8, FIELD_4:def 6;
B: E is FieldExtension of FAdj (F,{a}) by FIELD_4:7;
Sum l = (l . v) * v by A, VECTSP_6:20
.= LCp * adegp by A, Lm12a
.= LCpE * (a |^ (deg p)) by B, Lm12b
.= Ext_eval ((LM p),a) by exevalLM ;
hence Sum l = Ext_eval ((LM p),a) ; :: thesis: verum