let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F)
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 Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F)
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 Element of E; :: thesis: for n being Element of NAT
for l being Linear_Combination of VecSp (E,F)
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 n be Element of NAT ; :: thesis: for l being Linear_Combination of VecSp (E,F)
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 VecSp (E,F); :: 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;
assume A: ( l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} ) ; :: thesis: Sum l = Ext_eval ((LM p),a)
reconsider LCp = LC p as Element of E by H2;
reconsider adegp = a |^ (deg p) as Element of E ;
reconsider v = a |^ (deg p) as Element of (VecSp (E,F)) by FIELD_4:def 6;
thus Sum l = (l . v) * v by A, VECTSP_6:20
.= LCp * adegp by A, Lm12a
.= Ext_eval ((LM p),a) by exevalLM ; :: thesis: verum