set PR = Polynom-Ring R;
set cPR = the carrier of (Polynom-Ring R);
set cR = the carrier of R;
now
assume not Polynom-Ring R is Noetherian ; :: thesis: contradiction
then consider I being Ideal of (Polynom-Ring R) such that
A1: not I is finitely_generated by IDEAL_1:def 27;
defpred S1[ set , set , set ] means ( c2 is non empty finite Subset of I implies ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = c2 & B = I \ (A -Ideal ) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & c3 = c2 \/ {r} ) ) );
A2: now
let n be Element of NAT ; :: thesis: for x being Subset of the carrier of (Polynom-Ring R) ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b3,b4]
let x be Subset of the carrier of (Polynom-Ring R); :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
per cases ( not x is non empty finite Subset of I or x is non empty finite Subset of I ) ;
suppose x is not non empty finite Subset of I ; :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
hence ex y being Subset of the carrier of (Polynom-Ring R) st S1[n,x,y] ; :: thesis: verum
end;
suppose A3: x is non empty finite Subset of I ; :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
then reconsider x' = x as non empty Subset of the carrier of (Polynom-Ring R) ;
set B = I \ (x' -Ideal );
then reconsider B = I \ (x' -Ideal ) as non empty Subset of the carrier of (Polynom-Ring R) ;
A5: minlen B c= the carrier of (Polynom-Ring R) by XBOOLE_1:1;
consider r being set such that
A6: r in minlen B by XBOOLE_0:def 1;
reconsider r = r as Element of the carrier of (Polynom-Ring R) by A5, A6;
S1[n,x,x' \/ {r}] by A6;
hence ex y being Subset of the carrier of (Polynom-Ring R) st S1[n,x,y] ; :: thesis: verum
end;
end;
end;
consider F being Function of NAT , bool the carrier of (Polynom-Ring R) such that
A7: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
defpred S2[ Element of NAT ] means F . R is non empty finite Subset of I;
F . 0 c= I
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F . 0 or x in I )
assume x in F . 0 ; :: thesis: x in I
then x = 0. (Polynom-Ring R) by A7, TARSKI:def 1;
hence x in I by IDEAL_1:2; :: thesis: verum
end;
then A8: S2[ 0 ] by A7;
A9: now
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume S2[n] ; :: thesis: S2[n + 1]
then reconsider Fn = F . n as non empty finite Subset of I ;
consider A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A10: ( A = Fn & B = I \ (A -Ideal ) ) and
A11: ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (n + 1) = Fn \/ {r} ) by A7;
consider r being Element of the carrier of (Polynom-Ring R) such that
A12: ( r in minlen B & F . (n + 1) = Fn \/ {r} ) by A11;
r in I by A10, A12, XBOOLE_0:def 5;
then {r} c= I by ZFMISC_1:37;
hence S2[n + 1] by A12, XBOOLE_1:8; :: thesis: verum
end;
A13: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A8, A9);
A14: for i, j being Element of NAT st i <= j holds
F . i c= F . j
proof
let i, j be Element of NAT ; :: thesis: ( i <= j implies F . i c= F . j )
assume i <= j ; :: thesis: F . i c= F . j
then consider m being Nat such that
A15: j = i + m by NAT_1:10;
A16: m in NAT by ORDINAL1:def 13;
defpred S3[ Element of NAT ] means F . i c= F . (i + R);
A17: S3[ 0 ] ;
A18: for m being Element of NAT st S3[m] holds
S3[m + 1]
proof
let m be Element of NAT ; :: thesis: ( S3[m] implies S3[m + 1] )
assume A19: F . i c= F . (i + m) ; :: thesis: S3[m + 1]
F . (i + m) is non empty finite Subset of I by A13;
then consider A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
( A = F . (i + m) & B = I \ (A -Ideal ) ) and
A20: ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . ((i + m) + 1) = (F . (i + m)) \/ {r} ) by A7;
consider r being Element of the carrier of (Polynom-Ring R) such that
A21: ( r in minlen B & F . ((i + m) + 1) = (F . (i + m)) \/ {r} ) by A20;
F . (i + m) c= F . ((i + m) + 1) by A21, XBOOLE_1:7;
hence F . i c= F . (i + (m + 1)) by A19, XBOOLE_1:1; :: thesis: verum
end;
for m being Element of NAT holds S3[m] from NAT_1:sch 1(A17, A18);
 hence F . i c= F . j by A15, A16; :: thesis: verum
