set n = card (nonConstantPolys F);
set M = nonConstantPolys (g,F);
set I = (nonConstantPolys (g,F)) -Ideal ;
set R = Polynom-Ring ((card (nonConstantPolys F)),F);
now (nonConstantPolys (g,F)) -Ideal is proper assume
not
(nonConstantPolys (g,F)) -Ideal is
proper
;
contradictionthen
(nonConstantPolys (g,F)) -Ideal = the
carrier of
(Polynom-Ring ((card (nonConstantPolys F)),F))
by SUBSET_1:def 6;
then consider Ps being non
empty finite Subset of
(Polynom-Ring ((card (nonConstantPolys F)),F)),
L being
LeftLinearCombination of
Ps such that A:
(
Ps c= nonConstantPolys (
g,
F) &
1. (Polynom-Ring ((card (nonConstantPolys F)),F)) = Sum L )
by ideal1;
then reconsider L =
L as non
empty LeftLinearCombination of
Ps ;
set PsF =
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } ;
H:
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } is
finite
proof
defpred S1[
object ,
object ]
means ex
p being non
constant Element of the
carrier of
(Polynom-Ring F) st
(
p in { p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } &
F = p &
g = Poly (
(g . p),
p) );
H0:
for
x being
object st
x in { p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } holds
ex
y being
object st
(
y in Ps &
S1[
x,
y] )
consider f being
Function of
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } ,
Ps such that H1:
for
x being
object st
x in { p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } holds
S1[
x,
f . x]
from FUNCT_2:sch 1(H0);
H3:
rng f c= Ps
by RELAT_1:def 19;
f is
one-to-one
proof
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume H4:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
x1 = x2then consider p1 being non
constant Element of the
carrier of
(Polynom-Ring F) such that H5:
(
p1 in { p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } &
x1 = p1 &
f . x1 = Poly (
(g . p1),
p1) )
by H1;
consider p2 being non
constant Element of the
carrier of
(Polynom-Ring F) such that H6:
(
p2 in { p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } &
x2 = p2 &
f . x2 = Poly (
(g . p2),
p2) )
by H1, H4;
H7:
(
p1 is non
constant Polynomial of
F &
p2 is non
constant Polynomial of
F )
(
rng g c= card (nonConstantPolys F) &
dom g = nonConstantPolys F &
p1 in nonConstantPolys F &
p2 in nonConstantPolys F )
by FUNCT_2:def 1, RELAT_1:def 19;
then
(
g . p1 in card (nonConstantPolys F) &
g . p2 in card (nonConstantPolys F) )
by FUNCT_1:3;
hence
x1 = x2
by H4, H5, H6, H7, bij3;
verum end;
hence
f is
one-to-one
;
verum
end;
then
dom f is
finite
by H3, CARD_1:59;
hence
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } is
finite
by FUNCT_2:def 1;
verum
end;
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } is
Subset of the
carrier of
(Polynom-Ring F)
then reconsider PsF =
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : Poly ((g . p),p) in Ps } as
finite Subset of the
carrier of
(Polynom-Ring F) by H;
consider E being
FieldExtension of
F such that B:
for
p being non
constant Element of the
carrier of
(Polynom-Ring F) st
p in PsF holds
p is_with_roots_in E
by KrSet;
reconsider S =
Polynom-Ring (
(card (nonConstantPolys F)),
E) as
comRingExtension of
Polynom-Ring (
(card (nonConstantPolys F)),
F)
by ringext;
D:
F is
Subring of
E
by FIELD_4:def 1;
ex
x being
Function of
(card (nonConstantPolys F)),
E st
for
pF being non
constant Element of the
carrier of
(Polynom-Ring F) st
pF in PsF holds
ex
a being
Element of
E st
(
x . (g . pF) = a &
Ext_eval (
pF,
a)
= 0. E )
then consider x being
Function of
(card (nonConstantPolys F)),
E such that C:
for
pF being non
constant Element of the
carrier of
(Polynom-Ring F) st
pF in PsF holds
ex
a being
Element of
E st
(
x . (g . pF) = a &
Ext_eval (
pF,
a)
= 0. E )
;
reconsider p =
Sum L as
Polynomial of
(card (nonConstantPolys F)),
F by POLYNOM1:def 11;
consider G being
FinSequence of the
carrier of
E such that U:
(
len G = len L &
Ext_eval (
p,
x)
= Sum G & ( for
i being
set st
i in dom G holds
for
q being
Polynomial of
(card (nonConstantPolys F)),
F st
q = L . i holds
G . i = Ext_eval (
q,
x) ) )
by ideal2;
E:
for
i being
Nat st
i in dom L holds
for
q being
Polynomial of
(card (nonConstantPolys F)),
F st
q = L . i holds
Ext_eval (
q,
x)
= 0. E
proof
let i be
Nat;
( i in dom L implies for q being Polynomial of (card (nonConstantPolys F)),F st q = L . i holds
Ext_eval (q,x) = 0. E )
assume E1:
i in dom L
;
for q being Polynomial of (card (nonConstantPolys F)),F st q = L . i holds
Ext_eval (q,x) = 0. E
let q be
Polynomial of
(card (nonConstantPolys F)),
F;
( q = L . i implies Ext_eval (q,x) = 0. E )
assume
q = L . i
;
Ext_eval (q,x) = 0. E
then
q = L /. i
by E1, PARTFUN1:def 6;
then consider u being
Element of
(Polynom-Ring ((card (nonConstantPolys F)),F)),
p being
Element of
Ps such that E2:
q = u * p
by E1, IDEAL_1:def 9;
reconsider p =
p as
Polynomial of
(card (nonConstantPolys F)),
F by POLYNOM1:def 11;
p in nonConstantPolys (
g,
F)
by A;
then consider pF being non
constant Element of the
carrier of
(Polynom-Ring F) such that E3:
Poly (
(g . pF),
pF)
= p
;
E7:
dom x = card (nonConstantPolys F)
by FUNCT_2:def 1;
E8:
(
rng g c= card (nonConstantPolys F) &
dom g = nonConstantPolys F &
pF in nonConstantPolys F )
by FUNCT_2:def 1, RELAT_1:def 19;
E9:
g . pF in rng g
by E8, FUNCT_1:3;
then E6:
x . (g . pF) = x /. (g . pF)
by E8, E7, PARTFUN1:def 6;
pF in PsF
by E3;
then consider a being
Element of
E such that E4:
(
x . (g . pF) = a &
Ext_eval (
pF,
a)
= 0. E )
by C;
E5:
Ext_eval (
(Poly ((g . pF),pF)),
x)
= 0. E
by E9, E8, E6, E4, eval0;
reconsider u =
u as
Polynomial of
(card (nonConstantPolys F)),
F by POLYNOM1:def 11;
thus Ext_eval (
q,
x) =
Ext_eval (
(u *' (Poly ((g . pF),pF))),
x)
by E2, E3, POLYNOM1:def 11
.=
(Ext_eval (u,x)) * (0. E)
by D, E5, evalti
.=
0. E
;
verum
end; F:
for
i being
Element of
NAT st
i in dom G holds
G /. i = 0. E
then H:
for
i being
Element of
NAT st
i in dom G &
i <> 1 holds
G /. i = 0. E
;
G:
1
in dom G
then 0. E =
G /. 1
by F
.=
Ext_eval (
p,
x)
by U, G, H, POLYNOM2:3
.=
Ext_eval (
(1_ ((card (nonConstantPolys F)),F)),
x)
by A, POLYNOM1:def 11
.=
1. E
by D, eval1
;
hence
contradiction
;
verum end;
hence
(nonConstantPolys (g,F)) -Ideal is proper
; verum