let F be polynomial_disjoint Field; :: thesis: 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); :: thesis: 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

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 ;

:: thesis: verum

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: 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

F0:
dom (KroneckerIso p) = the carrier of (Polynom-Ring p)
by FUNCT_2:def 1;
set g = (PolyHom isoi) . t;

A: for a being Element of F holds isoi . ((emb p) . a) = a

end;A: for a being Element of F holds isoi . ((emb p) . a) = a

proof

let a be Element of F; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum

now :: thesis: for x being object st x in NAT holds

((PolyHom isoi) . t) . x = p . x

hence
(PolyHom isoi) . t = p
; :: thesis: verum((PolyHom isoi) . t) . x = p . x

let x be object ; :: thesis: ( x in NAT implies ((PolyHom isoi) . t) . x = p . x )

assume x in NAT ; :: thesis: ((PolyHom isoi) . t) . x = p . x

then reconsider i = x as Element of NAT ;

((PolyHom isoi) . t) . i = isoi . ((emb (p,p)) . i) by FIELD_1:def 2

.= isoi . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((p . i) | F))) by FIELD_1:40

.= isoi . ((emb p) . (p . i)) by FIELD_1:39 ;

hence ((PolyHom isoi) . t) . x = p . x by A; :: thesis: verum

end;assume x in NAT ; :: thesis: ((PolyHom isoi) . t) . x = p . x

then reconsider i = x as Element of NAT ;

((PolyHom isoi) . t) . i = isoi . ((emb (p,p)) . i) by FIELD_1:def 2

.= isoi . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((p . i) | F))) by FIELD_1:40

.= isoi . ((emb p) . (p . i)) by FIELD_1:39 ;

hence ((PolyHom isoi) . t) . x = p . x by A; :: thesis: verum

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 ;

:: thesis: verum