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 ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),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 ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
let f be Element of the carrier of (Polynom-Ring F); eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
set z = KrRoot p;
set E = KroneckerField (F,p);
set h = canHom (emb p);
defpred S1[ Nat] means for f being Element of the carrier of (Polynom-Ring F) st len f = $1 holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f);
A1:
now for f being Element of the carrier of (Polynom-Ring F) st len f = 0 holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)let f be
Element of the
carrier of
(Polynom-Ring F);
( len f = 0 implies eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f) )assume
len f = 0
;
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)then
f = 0_. F
by POLYNOM4:5;
then A2:
f = 0. (Polynom-Ring F)
by POLYNOM3:def 10;
0_. (KroneckerField (F,p)) =
0. (Polynom-Ring (KroneckerField (F,p)))
by POLYNOM3:def 10
.=
emb (
f,
p)
by A2, RING_2:6
;
hence eval (
(emb (f,p)),
(KrRoot p)) =
0. (KroneckerField (F,p))
by POLYNOM4:17
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
f)
by A2, RING_1:def 6
;
verum end;
A3:
now for k being Nat st ( for m being Nat st m < k holds
S1[m] ) holds
S1[k]let k be
Nat;
( ( for m being Nat st m < k holds
S1[m] ) implies S1[k] )assume A4:
for
m being
Nat st
m < k holds
S1[
m]
;
S1[k]now for f being Element of the carrier of (Polynom-Ring F) st len f = k holds
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)let f be
Element of the
carrier of
(Polynom-Ring F);
( len f = k implies eval ((emb (b1,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1) )assume A5:
len f = k
;
eval ((emb (b1,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1)per cases
( k = 0 or k > 0 )
;
suppose
k > 0
;
eval ((emb (b1,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1)then consider q being
Polynomial of
F such that A6:
(
len q < len f &
f = q + (Leading-Monomial f) & ( for
n being
Element of
NAT st
n < (len f) - 1 holds
q . n = f . n ) )
by A5, POLYNOM4:16;
reconsider g =
q as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider LMf =
LM f as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider r1 =
emb (
LMf,
p),
r2 =
emb (
g,
p) as
Polynomial of
(KroneckerField (F,p)) ;
A7:
emb (
(LMf + g),
p) =
(emb (LMf,p)) + (emb (g,p))
by VECTSP_1:def 20
.=
r1 + r2
by POLYNOM3:def 10
;
Leading-Monomial (emb (f,p)) = emb (
LMf,
p)
by Th33;
then A8:
eval (
(emb (LMf,p)),
(KrRoot p))
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
LMf)
by Lm5;
A9:
eval (
(emb (g,p)),
(KrRoot p))
= Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
g)
by A6, A5, A4;
A10:
(eval ((emb (LMf,p)),(KrRoot p))) + (eval ((emb (g,p)),(KrRoot p))) =
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
(LMf + g))
by A9, A8, RING_1:13
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
f)
by A6, POLYNOM3:def 10
;
thus eval (
(emb (f,p)),
(KrRoot p)) =
eval (
(r1 + r2),
(KrRoot p))
by A7, A6, POLYNOM3:def 10
.=
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
f)
by A10, POLYNOM4:19
;
verum end; end; hence
S1[
k]
;
verum end;
A11:
for k being Nat holds S1[k]
from NAT_1:sch 4(A3);
ex n being Nat st len f = n
;
hence
eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
by A11; verum