end;
defpred S3[ set , set ] means ex n being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n & B = I \ (A -Ideal ) & n = R & F . (n + 1) = (F . n) \/ {c2} & c2 in minlen B );
A22: now
let x be Element of NAT ; :: thesis: ex y being Element of the carrier of (Polynom-Ring R) st S3[x,y]
F . x is non empty finite Subset of I by A13;
then consider A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A23: ( A = F . x & B = I \ (A -Ideal ) ) and
A24: ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (x + 1) = (F . x) \/ {r} ) by A7;
thus ex y being Element of the carrier of (Polynom-Ring R) st S3[x,y] by A23, A24; :: thesis: verum
end;
consider f being Function of NAT ,the carrier of (Polynom-Ring R) such that
A25: for x being Element of NAT holds S3[x,f . x] from FUNCT_2:sch 3(A22);
A26: for i being Element of NAT holds f . i <> 0. (Polynom-Ring R)
proof
let i be Element of NAT ; :: thesis: f . i <> 0. (Polynom-Ring R)
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A27: ( A = F . n & B = I \ (A -Ideal ) & n = i & F . (n + 1) = (F . n) \/ {(f . i)} & f . i in minlen B ) by A25;
F . n c= A -Ideal by A27, IDEAL_1:def 15;
then A28: not f . i in F . n by A27, XBOOLE_0:def 5;
A29: F . 0 c= F . n by A14;
0. (Polynom-Ring R) in F . 0 by A7, TARSKI:def 1;
hence f . i <> 0. (Polynom-Ring R) by A28, A29; :: thesis: verum
end;
A30: for i, j being Element of NAT
for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj
proof
let i, j be Element of NAT ; :: thesis: for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj
let fi, fj be Polynomial of R; :: thesis: ( i <= j & fi = f . i & fj = f . j implies len fi <= len fj )
assume A31: ( i <= j & fi = f . i & fj = f . j ) ; :: thesis: len fi <= len fj
then consider k being Nat such that
A32: j = i + k by NAT_1:10;
A33: k in NAT by ORDINAL1:def 13;
defpred S4[ Element of NAT ] means for fk being Polynomial of R st fk = f . (i + R) holds
len fi <= len fk;
A34: S4[ 0 ] by A31;
A35: now
let k be Element of NAT ; :: thesis: ( S4[k] implies S4[k + 1] )
assume A36: S4[k] ; :: thesis: S4[k + 1]
now
let fk1 be Polynomial of R; :: thesis: ( fk1 = f . (i + (k + 1)) implies len fi <= len fk1 )
assume A37: fk1 = f . (i + (k + 1)) ; :: thesis: len fi <= len fk1
reconsider fk = f . (i + k) as Polynomial of R by POLYNOM3:def 12;
A38: len fi <= len fk by A36;
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A39: ( A = F . n & B = I \ (A -Ideal ) & n = i + k & F . (n + 1) = (F . n) \/ {(f . (i + k))} & f . (i + k) in minlen B ) by A25;
consider n' being Element of NAT , A', B' being non empty Subset of the carrier of (Polynom-Ring R) such that
A40: ( A' = F . n' & B' = I \ (A' -Ideal ) & n' = i + (k + 1) & F . (n' + 1) = (F . n') \/ {(f . (i + (k + 1)))} & f . (i + (k + 1)) in minlen B' ) by A25;
i + (k + 1) = (i + k) + 1 ;
then i + k < i + (k + 1) by NAT_1:13;
then A -Ideal c= A' -Ideal by A14, A39, A40, IDEAL_1:57;
then A41: not f . (i + (k + 1)) in A -Ideal by A40, XBOOLE_0:def 5;
f . (i + (k + 1)) in I by A40, XBOOLE_0:def 5;
then f . (i + (k + 1)) in B by A39, A41, XBOOLE_0:def 5;
then len fk <= len fk1 by A37, A39, Th17;
hence len fi <= len fk1 by A38, XXREAL_0:2; :: thesis: verum
end;
hence S4[k + 1] ; :: thesis: verum
end;
for k being Element of NAT holds S4[k] from NAT_1:sch 1(A34, A35);
 hence len fi <= len fj by A31, A32, A33; :: thesis: verum
