let F be Field; for p being irreducible Element of the carrier of (Polynom-Ring F)
for f being Element of the carrier of (Polynom-Ring F) holds eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
let p be irreducible Element of the carrier of (Polynom-Ring F); for f being Element of the carrier of (Polynom-Ring F) holds eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
let f be Element of the carrier of (Polynom-Ring F); eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
set LMf = Leading-Monomial f;
set LMfe = Leading-Monomial (emb (f,p));
set z = KrRoot p;
set E = KroneckerField (F,p);
set efp = emb (f,p);
set n = (len (emb (f,p))) -' 1;
per cases
( f = 0_. F or f <> 0_. F )
;
suppose A1:
f = 0_. F
;
eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))then
emb (
f,
p)
= 0_. (KroneckerField (F,p))
by Th23;
then
Leading-Monomial (emb (f,p)) = 0_. (KroneckerField (F,p))
by POLYNOM4:13;
then A2:
eval (
(Leading-Monomial (emb (f,p))),
(KrRoot p)) =
0. (KroneckerField (F,p))
by POLYNOM4:17
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(0. (Polynom-Ring F)))
by RING_1:def 6
;
0. (Polynom-Ring F) = 0_. F
by POLYNOM3:def 10;
hence
eval (
(LM (emb (f,p))),
(KrRoot p))
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(LM f))
by A1, A2, POLYNOM4:13;
verum end; suppose
f <> 0_. F
;
eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))then reconsider f1 =
f as non
zero Polynomial of
F by UPROOTS:def 5;
reconsider fnF =
(f . ((len (emb (f,p))) -' 1)) | F as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider x =
<%(0. F),(1. F)%> as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
A3:
(emb (f,p)) . ((len (emb (f,p))) -' 1) = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
((f . ((len (emb (f,p))) -' 1)) | F))
by Th41;
A4:
(power (KroneckerField (F,p))) . (
(KrRoot p),
((len (emb (f,p))) -' 1)) =
(KrRoot p) |^ ((len (emb (f,p))) -' 1)
by BINOM:def 2
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(x |^ ((len (emb (f,p))) -' 1)))
by Th3
;
set a =
f . ((len (emb (f,p))) -' 1);
A5:
deg f =
deg (emb (f,p))
by Th32
.=
(len (emb (f,p))) - 1
;
then A6:
(len (emb (f,p))) -' 1
= deg f1
by XREAL_0:def 2;
not
LC f1 is
zero
;
then A7:
not
f . ((len (emb (f,p))) -' 1) is
zero
by A5, RATFUNC1:def 6;
x |^ ((len (emb (f,p))) -' 1) =
(power (Polynom-Ring F)) . (
<%(0. F),(1. F)%>,
((len (emb (f,p))) -' 1))
by BINOM:def 2
.=
<%(0. F),(1. F)%> `^ ((len (emb (f,p))) -' 1)
by POLYNOM5:def 3
.=
anpoly (
(1. F),
((len (emb (f,p))) -' 1))
by Th13
;
then A8:
fnF * (x |^ ((len (emb (f,p))) -' 1)) =
(anpoly ((f . ((len (emb (f,p))) -' 1)),0)) *' (anpoly ((1. F),((len (emb (f,p))) -' 1)))
by POLYNOM3:def 10
.=
anpoly (
((f . ((len (emb (f,p))) -' 1)) * (1. F)),
(0 + ((len (emb (f,p))) -' 1)))
by A7, Th11
.=
LM f
by A6, Th12
;
thus eval (
(Leading-Monomial (emb (f,p))),
(KrRoot p)) =
((emb (f,p)) . ((len (emb (f,p))) -' 1)) * ((power (KroneckerField (F,p))) . ((KrRoot p),((len (emb (f,p))) -' 1)))
by POLYNOM4:22
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(Leading-Monomial f))
by A8, A3, A4, RING_1:14
;
verum end;