:: Hilbert Basis Theorem
:: by Jonathan Backer and Piotr Rudnicki
::
:: Received November 27, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: HILBASIS:1
for A, B being FinSequence
for f being Function st (rng A) \/ (rng B) c= dom f holds
ex fA, fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
proofend;

theorem Th2: :: HILBASIS:2
for b being bag of 0 holds decomp b = <*<*{},{}*>*>
proofend;

theorem Th3: :: HILBASIS:3
for i, j being Element of NAT
for b being bag of j st i <= j holds
b | i is Element of Bags i
proofend;

theorem Th4: :: HILBASIS:4
for i, j being set
for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i &amp; b29 = b2 | i &amp; b1 divides b2 holds
b19 divides b29
proofend;

theorem Th5: :: HILBASIS:5
for i, j being set
for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i &amp; b29 = b2 | i holds
( (b1 -' b2) | i = b19 -' b29 &amp; (b1 + b2) | i = b19 + b29 )
proofend;

definition
let n, k be Nat;
let b be bag of n;
funcb bag_extend k ->  Element of Bags (n + 1) means :Def1: :: HILBASIS:def 1
( it | n = b &amp; it . n = k );
existence
 ex b1 being Element of Bags (n + 1) st
( b1 | n = b &amp; b1 . n = k )
proofend;
uniqueness
 for b1, b2 being Element of Bags (n + 1) st b1 | n = b &amp; b1 . n = k &amp; b2 | n = b &amp; b2 . n = k holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines bag_extend HILBASIS:def_1_:_
 for n, k being Nat
for b being bag of n
for b4 being Element of Bags (n + 1) holds
( b4 = b bag_extend k iff ( b4 | n = b &amp; b4 . n = k ) );

theorem Th6: :: HILBASIS:6
for n being Element of NAT holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0
proofend;

theorem Th7: :: HILBASIS:7
for n being Ordinal
for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
proofend;

definition
let X be set ;
let x be Element of X;
func UnitBag x ->  Element of Bags X equals :: HILBASIS:def 2
(EmptyBag X) +* (x,1);
coherence
 (EmptyBag X) +* (x,1) is Element of Bags X by PRE_POLY:def_12;
end;

:: deftheorem  defines UnitBag HILBASIS:def_2_:_
 for X being set
for x being Element of X holds UnitBag x = (EmptyBag X) +* (x,1);

theorem Th8: :: HILBASIS:8
for X being non empty set
for x being Element of X holds support (UnitBag x) = {x}
proofend;

theorem Th9: :: HILBASIS:9
for X being non empty set
for x being Element of X holds
( (UnitBag x) . x = 1 &amp; ( for y being Element of X st x <> y holds
(UnitBag x) . y = 0 ) )
proofend;

theorem Th10: :: HILBASIS:10
for X being non empty set
for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds
x1 = x2
proofend;

theorem Th11: :: HILBASIS:11
for X being non empty Ordinal
for x being Element of X
for L being non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval ((UnitBag x),e) = e . x
proofend;

definition
let X be set ;
let x be Element of X;
let L be non empty unital multLoopStr_0 ;
func 1_1 (x,L) ->  Series of X,L equals :: HILBASIS:def 3
(0_ (X,L)) +* ((UnitBag x),(1_ L));
coherence
 (0_ (X,L)) +* ((UnitBag x),(1_ L)) is Series of X,L ;
end;

:: deftheorem  defines 1_1 HILBASIS:def_3_:_
 for X being set
for x being Element of X
for L being non empty unital multLoopStr_0 holds 1_1 (x,L) = (0_ (X,L)) +* ((UnitBag x),(1_ L));

theorem Th12: :: HILBASIS:12
for X being set
for L being non trivial unital doubleLoopStr
for x being Element of X holds
( (1_1 (x,L)) . (UnitBag x) = 1_ L &amp; ( for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L ) )
proofend;

theorem Th13: :: HILBASIS:13
for X being set
for x being Element of X
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
proofend;

registration
let X be Ordinal;
let x be Element of X;
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ;
cluster 1_1 (x,L) ->  finite-Support ;
coherence
 1_1 (x,L) is finite-Support
proofend;
end;

theorem Th14: :: HILBASIS:14
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for X being non empty set
for x1, x2 being Element of X st 1_1 (x1,L) = 1_1 (x2,L) holds
x1 = x2
proofend;

theorem Th15: :: HILBASIS:15
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x being Element of (Polynom-Ring L)
for p being sequence of L st x = p holds
- x = - p
proofend;

theorem Th16: :: HILBASIS:16
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x, y being Element of (Polynom-Ring L)
for p, q being sequence of L st x = p &amp; y = q holds
x - y = p - q
proofend;

definition
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let I be non empty Subset of (Polynom-Ring L);
func minlen I ->  non empty Subset of I equals :: HILBASIS:def 4
 {  x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x &amp; y9 in I holds
len x9 <= len y9  }  ;
coherence
  {  x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x &amp; y9 in I holds
len x9 <= len y9  }  is non empty Subset of I
proofend;
end;

:: deftheorem  defines minlen HILBASIS:def_4_:_
 for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for I being non empty Subset of (Polynom-Ring L) holds minlen I =  {  x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x &amp; y9 in I holds
len x9 <= len y9  }  ;

theorem Th17: :: HILBASIS:17
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for I being non empty Subset of (Polynom-Ring L)
for i1, i2 being Polynomial of L st i1 in minlen I &amp; i2 in I holds
( i1 in I &amp; len i1 <= len i2 )
proofend;

definition
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let n be Nat;
let a be Element of L;
func monomial (a,n) ->  Polynomial of L means :Def5: :: HILBASIS:def 5
 for x being Nat holds
( ( x = n implies it . x = a ) &amp; ( x <> n implies it . x = 0. L ) );
existence
 ex b1 being Polynomial of L st
for x being Nat holds
( ( x = n implies b1 . x = a ) &amp; ( x <> n implies b1 . x = 0. L ) )
proofend;
uniqueness
 for b1, b2 being Polynomial of L st ( for x being Nat holds
( ( x = n implies b1 . x = a ) &amp; ( x <> n implies b1 . x = 0. L ) ) ) &amp; ( for x being Nat holds
( ( x = n implies b2 . x = a ) &amp; ( x <> n implies b2 . x = 0. L ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines monomial HILBASIS:def_5_:_
 for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Nat
for a being Element of L
for b4 being Polynomial of L holds
( b4 = monomial (a,n) iff for x being Nat holds
( ( x = n implies b4 . x = a ) &amp; ( x <> n implies b4 . x = 0. L ) ) );

theorem Th18: :: HILBASIS:18
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Element of NAT
for a being Element of L holds
( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) &amp; ( a = 0. L implies len (monomial (a,n)) = 0 ) &amp; len (monomial (a,n)) <= n + 1 )
proofend;

theorem Th19: :: HILBASIS:19
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
proofend;

theorem Th20: :: HILBASIS:20
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
proofend;

theorem Th21: :: HILBASIS:21
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1
proofend;

begin

theorem Th22: :: HILBASIS:22
for R, S being non empty doubleLoopStr
for I being Ideal of R
for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
proofend;

theorem Th23: :: HILBASIS:23
for R, S being non empty right_complementable add-associative right_zeroed doubleLoopStr
for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
proofend;

theorem Th24: :: HILBASIS:24
for R, S being non empty right_complementable add-associative right_zeroed doubleLoopStr
for F being non empty Subset of R
for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism &amp; len lc = len LC &amp; E represents lc &amp; ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
proofend;

theorem Th25: :: HILBASIS:25
for R, S being non empty doubleLoopStr
for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism
proofend;

theorem Th26: :: HILBASIS:26
for R, S being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for F being non empty Subset of R
for P being Function of R,S st P is RingIsomorphism holds
P .: (F -Ideal) = (P .: F) -Ideal
proofend;

theorem Th27: :: HILBASIS:27
for R, S being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for P being Function of R,S st P is RingIsomorphism &amp; R is Noetherian holds
S is Noetherian
proofend;

theorem Th28: :: HILBASIS:28
for R being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism
proofend;

theorem Th29: :: HILBASIS:29
for R being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Element of NAT
for b being bag of n
for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) &amp; p1 . b = Sum (g * F) )
proofend;

definition
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of NAT ;
func upm (n,R) ->  Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) means :Def6: :: HILBASIS:def 6
 for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = it . p1 &amp; p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n);
