:: by Jonathan Backer and Piotr Rudnicki

::

:: Received November 27, 2000

:: Copyright (c) 2000-2017 Association of Mizar Users

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 )

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 )

proof end;

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 & b29 = b2 | i & b1 divides b2 holds

b19 divides b29

for b1, b2 being bag of j

for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds

b19 divides b29

proof end;

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 & b29 = b2 | i holds

( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )

for b1, b2 being bag of j

for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i holds

( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )

proof end;

definition

let n, k be Nat;

let b be bag of n;

ex b_{1} being Element of Bags (n + 1) st

( b_{1} | n = b & b_{1} . n = k )

for b_{1}, b_{2} being Element of Bags (n + 1) st b_{1} | n = b & b_{1} . n = k & b_{2} | n = b & b_{2} . n = k holds

b_{1} = b_{2}

end;
let b be bag of n;

func b bag_extend k -> Element of Bags (n + 1) means :Def1: :: HILBASIS:def 1

( it | n = b & it . n = k );

existence ( it | n = b & it . n = k );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines bag_extend HILBASIS:def 1 :

for n, k being Nat

for b being bag of n

for b_{4} being Element of Bags (n + 1) holds

( b_{4} = b bag_extend k iff ( b_{4} | n = b & b_{4} . n = k ) );

for n, k being Nat

for b being bag of n

for b

( b

definition

let X be set ;

let x be Element of X;

coherence

(EmptyBag X) +* (x,1) is Element of Bags X by PRE_POLY:def 12;

end;
let x be Element of X;

coherence

(EmptyBag X) +* (x,1) is Element of Bags X by PRE_POLY:def 12;

:: deftheorem defines UnitBag HILBASIS:def 2 :

for X being set

for x being Element of X holds UnitBag x = (EmptyBag X) +* (x,1);

for X being set

for x being Element of X holds UnitBag x = (EmptyBag X) +* (x,1);

theorem Th9: :: HILBASIS:9

for X being non empty set

for x being Element of X holds

( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds

(UnitBag x) . y = 0 ) )

for x being Element of X holds

( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds

(UnitBag x) . y = 0 ) )

proof end;

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

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

proof end;

definition

let X be set ;

let x be Element of X;

let L be non empty unital multLoopStr_0 ;

coherence

(0_ (X,L)) +* ((UnitBag x),(1_ L)) is Series of X,L ;

end;
let x be Element of X;

let L be non empty unital multLoopStr_0 ;

coherence

(0_ (X,L)) +* ((UnitBag x),(1_ L)) is Series of X,L ;

:: 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));

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 & ( for b being bag of X st b <> UnitBag x holds

(1_1 (x,L)) . b = 0. L ) )

for L being non trivial unital doubleLoopStr

for x being Element of X holds

( (1_1 (x,L)) . (UnitBag x) = 1_ L & ( for b being bag of X st b <> UnitBag x holds

(1_1 (x,L)) . b = 0. L ) )

proof end;

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)}

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)}

proof end;

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 ;

coherence

1_1 (x,L) is finite-Support

end;
let x be Element of X;

let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ;

coherence

1_1 (x,L) is finite-Support

proof 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

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

proof end;

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

for x being Element of (Polynom-Ring L)

for p being sequence of L st x = p holds

- x = - p

proof end;

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 & y = q holds

x - y = p - q

for x, y being Element of (Polynom-Ring L)

for p, q being sequence of L st x = p & y = q holds

x - y = p - q

proof end;

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);

{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } is non empty Subset of I

end;
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 & 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 & y9 in I holds

len x9 <= len y9 } ;

{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds

len x9 <= len y9 } is non empty Subset of I

proof 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 & y9 in I holds

len x9 <= len y9 } ;

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 & 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 & i2 in I holds

( i1 in I & len i1 <= len i2 )

for I being non empty Subset of (Polynom-Ring L)

for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds

( i1 in I & len i1 <= len i2 )

proof end;

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;

ex b_{1} being Polynomial of L st

for x being Nat holds

( ( x = n implies b_{1} . x = a ) & ( x <> n implies b_{1} . x = 0. L ) )

for b_{1}, b_{2} being Polynomial of L st ( for x being Nat holds

( ( x = n implies b_{1} . x = a ) & ( x <> n implies b_{1} . x = 0. L ) ) ) & ( for x being Nat holds

( ( x = n implies b_{2} . x = a ) & ( x <> n implies b_{2} . x = 0. L ) ) ) holds

