deffunc H1( set ) -> set = $1;
let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian
let X be infinite Ordinal; not Polynom-Ring (X,R) is Noetherian
assume A1:
Polynom-Ring (X,R) is Noetherian
; contradiction
reconsider f0 = X --> (0. R) as Function of X, the carrier of R ;
deffunc H2( Element of X) -> Series of X,R = 1_1 ($1,R);
set tcR = the carrier of R;
A2:
for d1, d2 being Element of X st H2(d1) = H2(d2) holds
d1 = d2
by Th14;
the carrier of R c= the carrier of R
;
then reconsider cR = the carrier of R as non empty Subset of the carrier of R ;
set S = { (1_1 (n,R)) where n is Element of X : n in NAT } ;
set tcPR = the carrier of (Polynom-Ring (X,R));
A3:
NAT c= X
by CARD_3:85;
reconsider 0X = 0 as Element of X by A3;
A4:
{ (1_1 (n,R)) where n is Element of X : n in NAT } c= the carrier of (Polynom-Ring (X,R))
1_1 (0X,R) in { (1_1 (n,R)) where n is Element of X : n in NAT }
;
then reconsider S = { (1_1 (n,R)) where n is Element of X : n in NAT } as non empty Subset of the carrier of (Polynom-Ring (X,R)) by A4;
consider C being non empty finite Subset of the carrier of (Polynom-Ring (X,R)) such that
A5:
C c= S
and
A6:
C -Ideal = S -Ideal
by A1, IDEAL_1:96;
set CN = { H1(n) where n is Element of X : H2(n) in C } ;
A7:
C is finite
;
A8:
{ H1(n) where n is Element of X : H2(n) in C } is finite
from FUNCT_7:sch 2(A7, A2);
A9:
{ H1(n) where n is Element of X : H2(n) in C } c= NAT
set c = the Element of C;
the Element of C in S
by A5;
then consider cn being Element of X such that
A12:
the Element of C = 1_1 (cn,R)
and
A13:
cn in NAT
;
reconsider cn = cn as Element of NAT by A13;
cn in { H1(n) where n is Element of X : H2(n) in C }
by A12;
then reconsider CN = { H1(n) where n is Element of X : H2(n) in C } as non empty finite Subset of NAT by A8, A9;
reconsider mm = max CN as Element of NAT by ORDINAL1:def 12;
reconsider m1 = mm + 1 as Element of NAT ;
reconsider m2 = m1 as Element of X by A3;
( 1_1 (m2,R) in S & S c= S -Ideal )
by IDEAL_1:def 14;
then consider lc being LinearCombination of C such that
A14:
1_1 (m2,R) = Sum lc
by A6, IDEAL_1:60;
reconsider ev = f0 +* (m2,(1_ R)) as Function of X,R ;
consider E being FinSequence of [: the carrier of (Polynom-Ring (X,R)), the carrier of (Polynom-Ring (X,R)), the carrier of (Polynom-Ring (X,R)):] such that
A15:
E represents lc
by IDEAL_1:35;
set P = Polynom-Evaluation (X,R,ev);
deffunc H3( Nat) -> Element of the carrier of R = (((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `3_3));
consider LC being FinSequence of the carrier of R such that
A16:
len LC = len lc
and
A17:
for k being Nat st k in dom LC holds
LC . k = H3(k)
from FINSEQ_2:sch 1();
now for i being set st i in dom LC holds
ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * vlet i be
set ;
( i in dom LC implies ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * v )assume A18:
i in dom LC
;
ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * vthen reconsider k =
i as
Element of
NAT ;
reconsider a =
(Polynom-Evaluation (X,R,ev)) . ((E /. k) `2_3) as
Element of
cR ;
reconsider u =
(Polynom-Evaluation (X,R,ev)) . ((E /. k) `1_3),
v =
(Polynom-Evaluation (X,R,ev)) . ((E /. k) `3_3) as
Element of
R ;
take u =
u;
ex v being Element of R ex a being Element of cR st LC /. i = (u * a) * vtake v =
v;
ex a being Element of cR st LC /. i = (u * a) * vtake a =
a;
LC /. i = (u * a) * vthus LC /. i =
LC . k
by A18, PARTFUN1:def 6
.=
(u * a) * v
by A17, A18
;
verum end;
then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def 8;
A19:
now for i being Element of NAT st i in dom LC holds
LC . i = 0. Rlet i be
Element of
NAT ;
( i in dom LC implies LC . i = 0. R )A20:
now not m2 in CNend; assume A21:
i in dom LC
;
LC . i = 0. Rthen
i in dom lc
by A16, FINSEQ_3:29;
then reconsider y =
(E /. i) `2_3 as
Element of
C by A15;
y in S
by A5;
then consider n being
Element of
X such that A22:
y = 1_1 (
n,
R)
and
n in NAT
;
n in CN
by A22;
then A23:
ev . n =
(X --> (0. R)) . n
by A20, FUNCT_7:32
.=
0. R
;
A24:
Support (1_1 (n,R)) = {(UnitBag n)}
by Th13;
A25:
(Polynom-Evaluation (X,R,ev)) . (1_1 (n,R)) =
eval (
(1_1 (n,R)),
ev)
by POLYNOM2:def 5
.=
((1_1 (n,R)) . (UnitBag n)) * (eval ((UnitBag n),ev))
by A24, POLYNOM2:19
.=
(1_ R) * (eval ((UnitBag n),ev))
by Th12
.=
(1_ R) * (ev . n)
by Th11
.=
0. R
by A23
;
thus LC . i =
(((Polynom-Evaluation (X,R,ev)) . ((E /. i) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `3_3))
by A17, A21
.=
(0. R) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `3_3))
by A22, A25
.=
0. R
;
verum end;
dom (X --> (0. R)) = X
;
then A26:
ev . m2 = 1_ R
by FUNCT_7:31;
A27:
Support (1_1 (m2,R)) = {(UnitBag m2)}
by Th13;
A28: (Polynom-Evaluation (X,R,ev)) . (1_1 (m2,R)) =
eval ((1_1 (m2,R)),ev)
by POLYNOM2:def 5
.=
((1_1 (m2,R)) . (UnitBag m2)) * (eval ((UnitBag m2),ev))
by A27, POLYNOM2:19
.=
(1_ R) * (eval ((UnitBag m2),ev))
by Th12
.=
(1_ R) * (ev . m2)
by Th11
.=
1_ R
by A26
;
for k being set st k in dom LC holds
LC . k = (((Polynom-Evaluation (X,R,ev)) . ((E /. k) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. k) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. k) `3_3))
by A17;
then (Polynom-Evaluation (X,R,ev)) . (Sum lc) =
Sum LC
by A15, A16, Th24
.=
0. R
by A19, POLYNOM3:1
;
hence
contradiction
by A14, A28; verum