existence
 ex b1 being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st
for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 &amp; p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
proofend;
uniqueness
 for b1, b2 being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st ( for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 &amp; p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) &amp; ( for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b2 . p1 &amp; p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines upm HILBASIS:def_6_:_
 for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT
for b3 being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) holds
( b3 = upm (n,R) iff for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b3 . p1 &amp; p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) );

registration
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of NAT ;
cluster upm (n,R) ->  additive ;
coherence
 upm (n,R) is additive
proofend;
cluster upm (n,R) ->  multiplicative ;
coherence
 upm (n,R) is multiplicative
proofend;
cluster upm (n,R) ->  unity-preserving ;
coherence
 upm (n,R) is unity-preserving
proofend;
cluster upm (n,R) ->  one-to-one ;
coherence
 upm (n,R) is one-to-one
proofend;
end;

definition
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of NAT ;
func mpu (n,R) ->  Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) means :Def7: :: HILBASIS:def 7
 for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = it . p1 &amp; p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i);
existence
 ex b1 being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) st
for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b1 . p1 &amp; p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
proofend;
uniqueness
 for b1, b2 being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) st ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b1 . p1 &amp; p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) &amp; ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b2 . p1 &amp; p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines mpu HILBASIS:def_7_:_
 for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT
for b3 being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) holds
( b3 = mpu (n,R) iff for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b3 . p1 &amp; p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) );

theorem Th30: :: HILBASIS:30
for R being non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT
for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p
proofend;

theorem Th31: :: HILBASIS:31
for R being non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism
proofend;

begin

registration
let R be non empty right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive Noetherian doubleLoopStr ;
cluster Polynom-Ring R ->  Noetherian ;
coherence
 Polynom-Ring R is Noetherian
proofend;
end;

theorem Th32: :: HILBASIS:32
for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr st R is Noetherian holds
for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian
proofend;

theorem Th33: :: HILBASIS:33
for F being Field holds F is Noetherian
proofend;

theorem :: HILBASIS:34
for F being Field
for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian
proofend;

theorem :: HILBASIS:35
for R being 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
proofend;