let n be non zero Nat; for F being non almost_trivial Field ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
let F be non almost_trivial Field; ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
set x = the non trivial Element of F;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider o = rpoly (n,(0. F)) as object ;
set x = the non trivial Element of F;
per cases
( not o in [#] F or ex a being Element of F st a = rpoly (n,(0. F)) )
;
suppose A1:
not
o in [#] F
;
ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )then reconsider K =
ExField ( the non
trivial Element of
F,
(rpoly (n,(0. F)))) as
Field by Th7, Th8, Th10, Th9, Th12, Th11;
set p =
rpoly (
n,
(0. K));
then A5:
rpoly (
n,
(0. F))
= rpoly (
n,
(0. K))
;
A6:
rpoly (
n,
(0. K))
in [#] (Polynom-Ring K)
by POLYNOM3:def 10;
rpoly (
n,
(0. K))
in {(rpoly (n,(0. F)))}
by A5, TARSKI:def 1;
then
rpoly (
n,
(0. K))
in carr ( the non
trivial Element of
F,
(rpoly (n,(0. F))))
by XBOOLE_0:def 3;
then A7:
rpoly (
n,
(0. K))
in [#] K
by Def8;
then
rpoly (
n,
(0. K))
in ([#] K) /\ ([#] (Polynom-Ring K))
by A6, XBOOLE_0:def 4;
then reconsider K =
K as non
polynomial_disjoint Field by Def3;
take
K
;
ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )take p =
rpoly (
n,
(0. K));
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
(
isoR ( the non
trivial Element of
F,
(rpoly (n,(0. F)))) is
additive &
isoR ( the non
trivial Element of
F,
(rpoly (n,(0. F)))) is
multiplicative &
isoR ( the non
trivial Element of
F,
(rpoly (n,(0. F)))) is
unity-preserving )
by A1, Th15;
hence
K,
F are_isomorphic
by MOD_4:def 12, QUOFIELD:def 23;
( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )thus
(
deg p = n &
p in ([#] K) /\ ([#] (Polynom-Ring K)) )
by A7, A6, XBOOLE_0:def 4, HURWITZ:27;
verum end; end;