deffunc H1( set ) -> set = $1;
let R be non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive 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:102;
0 in NAT
;
then 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:99;
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
consider c being Element of C;
c in C
;
then
c in S
by A5;
then consider cn being Element of X such that
A12:
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 13;
reconsider m1 = mm + 1 as Element of NAT ;
m1 in NAT
;
then reconsider m2 = m1 as Element of X by A3;
( 1_1 m2,R in S & S c= S -Ideal )
by IDEAL_1:def 15;
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 )) * ((Polynom-Evaluation X,R,ev) . ((E /. $1) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. $1) `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 let 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 ) as
Element of
cR ;
reconsider u =
(Polynom-Evaluation X,R,ev) . ((E /. k) `1 ),
v =
(Polynom-Evaluation X,R,ev) . ((E /. k) `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 8
.=
(u * a) * v
by A17, A18
;
verum end;
then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def 9;
A19:
now let i be
Element of
NAT ;
( i in dom LC implies LC . i = 0. R )assume A21:
i in dom LC
;
LC . i = 0. Rthen
i in dom lc
by A16, FINSEQ_3:31;
then reconsider y =
(E /. i) `2 as
Element of
C by A15, IDEAL_1:def 12;
y in C
;
then
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:34
.=
0. R
by FUNCOP_1:13
;
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:21
.=
(1_ R) * (eval (UnitBag n),ev)
by Th12
.=
(1_ R) * (ev . n)
by Th11
.=
0. R
by A23, VECTSP_1:36
;
thus LC . i =
(((Polynom-Evaluation X,R,ev) . ((E /. i) `1 )) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `3 ))
by A17, A21
.=
(0. R) * ((Polynom-Evaluation X,R,ev) . ((E /. i) `3 ))
by A22, A25, VECTSP_1:36
.=
0. R
by VECTSP_1:36
;
verum end;
dom (X --> (0. R)) = X
by FUNCOP_1:19;
then A26:
ev . m2 = 1_ R
by FUNCT_7:33;
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:21
.=
(1_ R) * (eval (UnitBag m2),ev)
by Th12
.=
(1_ R) * (ev . m2)
by Th11
.=
1_ R
by A26, GROUP_1:def 5
;
for k being set st k in dom LC holds
LC . k = (((Polynom-Evaluation X,R,ev) . ((E /. k) `1 )) * ((Polynom-Evaluation X,R,ev) . ((E /. k) `2 ))) * ((Polynom-Evaluation X,R,ev) . ((E /. k) `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, VECTSP_1:36, VECTSP_1:def 13; verum