deffunc H_{1}( 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 H_{2}( 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 H_{2}(d1) = H_{2}(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))

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 = { H_{1}(n) where n is Element of X : H_{2}(n) in C } ;

A7: C is finite ;

A8: { H_{1}(n) where n is Element of X : H_{2}(n) in C } is finite
from FUNCT_7:sch 2(A7, A2);

A9: { H_{1}(n) where n is Element of X : H_{2}(n) in C } c= NAT

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 { H_{1}(n) where n is Element of X : H_{2}(n) in C }
by A12;

then reconsider CN = { H_{1}(n) where n is Element of X : H_{2}(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 H_{3}( 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 = H_{3}(k)
from FINSEQ_2:sch 1();

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; :: thesis: verum

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 H

set tcR = the carrier of R;

A2: for d1, d2 being Element of X st H

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

1_1 (0X,R) in { (1_1 (n,R)) where n is Element of X : n in NAT }
;
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;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

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 = { H

A7: C is finite ;

A8: { H

A9: { H

proof

set c = the Element of C;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(n) where n is Element of X : H_{2}(n) in C } or x in NAT )

assume x in { H_{1}(n) where n is Element of X : H_{2}(n) in C }
; :: thesis: x in NAT

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 A5, A11;

then ex m being Element of X st

( 1_1 (n,R) = 1_1 (m,R) & m in NAT ) ;

hence x in NAT by A10, Th14; :: thesis: verum

end;assume x in { H

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 A5, A11;

then ex m being Element of X st

( 1_1 (n,R) = 1_1 (m,R) & m in NAT ) ;

hence x in NAT by A10, Th14; :: thesis: verum

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 { H

then reconsider CN = { H

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 H

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 = H

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

then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def 8;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 A18, PARTFUN1:def 6

.= (u * a) * v by A17, A18 ; :: thesis: verum

end;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 A18, PARTFUN1:def 6

.= (u * a) * v by A17, A18 ; :: thesis: verum

A19: now :: thesis: for i being Element of NAT st i in dom LC holds

LC . i = 0. R

dom (X --> (0. R)) = X
;LC . i = 0. R

let i be Element of NAT ; :: thesis: ( i in dom LC implies LC . i = 0. R )

then 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 ; :: thesis: verum

end;A20: now :: thesis: not m2 in CN

assume A21:
i in dom LC
; :: thesis: LC . i = 0. Rassume
m2 in CN
; :: thesis: contradiction

then (max CN) + 1 <= max CN by XXREAL_2:def 8;

hence contradiction by XREAL_1:29; :: thesis: verum

end;then (max CN) + 1 <= max CN by XXREAL_2:def 8;

hence contradiction by XREAL_1:29; :: thesis: verum

then 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 ; :: thesis: verum

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; :: thesis: verum