let F be Field; :: thesis: for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (m,p))))
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)); :: thesis: for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (m,p))))
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (m,p))))
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (m,p))))
let o be Ordinal; :: thesis: ( o in card (nonConstantPolys F) implies eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,o))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (o,p)))) )
assume A0: o in card (nonConstantPolys F) ; :: thesis: eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,o))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (o,p))))
set m = card (nonConstantPolys F);
set LMf = Leading-Monomial p;
set LMfe = Leading-Monomial ((PolyHom (emb (F,I,g))) . p);
set z = KrRoot (I,o);
set E = KroneckerField (F,g,I);
set efp = (PolyHom (emb (F,I,g))) . p;
set n = (len ((PolyHom (emb (F,I,g))) . p)) -' 1;
reconsider f1 = p as non zero Polynomial of F ;
reconsider fnF = (p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) | ((card (nonConstantPolys F)),F) as Element of the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
reconsider x = Poly (o,<%(0. F),(1. F)%>) as Element of the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
A3: ((PolyHom (emb (F,I,g))) . p) . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) | ((card (nonConstantPolys F)),F))) by TH40;
A4: (power (KroneckerField (F,g,I))) . ((KrRoot (I,o)),((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) = (KrRoot (I,o)) |^ ((len ((PolyHom (emb (F,I,g))) . p)) -' 1) by BINOM:def 2
.= Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(x |^ ((len ((PolyHom (emb (F,I,g))) . p)) -' 1))) by FIELD_1:2 ;
set a = p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1);
I: deg p = deg ((PolyHom (emb (F,I,g))) . p) by FIELD_1:31;
H: ( deg p = (len p) - 1 & deg ((PolyHom (emb (F,I,g))) . p) = (len ((PolyHom (emb (F,I,g))) . p)) - 1 ) by HURWITZ:def 2;
( deg p > 0 & deg ((PolyHom (emb (F,I,g))) . p) > 0 ) by I, RING_4:def 4;
then ( (len ((PolyHom (emb (F,I,g))) . p)) - 1 > 0 & (len p) - 1 > 0 ) by HURWITZ:def 2;
then J: ( (len p) - 1 = (len p) -' 1 & (len ((PolyHom (emb (F,I,g))) . p)) - 1 = (len ((PolyHom (emb (F,I,g))) . p)) -' 1 ) by XREAL_0:def 2;
A1: (len ((PolyHom (emb (F,I,g))) . p)) -' 1 = deg p by H, J, FIELD_1:31;
A2: p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1) = LC p by H, I, RATFUNC1:def 6;
A8: fnF = Poly (o,((p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) | F)) by A0, XYZbb
.= Poly (o,(anpoly ((p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)),0))) by FIELD_1:7 ;
x |^ ((len ((PolyHom (emb (F,I,g))) . p)) -' 1) = (power (Polynom-Ring ((card (nonConstantPolys F)),F))) . ((Poly (o,<%(- (0. F)),(1. F)%>)),((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) by BINOM:def 2
.= (power (Polynom-Ring ((card (nonConstantPolys F)),F))) . ((Poly (o,(rpoly (1,(0. F))))),((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) by RING_5:10
.= (power (Polynom-Ring ((card (nonConstantPolys F)),F))) . ((Poly (o,(anpoly ((1. F),1)))),((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) by FIELD_1:8
.= Poly (o,(anpoly ((1. F),((len ((PolyHom (emb (F,I,g))) . p)) -' 1)))) by A0, Th13 ;
then A9: fnF * (x |^ ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) = (Poly (o,(anpoly ((p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)),0)))) *' (Poly (o,(anpoly ((1. F),((len ((PolyHom (emb (F,I,g))) . p)) -' 1))))) by A8, POLYNOM1:def 11
.= Poly (o,(anpoly (((p . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) * (1. F)),(0 + ((len ((PolyHom (emb (F,I,g))) . p)) -' 1))))) by A0, A2, Th11
.= LM (Poly (o,p)) by A0, A2, A1, Th12 ;
eval ((Leading-Monomial ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,o))) = (((PolyHom (emb (F,I,g))) . p) . ((len ((PolyHom (emb (F,I,g))) . p)) -' 1)) * ((power (KroneckerField (F,g,I))) . ((KrRoot (I,o)),((len ((PolyHom (emb (F,I,g))) . p)) -' 1))) by POLYNOM4:22;
hence eval ((Leading-Monomial ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,o))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (o,p)))) by A9, A4, A3, RING_1:14; :: thesis: verum