deffunc H1( set ) -> set = \$1;
let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian
let X be infinite Ordinal; :: thesis: not Polynom-Ring (X,R) is Noetherian
assume A1: Polynom-Ring (X,R) is Noetherian ; :: thesis: 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))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (1_1 (n,R)) where n is Element of X : n in NAT } or x in the carrier of (Polynom-Ring (X,R)) )
assume x in { (1_1 (n,R)) where n is Element of X : n in NAT } ; :: thesis: x in the carrier of (Polynom-Ring (X,R))
then ex n being Element of X st
( x = 1_1 (n,R) & n in NAT ) ;
hence x in the carrier of (Polynom-Ring (X,R)) by POLYNOM1:def 11; :: thesis: verum
end;
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 ;
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 A9: { H1(n) where n is Element of X : H2(n) in C } c= NAT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(n) where n is Element of X : H2(n) in C } or x in NAT )
assume x in { H1(n) where n is Element of X : H2(n) in C } ; :: thesis:
then consider n being Element of X such that
A10: x = n and
A11: 1_1 (n,R) in C ;
1_1 (n,R) in S by ;
then ex m being Element of X st
( 1_1 (n,R) = 1_1 (m,R) & m in NAT ) ;
hence x in NAT by ; :: thesis: verum
end;
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 ;
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
now :: thesis: 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) * v
let i be set ; :: thesis: ( 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 ; :: thesis: ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * v
then 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; :: thesis: ex v being Element of R ex a being Element of cR st LC /. i = (u * a) * v
take v = v; :: thesis: ex a being Element of cR st LC /. i = (u * a) * v
take a = a; :: thesis: LC /. i = (u * a) * v
thus LC /. i = LC . k by
.= (u * a) * v by ; :: thesis: verum
end;
then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def 8;
A19: now :: thesis: for i being Element of NAT st i in dom LC holds
LC . i = 0. R
let i be Element of NAT ; :: thesis: ( i in dom LC implies LC . i = 0. R )
A20: now :: thesis: not m2 in CNend;
assume A21: i in dom LC ; :: thesis: LC . i = 0. R
then i in dom lc by ;
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
.= 0. R ;
A24: Support (1_1 (n,R)) = {()} 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)) . ()) * (eval ((),ev)) by
.= (1_ R) * (eval ((),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
.= (0. R) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `3_3)) by
.= 0. R ; :: thesis: 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
.= (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
.= 0. R by ;
hence contradiction by A14, A28; :: thesis: verum