let F be polynomial_disjoint Field; for p being irreducible Element of the carrier of (Polynom-Ring F) holds Ext_eval (p,(KrRootP p)) = 0. F
let p be irreducible Element of the carrier of (Polynom-Ring F); Ext_eval (p,(KrRootP p)) = 0. F
set K = KroneckerField (F,p);
set u = KrRoot p;
set E = embField (canHomP p);
set h = (KroneckerIso p) * (emb_iso (canHomP p));
reconsider h = (KroneckerIso p) * (emb_iso (canHomP p)) as Function of (embField (canHomP p)),(KroneckerField (F,p)) by FUNCT_2:13;
emb_iso (canHomP p) is onto
by lemdis, FIELD_2:15;
then B:
( h is one-to-one & h is onto )
by FUNCT_2:27;
( emb_iso (canHomP p) is additive & emb_iso (canHomP p) is multiplicative )
by lemdis, FIELD_2:13, FIELD_2:14;
then C:
h is linear
by RINGCAT1:1;
then reconsider P = KroneckerField (F,p) as embField (canHomP p) -isomorphic Field by B, RING_3:def 4;
reconsider iso = h as Isomorphism of (embField (canHomP p)),P by B, C;
reconsider E = embField (canHomP p) as P -isomorphic Field by RING_3:74;
reconsider E = E as P -homomorphic Field ;
reconsider isoi = iso " as Homomorphism of P,E by RING_3:73;
reconsider t = emb (p,p) as Element of the carrier of (Polynom-Ring P) ;
reconsider ui = KrRoot p as Element of P ;
KrRoot p is_a_root_of emb (p,p)
by FIELD_1:42;
then X:
eval (((PolyHom isoi) . t),(isoi . ui)) = 0. E
by FIELD_1:34, POLYNOM5:def 7;
Y:
(PolyHom isoi) . t = p
proof
set g =
(PolyHom isoi) . t;
A:
for
a being
Element of
F holds
isoi . ((emb p) . a) = a
proof
let a be
Element of
F;
isoi . ((emb p) . a) = a
reconsider b =
a | F as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
A12:
the
carrier of
(Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p }
by RING_4:def 8;
(
deg (a | F) <= 0 &
deg p > 0 )
by RATFUNC1:def 2, RING_4:def 4;
then A3:
a | F in the
carrier of
(Polynom-Ring p)
by A12;
then reconsider b1 =
a | F as
Element of
(Polynom-Ring p) ;
reconsider v =
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
b) as
Element of
(KroneckerField (F,p)) by RING_1:12;
A5:
b1 in dom (KroneckerIso p)
by A3, FUNCT_2:def 1;
A7:
dom ((KroneckerIso p) ") =
rng (KroneckerIso p)
by FUNCT_1:33
.=
the
carrier of
(KroneckerField (F,p))
by FUNCT_2:def 3
;
(KroneckerIso p) . b1 = v
by FIELD_4:def 9;
then A6:
((KroneckerIso p) ") . v = b1
by A5, FUNCT_1:34;
F is
Subfield of
embField (canHomP p)
by FIELD_2:17;
then
the
carrier of
F c= the
carrier of
(embField (canHomP p))
by EC_PF_1:def 1;
then reconsider aa =
a as
Element of
(embField (canHomP p)) ;
A9:
dom (emb_iso (canHomP p)) = the
carrier of
E
by FUNCT_2:def 1;
aa in F
;
then (emb_iso (canHomP p)) . aa =
(canHomP p) . aa
by FIELD_2:def 8
.=
a | F
by defch
;
then A2:
((emb_iso (canHomP p)) ") . b1 = aa
by A9, FUNCT_1:34;
thus isoi . ((emb p) . a) =
isoi . v
by FIELD_1:39
.=
(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . v
by FUNCT_1:44
.=
a
by A2, A6, A7, FUNCT_1:13
;
verum
end;
hence
(PolyHom isoi) . t = p
;
verum
end;
F0:
dom (KroneckerIso p) = the carrier of (Polynom-Ring p)
by FUNCT_2:def 1;
E5:
rng (KroneckerIso p) = the carrier of (KroneckerField (F,p))
by FUNCT_2:def 3;
then
KrRoot p in rng (KroneckerIso p)
;
then E3:
KrRoot p in dom ((KroneckerIso p) ")
by FUNCT_1:32;
then E6:
((KroneckerIso p) ") . (KrRoot p) in rng ((KroneckerIso p) ")
by FUNCT_1:def 3;
E9:
emb_iso (canHomP p) is onto
by lemdis, FIELD_2:15;
then E4:
((KroneckerIso p) ") . (KrRoot p) in rng (emb_iso (canHomP p))
by E6, F0, FUNCT_1:33;
E10:
((KroneckerIso p) ") . (KrRoot p) in dom (KroneckerIso p)
by E6, FUNCT_1:33;
dom ((emb_iso (canHomP p)) ") =
the carrier of (Polynom-Ring p)
by E9, FUNCT_1:33
.=
dom (KroneckerIso p)
by FUNCT_2:def 1
;
then
((emb_iso (canHomP p)) ") . (((KroneckerIso p) ") . (KrRoot p)) in rng ((emb_iso (canHomP p)) ")
by E10, FUNCT_1:3;
then
((emb_iso (canHomP p)) ") . (((KroneckerIso p) ") . (KrRoot p)) in dom (emb_iso (canHomP p))
by FUNCT_1:33;
then E2:
(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p) in dom (emb_iso (canHomP p))
by E3, FUNCT_1:13;
iso . (KrRootP p) =
(KroneckerIso p) . ((emb_iso (canHomP p)) . ((((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p)))
by E2, FUNCT_1:13
.=
(KroneckerIso p) . ((emb_iso (canHomP p)) . (((emb_iso (canHomP p)) ") . (((KroneckerIso p) ") . (KrRoot p))))
by E3, FUNCT_1:13
.=
(KroneckerIso p) . (((KroneckerIso p) ") . (KrRoot p))
by E4, FUNCT_1:35
.=
KrRoot p
by E5, FUNCT_1:35
;
then
isoi . ui = KrRootP p
by FUNCT_2:26;
hence Ext_eval (p,(KrRootP p)) =
0. E
by X, Y, FIELD_4:26
.=
0. F
by FIELD_2:def 7
;
verum