b_{1} = b_{2}

end;
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 ) & ( x <> n implies it . x = 0. L ) );

existence for x being Nat holds

( ( x = n implies it . x = a ) & ( x <> n implies it . x = 0. L ) );

ex b

for x being Nat holds

( ( x = n implies b

proof end;

uniqueness for b

( ( x = n implies b

( ( x = n implies b

b

proof 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 b_{4} being Polynomial of L holds

( b_{4} = monomial (a,n) iff for x being Nat holds

( ( x = n implies b_{4} . x = a ) & ( x <> n implies b_{4} . x = 0. L ) ) );

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 b

( b

( ( x = n implies b

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 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )

for n being Element of NAT

for a being Element of L holds

( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )

proof end;

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)

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)

proof end;

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

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

proof end;

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

for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1

proof end;

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

for I being Ideal of R

for P being Function of R,S st P is RingIsomorphism holds

P .: I is Ideal of S

proof end;

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

for f being Function of R,S st f is RingHomomorphism holds

f . (0. R) = 0. S

proof end;

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 & len lc = len LC & E represents lc & ( 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

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 & len lc = len LC & E represents lc & ( 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

proof end;

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

for P being Function of R,S st P is RingIsomorphism holds

P " is RingIsomorphism

proof end;

theorem Th26: :: HILBASIS:26

for R, S being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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

proof end;

theorem Th27: :: HILBASIS:27

for R, S being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds

S is Noetherian

for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds

S is Noetherian

proof end;

theorem Th28: :: HILBASIS:28

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

proof end;

theorem Th29: :: HILBASIS:29

for R being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for n being 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 ) & p1 . b = Sum (g * F) )

for n being 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 ) & p1 . b = Sum (g * F) )

proof end;

definition

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;

let n be Nat;

ex b_{1} 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 = b_{1} . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n)

for b_{1}, b_{2} 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 = b_{1} . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) & ( 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 = b_{2} . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) holds

b_{1} = b_{2}

end;
let n be 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 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n);

existence 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 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n);

ex b

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

p3 . b = p2 . (b | n)

proof end;

uniqueness for b

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = b

p3 . b = p2 . (b | n) ) & ( 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 = b

p3 . b = p2 . (b | n) ) holds

b

proof end;

:: deftheorem Def6 defines upm HILBASIS:def 6 :

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for n being Nat

for b_{3} being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) holds

( b_{3} = 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 = b_{3} . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) );

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for n being Nat

for b

( b

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = b

p3 . b = p2 . (b | n) );

registration

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;

let n be Nat;

coherence

upm (n,R) is additive

upm (n,R) is multiplicative

upm (n,R) is unity-preserving

upm (n,R) is one-to-one

end;
let n be Nat;

coherence

upm (n,R) is additive

proof end;

coherence upm (n,R) is multiplicative

proof end;

coherence upm (n,R) is unity-preserving

proof end;

coherence upm (n,R) is one-to-one

proof end;

definition

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;

let n be Nat;

ex b_{1} 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 = b_{1} . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i)

for b_{1}, b_{2} 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 = b_{1} . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) & ( 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 = b_{2} . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) holds

b_{1} = b_{2}

end;
let n be 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 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i);

existence 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 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i);

ex b

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

p2 . b = p1 . (b bag_extend i)

proof end;

uniqueness for b

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

p2 . b = p1 . (b bag_extend i) ) & ( 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 = b

p2 . b = p1 . (b bag_extend i) ) holds

b

proof end;

:: deftheorem Def7 defines mpu HILBASIS:def 7 :

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for n being Nat

for b_{3} being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) holds

( b_{3} = 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 = b_{3} . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) );

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for n being Nat

for b

( b

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

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 well-unital distributive associative commutative doubleLoopStr

for n being Nat

for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

for n being Nat

for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

proof end;

theorem Th31: :: HILBASIS:31

for R being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for n being Nat ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism

for n being Nat ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism

proof end;

registration

let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative Noetherian doubleLoopStr ;

coherence

Polynom-Ring R is Noetherian

end;
coherence

Polynom-Ring R is Noetherian

proof end;

theorem Th32: :: HILBASIS:32

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr st R is Noetherian holds

for n being Nat holds Polynom-Ring (n,R) is Noetherian

for n being Nat holds Polynom-Ring (n,R) is Noetherian

proof end;

theorem :: HILBASIS:35

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr

for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian

for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian

proof end;