end;
defpred S4[ set , set ] means ex n being Element of NAT ex A being Polynomial of R st
( n = R & A = f . n & c2 = A . ((len A) -' 1) );
A42: now
let x be Element of NAT ; :: thesis: ex y being Element of the carrier of R st S4[x,y]
reconsider fx = f . x as Polynomial of R by POLYNOM3:def 12;
fx . ((len fx) -' 1) is Element of the carrier of R ;
hence ex y being Element of the carrier of R st S4[x,y] ; :: thesis: verum
end;
consider a being Function of NAT ,the carrier of R such that
A43: for x being Element of NAT holds S4[x,a . x] from FUNCT_2:sch 3(A42);
reconsider a = a as sequence of R ;
for B being non empty Subset of the carrier of R ex C being non empty finite Subset of the carrier of R st
( C c= B & C -Ideal = B -Ideal ) by IDEAL_1:99;
then consider m being Element of NAT such that
A44: a . (m + 1) in (rng (a | (m + 1))) -Ideal by IDEAL_1:100;
consider lc being LinearCombination of rng (a | (Segm (m + 1))) such that
A45: a . (m + 1) = Sum lc by A44, IDEAL_1:60;
reconsider fm1 = f . (m + 1) as Polynomial of R by POLYNOM3:def 12;
A46: now
let i be Element of NAT ; :: thesis: for fi being Polynomial of R st fi = f . i holds
(len fi) - 1 >= 0
let fi be Polynomial of R; :: thesis: ( fi = f . i implies (len fi) - 1 >= 0 )
assume fi = f . i ; :: thesis: (len fi) - 1 >= 0
then fi <> 0. (Polynom-Ring R) by A26;
then fi <> 0_. R by POLYNOM3:def 12;
then len fi <> 0 by POLYNOM4:8;
then len fi > 0 ;
then len fi >= 0 + 1 by NAT_1:13;
hence (len fi) - 1 >= 0 by XREAL_1:21; :: thesis: verum
end;
defpred S5[ set , set ] means ( ex u, v, w being Element of the carrier of R st
( R = (u * v) * w & v in rng (a | (Segm (m + 1))) ) implies ex x, y, z being Element of the carrier of (Polynom-Ring R) ex p being Polynomial of R st
( c2 = p & p = (x * y) * z & R = p . ((len fm1) -' 1) & len p <= len fm1 & y in F . (m + 1) ) );
A47: for e being set st e in the carrier of R holds
ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
proof
let e be set ; :: thesis: ( e in the carrier of R implies ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] ) )
assume e in the carrier of R ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
per cases ( ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) or for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ) ;
suppose ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
then consider u, b', w being Element of the carrier of R such that
A48: e = (u * b') * w and
A49: b' in rng (a | (Segm (m + 1))) ;
set a' = u;
set c' = w;
consider n being set such that
A50: ( n in dom (a | (Segm (m + 1))) & b' = (a | (Segm (m + 1))) . n ) by A49, FUNCT_1:def 5;
A51: dom (a | (Segm (m + 1))) = (dom a) /\ (Segm (m + 1)) by FUNCT_1:68
.= NAT /\ (Segm (m + 1)) by FUNCT_2:def 1
.= Segm (m + 1) by XBOOLE_1:28 ;
reconsider n = n as Element of NAT by A50;
A52: n < m + 1 by A50, A51, GR_CY_1:10;
set y = f . n;
reconsider y' = f . n as Polynomial of R by POLYNOM3:def 12;
set x' = monomial u,((len fm1) -' (len y'));
set z' = monomial w,0 ;
reconsider x = monomial u,((len fm1) -' (len y')), z = monomial w,0 as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 12;
set p = (x * (f . n)) * z;
A53: x * (f . n) = (monomial u,((len fm1) -' (len y'))) *' y' by POLYNOM3:def 12;
then A54: (x * (f . n)) * z = ((monomial u,((len fm1) -' (len y'))) *' y') *' (monomial w,0 ) by POLYNOM3:def 12;
A55: b' = a . n by A50, FUNCT_1:70;
consider n' being Element of NAT , A being Polynomial of R such that
A56: ( n' = n & A = f . n' & a . n = A . ((len A) -' 1) ) by A43;
reconsider p = (x * (f . n)) * z as Polynomial of R by POLYNOM3:def 12;
len y' <= len fm1 by A30, A52;
then (len y') - (len y') <= (len fm1) - (len y') by XREAL_1:11;
then A57: (len fm1) -' (len y') = (len fm1) - (len y') by XREAL_0:def 2;
A58: (len y') - 1 >= 0 by A46;
(len fm1) - 1 >= 0 by A46;
then (len fm1) -' 1 = ((len fm1) - (len y')) + ((len y') - 1) by XREAL_0:def 2
.= ((len y') -' 1) + ((len fm1) -' (len y')) by A57, A58, XREAL_0:def 2 ;
then A59: ((monomial u,((len fm1) -' (len y'))) *' y') . ((len fm1) -' 1) = u * b' by A55, A56, Th19;
(len fm1) -' 1 = ((len fm1) -' 1) + 0 ;
then A60: (u * b') * w = p . ((len fm1) -' 1) by A54, A59, Th20;
len (monomial u,((len fm1) -' (len y'))) <= ((len fm1) - (len y')) + 1 by A57, Th18;
then A61: (len (monomial u,((len fm1) -' (len y')))) + ((len y') - 1) <= ((len fm1) - ((len y') - 1)) + ((len y') - 1) by XREAL_1:8;
A62: 0 + 0 <= ((len y') - 1) + (len (monomial u,((len fm1) -' (len y')))) by A58;
len ((monomial u,((len fm1) -' (len y'))) *' y') <= ((len (monomial u,((len fm1) -' (len y')))) + (len y')) -' 1 by Th21;
then len ((monomial u,((len fm1) -' (len y'))) *' y') <= ((len (monomial u,((len fm1) -' (len y')))) + (len y')) - 1 by A62, XREAL_0:def 2;
then A63: len ((monomial u,((len fm1) -' (len y'))) *' y') <= len fm1 by A61, XXREAL_0:2;
len (monomial w,0 ) <= 0 + 1 by Th18;
then (len ((monomial u,((len fm1) -' (len y'))) *' y')) + (len (monomial w,0 )) <= (len fm1) + 1 by A63, XREAL_1:9;
then A64: ((len ((monomial u,((len fm1) -' (len y'))) *' y')) + (len (monomial w,0 ))) -' 1 <= ((len fm1) + 1) -' 1 by NAT_D:42;
len (((monomial u,((len fm1) -' (len y'))) *' y') *' (monomial w,0 )) <= ((len ((monomial u,((len fm1) -' (len y'))) *' y')) + (len (monomial w,0 ))) -' 1 by Th21;
then len (((monomial u,((len fm1) -' (len y'))) *' y') *' (monomial w,0 )) <= ((len fm1) + 1) -' 1 by A64, XXREAL_0:2;
then len (((monomial u,((len fm1) -' (len y'))) *' y') *' (monomial w,0 )) <= ((len fm1) + 1) - 1 by XREAL_0:def 2;
then A65: len p <= (len fm1) + 0 by A53, POLYNOM3:def 12;
n + 1 <= m + 1 by A52, NAT_1:13;
then A66: F . (n + 1) c= F . (m + 1) by A14;
consider n' being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A67: ( A = F . n' & B = I \ (A -Ideal ) & n' = n & F . (n' + 1) = (F . n') \/ {(f . n)} & f . n in minlen B ) by A25;
{(f . n)} c= F . (n + 1) by A67, XBOOLE_1:7;
then f . n in F . (n + 1) by ZFMISC_1:37;
hence ex u being set st
( u in the carrier of (Polynom-Ring R) & S5[e,u] ) by A48, A60, A65, A66; :: thesis: verum
end;
suppose for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
hence ex u being set st
( u in the carrier of (Polynom-Ring R) & S5[e,u] ) ; :: thesis: verum
end;
end;
end;
consider LCT being Function of the carrier of R,the carrier of (Polynom-Ring R) such that
A68: for e being set st e in the carrier of R holds
S5[e,LCT . e] from FUNCT_2:sch 1(A47);
reconsider FM1 = F . (m + 1) as non empty Subset of the carrier of (Polynom-Ring R) by A13;
set raSm1 = rng (a | (Segm (m + 1)));
A69: for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )
dom LCT = the carrier of R by FUNCT_2:def 1;
then rng lc c= dom LCT ;
then A70: dom lc = dom (LCT * lc) by RELAT_1:46;
set LC = LCT * lc;
A71: len lc = len (LCT * lc) by A70, FINSEQ_3:31;
LCT * lc is LinearCombination of FM1
proof
let i be set ; :: according to IDEAL_1:def 9 :: thesis: ( not i in dom (LCT * lc) or ex b1, b2 being Element of the carrier of (Polynom-Ring R) ex b3 being Element of FM1 st (LCT * lc) /. i = (b1 * b3) * b2 )
assume A72: i in dom (LCT * lc) ; :: thesis: ex b1, b2 being Element of the carrier of (Polynom-Ring R) ex b3 being Element of FM1 st (LCT * lc) /. i = (b1 * b3) * b2
consider u, v being Element of R, a being Element of rng (a | (Segm (m + 1))) such that
A73: lc /. i = (u * a) * v by A70, A72, IDEAL_1:def 9;
A74: lc /. i = lc . i by A70, A72, PARTFUN1:def 8;
consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A75: ( LCT . (lc /. i) = p & p = (x * y) * z & (u * a) * v = p . ((len fm1) -' 1) & len p <= len fm1 & y in F . (m + 1) ) by A68, A73;
reconsider x = x, z = z as Element of (Polynom-Ring R) ;
reconsider y = y as Element of FM1 by A75;
(LCT * lc) /. i = (LCT * lc) . i by A72, PARTFUN1:def 8
.= (x * y) * z by A70, A72, A74, A75, FUNCT_1:23 ;
hence ex x, z being Element of (Polynom-Ring R) ex y being Element of FM1 st (LCT * lc) /. i = (x * y) * z ; :: thesis: verum
end;
then reconsider LC = LCT * lc as LinearCombination of FM1 ;
LC = LC ;
hence ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC ) by A71; :: thesis: verum
end;
for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
proof
defpred S6[ Element of NAT ] means for lc being LinearCombination of rng (a | (Segm (m + 1))) st len lc <= R holds
ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 );
A76: S6[ 0 ]
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ( len lc <= 0 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume len lc <= 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then A77: len lc = 0 ;
consider LC being LinearCombination of FM1 such that
A78: ( LC = LCT * lc & len lc = len LC ) by A69;
take LC ; :: thesis: ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
take p = 0_. R; :: thesis: ( LC = LCT * lc & p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus LC = LCT * lc by A78; :: thesis: ( p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
A79: lc = <*> the carrier of R by A77;
LC = <*> the carrier of (Polynom-Ring R) by A77, A78;
then Sum LC = 0. (Polynom-Ring R) by RLVECT_1:60
.= p by POLYNOM3:def 12 ;
hence p = Sum LC ; :: thesis: ( p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus p . ((len fm1) -' 1) = 0. R by FUNCOP_1:13
.= Sum lc by A79, RLVECT_1:60 ; :: thesis: len p <= len fm1
thus len p <= len fm1 by POLYNOM4:6; :: thesis: verum
end;
A80: for k being Element of NAT st S6[k] holds
S6[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S6[k] implies S6[k + 1] )
assume A81: S6[k] ; :: thesis: S6[k + 1]
thus S6[k + 1] :: thesis: verum
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ( len lc <= k + 1 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume A82: len lc <= k + 1 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
per cases ( len lc <= k or len lc > k ) ;
suppose len lc <= k ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A81; :: thesis: verum
end;
suppose A83: len lc > k ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then len lc >= k + 1 by NAT_1:13;
then A84: len lc = k + 1 by A82, XXREAL_0:1;
thus ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) :: thesis: verum
proof
per cases ( k = 0 or k > 0 ) ;
suppose A85: k = 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then dom lc = {1} by A84, FINSEQ_1:4, FINSEQ_1:def 3;
then A86: 1 in dom lc by TARSKI:def 1;
A87: lc = <*(lc . 1)*> by A84, A85, FINSEQ_1:57;
consider u, w being Element of R, v being Element of rng (a | (Segm (m + 1))) such that
A88: lc /. 1 = (u * v) * w by A86, IDEAL_1:def 9;
A89: lc . 1 = lc /. 1 by A86, PARTFUN1:def 8;
then consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A90: ( LCT . (lc . 1) = p & p = (x * y) * z & (u * v) * w = p . ((len fm1) -' 1) & len p <= len fm1 & y in F . (m + 1) ) by A68, A88;
consider LC being LinearCombination of FM1 such that
A91: ( LC = LCT * lc & len LC = len lc ) by A69;
A92: LC = <*(LCT . ((u * v) * w))*> by A87, A88, A89, A91, FINSEQ_2:39;
A93: Sum lc = p . ((len fm1) -' 1) by A87, A88, A89, A90, RLVECT_1:61;
Sum LC = p by A88, A89, A90, A92, RLVECT_1:61;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A90, A91, A93; :: thesis: verum
end;
suppose A94: k > 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
not lc is empty by A83;
then consider p being LinearCombination of rng (a | (Segm (m + 1))), e being Element of the carrier of R such that
A95: lc = p ^ <*e*> and
A96: <*e*> is LinearCombination of rng (a | (Segm (m + 1))) by IDEAL_1:32;
len lc = (len p) + (len <*e*>) by A95, FINSEQ_1:35
.= (len p) + 1 by FINSEQ_1:56 ;
then consider LCp being LinearCombination of FM1, sLCp being Polynomial of R such that
A97: ( LCp = LCT * p & sLCp = Sum LCp & sLCp . ((len fm1) -' 1) = Sum p & len sLCp <= len fm1 ) by A81, A84;
len <*e*> = 0 + 1 by FINSEQ_1:56;
then len <*e*> <= k by A94, NAT_1:13;
then consider LCe being LinearCombination of FM1, sLCe being Polynomial of R such that
A98: ( LCe = LCT * <*e*> & sLCe = Sum LCe & sLCe . ((len fm1) -' 1) = Sum <*e*> & len sLCe <= len fm1 ) by A81, A96;
consider LC being LinearCombination of FM1 such that
A99: ( LC = LCT * lc & len LC = len lc ) by A69;
dom LCT = the carrier of R by FUNCT_2:def 1;
then (rng p) \/ (rng <*e*>) c= dom LCT ;
then consider LCTp, LCTe being FinSequence such that
A100: ( LCTp = LCT * p & LCTe = LCT * <*e*> & LCT * (p ^ <*e*>) = LCTp ^ LCTe ) by Th1;
set sLC = sLCp + sLCe;
A101: Sum LC = (Sum LCp) + (Sum LCe) by A95, A97, A98, A99, A100, RLVECT_1:58
.= sLCp + sLCe by A97, A98, POLYNOM3:def 12 ;
A102: Sum lc = (Sum p) + e by A95, FVSUM_1:87
.= (sLCp . ((len fm1) -' 1)) + (sLCe . ((len fm1) -' 1)) by A97, A98, RLVECT_1:61
.= (sLCp + sLCe) . ((len fm1) -' 1) by NORMSP_1:def 5 ;
now
per cases ( len sLCp < len sLCe or len sLCp >= len sLCe ) ;
suppose len sLCp < len sLCe ; :: thesis: len (sLCp + sLCe) <= len fm1
then len (sLCp + sLCe) <= len sLCe by POLYNOM4:9;
hence len (sLCp + sLCe) <= len fm1 by A98, XXREAL_0:2; :: thesis: verum
end;
suppose len sLCp >= len sLCe ; :: thesis: len (sLCp + sLCe) <= len fm1
then len (sLCp + sLCe) <= len sLCp by POLYNOM4:9;
hence len (sLCp + sLCe) <= len fm1 by A97, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A99, A101, A102; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A103: for k being Element of NAT holds S6[k] from NAT_1:sch 1(A76, A80);
 let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
consider n being Element of NAT such that
A104: n = len lc ;
thus ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A103, A104; :: thesis: verum
end;
then consider LC being LinearCombination of FM1, sLC being Polynomial of R such that
A105: ( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) ;
set f' = fm1 - sLC;
A106: (fm1 - sLC) + sLC = fm1 + (sLC + (- sLC)) by POLYNOM3:26
.= fm1 + (sLC - sLC)
.= fm1 + (0_. R) by POLYNOM3:30
.= fm1 by POLYNOM3:29 ;
len (- sLC) <= len fm1 by A105, POLYNOM4:11;
then A107: len (fm1 - sLC) <= len fm1 by POLYNOM4:9;
now
assume A108: len (fm1 - sLC) = len fm1 ; :: thesis: contradiction
(len fm1) - 1 >= 0 by A46;
then A109: ((len fm1) -' 1) + 1 = ((len fm1) - 1) + 1 by XREAL_0:def 2
.= len fm1 ;
consider n being Element of NAT , A being Polynomial of R such that
A110: ( n = m + 1 & A = f . n & a . (m + 1) = A . ((len A) -' 1) ) by A43;
(fm1 - sLC) . ((len fm1) -' 1) = (fm1 . ((len fm1) -' 1)) - (fm1 . ((len fm1) -' 1)) by A45, A105, A110, POLYNOM3:27
.= 0. R by RLVECT_1:28 ;
hence contradiction by A108, A109, ALGSEQ_1:25; :: thesis: verum
end;
then A111: len (fm1 - sLC) < len fm1 by A107, XXREAL_0:1;
A112: sLC in FM1 -Ideal by A105, IDEAL_1:60;
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A113: ( A = F . n & B = I \ (A -Ideal ) & n = m + 1 & F . (n + 1) = (F . n) \/ {(f . (m + 1))} & f . (m + 1) in minlen B ) by A25;
A114: now
assume A115: fm1 - sLC in FM1 -Ideal ; :: thesis: contradiction
reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 12;
reconsider f' = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 12;
f . (m + 1) = f' + sLC by A106, POLYNOM3:def 12;
then fm1 in FM1 -Ideal by A112, A115, IDEAL_1:def 1;
hence contradiction by A113, XBOOLE_0:def 5; :: thesis: verum
end;
fm1 - sLC in I
proof
FM1 is Subset of I by A13;
then FM1 -Ideal c= I -Ideal by IDEAL_1:57;
then A116: FM1 -Ideal c= I by IDEAL_1:44;
reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 12;
reconsider f' = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 12;
A117: f . (m + 1) in I by A113, XBOOLE_0:def 5;
f' = (f . (m + 1)) - sLC by Th16;
hence fm1 - sLC in I by A112, A116, A117, IDEAL_1:15; :: thesis: verum
end;
then fm1 - sLC in I \ (FM1 -Ideal ) by A114, XBOOLE_0:def 5;
hence contradiction by A111, A113, Th17; :: thesis: verum
end;
hence Polynom-Ring R is Noetherian ; :: thesis: verum