:: HILBASIS semantic presentation 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 ) proof let A, B be FinSequence; ::_thesis: 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 ) let f be Function; ::_thesis: ( (rng A) \/ (rng B) c= dom f implies ex fA, fB being FinSequence st ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) ) assume A1: (rng A) \/ (rng B) c= dom f ; ::_thesis: ex fA, fB being FinSequence st ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) then A2: rng (A ^ B) c= dom f by FINSEQ_1:31; then reconsider fAB = f * (A ^ B) as FinSequence by FINSEQ_1:16; A3: rng B c= (rng A) \/ (rng B) by XBOOLE_1:7; then reconsider fB = f * B as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1; A4: dom (f * B) = dom B by A1, A3, RELAT_1:27, XBOOLE_1:1; then A5: len fB = len B by FINSEQ_3:29; A6: rng A c= (rng A) \/ (rng B) by XBOOLE_1:7; then reconsider fA = f * A as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1; take fA ; ::_thesis: ex fB being FinSequence st ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) take fB ; ::_thesis: ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) A7: dom (f * (A ^ B)) = dom (A ^ B) by A2, RELAT_1:27; A8: dom (f * A) = dom A by A1, A6, RELAT_1:27, XBOOLE_1:1; then A9: len fA = len A by FINSEQ_3:29; A10: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_fAB_holds_ (fA_^_fB)_._k_=_fAB_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len fAB implies (fA ^ fB) . b1 = fAB . b1 ) assume ( 1 <= k & k <= len fAB ) ; ::_thesis: (fA ^ fB) . b1 = fAB . b1 then A11: k in dom fAB by FINSEQ_3:25; percases ( k in dom fA or not k in dom fA ) ; supposeA12: k in dom fA ; ::_thesis: (fA ^ fB) . b1 = fAB . b1 hence (fA ^ fB) . k = fA . k by FINSEQ_1:def_7 .= f . (A . k) by A12, FUNCT_1:12 .= f . ((A ^ B) . k) by A8, A12, FINSEQ_1:def_7 .= fAB . k by A11, FUNCT_1:12 ; ::_thesis: verum end; suppose not k in dom fA ; ::_thesis: fAB . b1 = (fA ^ fB) . b1 then consider n being Nat such that A13: n in dom B and A14: k = (len A) + n by A8, A7, A11, FINSEQ_1:25; thus fAB . k = f . ((A ^ B) . k) by A11, FUNCT_1:12 .= f . (B . n) by A13, A14, FINSEQ_1:def_7 .= fB . n by A4, A13, FUNCT_1:12 .= (fA ^ fB) . k by A9, A4, A13, A14, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; len fAB = len (A ^ B) by A7, FINSEQ_3:29 .= (len fA) + (len fB) by A9, A5, FINSEQ_1:22 .= len (fA ^ fB) by FINSEQ_1:22 ; hence ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) by A10, FINSEQ_1:14; ::_thesis: verum end; theorem Th2: :: HILBASIS:2 for b being bag of 0 holds decomp b = <*<*{},{}*>*> proof let b be bag of 0 ; ::_thesis: decomp b = <*<*{},{}*>*> A1: EmptyBag {} = {} --> 0 ; then divisors b = <*{}*> by PRE_POLY:67; then A2: len (divisors b) = 1 by FINSEQ_1:39; A3: dom (divisors b) = dom (decomp b) by PRE_POLY:def_17; then 1 in dom (decomp b) by A2, FINSEQ_3:25; then A4: (decomp b) . 1 = (decomp b) /. 1 by PARTFUN1:def_6 .= <*{},{}*> by A1, PRE_POLY:71 ; len (decomp b) = 1 by A2, A3, FINSEQ_3:29; hence decomp b = <*<*{},{}*>*> by A4, FINSEQ_1:40; ::_thesis: verum end; 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 proof let i, j be Element of NAT ; ::_thesis: for b being bag of j st i <= j holds b | i is Element of Bags i let b be bag of j; ::_thesis: ( i <= j implies b | i is Element of Bags i ) assume A1: i <= j ; ::_thesis: b | i is Element of Bags i i c= j proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in i or x in j ) assume x in i ; ::_thesis: x in j then x in { y where y is Element of NAT : y < i } by AXIOMS:4; then consider x9 being Element of NAT such that A2: x9 = x and A3: x9 < i ; x9 < j by A1, A3, XXREAL_0:2; then x9 in { y where y is Element of NAT : y < j } ; hence x in j by A2, AXIOMS:4; ::_thesis: verum end; hence b | i is Element of Bags i by PRE_POLY:def_12; ::_thesis: verum 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 proof let i, j be set ; ::_thesis: 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 let b1, b2 be bag of j; ::_thesis: for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds b19 divides b29 let b19, b29 be bag of i; ::_thesis: ( b19 = b1 | i & b29 = b2 | i & b1 divides b2 implies b19 divides b29 ) assume that A1: ( b19 = b1 | i & b29 = b2 | i ) and A2: b1 divides b2 ; ::_thesis: b19 divides b29 now__::_thesis:_for_k_being_set_holds_b19_._k_<=_b29_._k let k be set ; ::_thesis: b19 . b1 <= b29 . b1 A3: dom b19 = i by PARTFUN1:def_2 .= dom b29 by PARTFUN1:def_2 ; percases ( not k in dom b19 or k in dom b19 ) ; supposeA4: not k in dom b19 ; ::_thesis: b19 . b1 <= b29 . b1 then b19 . k = {} by FUNCT_1:def_2 .= b29 . k by A3, A4, FUNCT_1:def_2 ; hence b19 . k <= b29 . k ; ::_thesis: verum end; suppose k in dom b19 ; ::_thesis: b19 . b1 <= b29 . b1 then ( b19 . k = b1 . k & b29 . k = b2 . k ) by A1, A3, FUNCT_1:47; hence b19 . k <= b29 . k by A2, PRE_POLY:def_11; ::_thesis: verum end; end; end; hence b19 divides b29 by PRE_POLY:def_11; ::_thesis: verum 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 ) proof let i, j be set ; ::_thesis: 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 ) let b1, b2 be bag of j; ::_thesis: 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 ) let b19, b29 be bag of i; ::_thesis: ( b19 = b1 | i & b29 = b2 | i implies ( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 ) ) assume that A1: b19 = b1 | i and A2: b29 = b2 | i ; ::_thesis: ( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 ) dom b1 = j by PARTFUN1:def_2; then A3: dom (b1 | i) = j /\ i by RELAT_1:61; dom b2 = j by PARTFUN1:def_2; then A4: dom (b2 | i) = j /\ i by RELAT_1:61; dom (b1 + b2) = j by PARTFUN1:def_2; then A5: dom ((b1 + b2) | i) = j /\ i by RELAT_1:61; A6: now__::_thesis:_for_x_being_set_st_x_in_j_/\_i_holds_ ((b1_+_b2)_|_i)_._x_=_(b19_+_b29)_._x let x be set ; ::_thesis: ( x in j /\ i implies ((b1 + b2) | i) . x = (b19 + b29) . x ) assume A7: x in j /\ i ; ::_thesis: ((b1 + b2) | i) . x = (b19 + b29) . x hence ((b1 + b2) | i) . x = (b1 + b2) . x by A5, FUNCT_1:47 .= (b1 . x) + (b2 . x) by PRE_POLY:def_5 .= (b19 . x) + (b2 . x) by A1, A3, A7, FUNCT_1:47 .= (b19 . x) + (b29 . x) by A2, A4, A7, FUNCT_1:47 .= (b19 + b29) . x by PRE_POLY:def_5 ; ::_thesis: verum end; dom (b1 -' b2) = j by PARTFUN1:def_2; then A8: dom ((b1 -' b2) | i) = j /\ i by RELAT_1:61; A9: now__::_thesis:_for_x_being_set_st_x_in_j_/\_i_holds_ ((b1_-'_b2)_|_i)_._x_=_(b19_-'_b29)_._x let x be set ; ::_thesis: ( x in j /\ i implies ((b1 -' b2) | i) . x = (b19 -' b29) . x ) assume A10: x in j /\ i ; ::_thesis: ((b1 -' b2) | i) . x = (b19 -' b29) . x hence ((b1 -' b2) | i) . x = (b1 -' b2) . x by A8, FUNCT_1:47 .= (b1 . x) -' (b2 . x) by PRE_POLY:def_6 .= (b19 . x) -' (b2 . x) by A1, A3, A10, FUNCT_1:47 .= (b19 . x) -' (b29 . x) by A2, A4, A10, FUNCT_1:47 .= (b19 -' b29) . x by PRE_POLY:def_6 ; ::_thesis: verum end; dom (b19 -' b29) = i by PARTFUN1:def_2 .= j /\ i by A1, A3, PARTFUN1:def_2 ; hence (b1 -' b2) | i = b19 -' b29 by A8, A9, FUNCT_1:2; ::_thesis: (b1 + b2) | i = b19 + b29 dom (b19 + b29) = i by PARTFUN1:def_2 .= j /\ i by A1, A3, PARTFUN1:def_2 ; hence (b1 + b2) | i = b19 + b29 by A5, A6, FUNCT_1:2; ::_thesis: verum end; 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 & it . n = k ); existence ex b1 being Element of Bags (n + 1) st ( b1 | n = b & b1 . n = k ) proof set b1 = b +* (n .--> k); A1: dom b = n by PARTFUN1:def_2; A2: dom (b +* (n .--> k)) = (dom b) \/ (dom (n .--> k)) by FUNCT_4:def_1 .= (dom b) \/ {n} by FUNCOP_1:13 .= n \/ {n} by PARTFUN1:def_2 .= succ n by ORDINAL1:def_1 .= n + 1 by NAT_1:38 ; then b +* (n .--> k) is ManySortedSet of n + 1 by PARTFUN1:def_2, RELAT_1:def_18; then reconsider b1 = b +* (n .--> k) as Element of Bags (n + 1) by PRE_POLY:def_12; take b1 ; ::_thesis: ( b1 | n = b & b1 . n = k ) A3: dom (b1 | n) = (n + 1) /\ n by A2, RELAT_1:61 .= (succ n) /\ n by NAT_1:38 .= (n \/ {n}) /\ n by ORDINAL1:def_1 .= n by XBOOLE_1:21 ; now__::_thesis:_for_x_being_set_st_x_in_n_holds_ (b1_|_n)_._x_=_b_._x let x be set ; ::_thesis: ( x in n implies (b1 | n) . x = b . x ) assume A4: x in n ; ::_thesis: (b1 | n) . x = b . x then A5: x in (dom b) \/ (dom (n .--> k)) by A1, XBOOLE_0:def_3; A6: now__::_thesis:_not_x_in_dom_(n_.-->_k) assume x in dom (n .--> k) ; ::_thesis: contradiction then x in {n} ; then x = n by TARSKI:def_1; hence contradiction by A4; ::_thesis: verum end; thus (b1 | n) . x = b1 . x by A3, A4, FUNCT_1:47 .= b . x by A5, A6, FUNCT_4:def_1 ; ::_thesis: verum end; hence b1 | n = b by A3, A1, FUNCT_1:2; ::_thesis: b1 . n = k n in {n} by TARSKI:def_1; then A7: n in dom (n .--> k) by FUNCOP_1:13; then n in (dom b) \/ (dom (n .--> k)) by XBOOLE_0:def_3; hence b1 . n = (n .--> k) . n by A7, FUNCT_4:def_1 .= k by FUNCOP_1:72 ; ::_thesis: verum end; uniqueness for b1, b2 being Element of Bags (n + 1) st b1 | n = b & b1 . n = k & b2 | n = b & b2 . n = k holds b1 = b2 proof let b1, b2 be Element of Bags (n + 1); ::_thesis: ( b1 | n = b & b1 . n = k & b2 | n = b & b2 . n = k implies b1 = b2 ) assume that A8: b1 | n = b and A9: b1 . n = k and A10: b2 | n = b and A11: b2 . n = k ; ::_thesis: b1 = b2 A12: dom b1 = n + 1 by PARTFUN1:def_2; A13: now__::_thesis:_for_x_being_set_st_x_in_n_+_1_holds_ b1_._x_=_b2_._x let x be set ; ::_thesis: ( x in n + 1 implies b1 . b1 = b2 . b1 ) assume A14: x in n + 1 ; ::_thesis: b1 . b1 = b2 . b1 then x in succ n by NAT_1:38; then A15: x in n \/ {n} by ORDINAL1:def_1; percases ( x in {n} or not x in {n} ) ; suppose x in {n} ; ::_thesis: b1 . b1 = b2 . b1 then x = n by TARSKI:def_1; hence b1 . x = b2 . x by A9, A11; ::_thesis: verum end; suppose not x in {n} ; ::_thesis: b1 . b1 = b2 . b1 then x in n by A15, XBOOLE_0:def_3; then x in (n + 1) /\ n by A14, XBOOLE_0:def_4; then A16: x in dom b by A8, A12, RELAT_1:61; hence b1 . x = b . x by A8, FUNCT_1:47 .= b2 . x by A10, A16, FUNCT_1:47 ; ::_thesis: verum end; end; end; dom b2 = n + 1 by PARTFUN1:def_2; hence b1 = b2 by A12, A13, FUNCT_1:2; ::_thesis: verum end; 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 & b4 . n = k ) ); theorem Th6: :: HILBASIS:6 for n being Element of NAT holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 proof let n be Element of NAT ; ::_thesis: EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 A1: now__::_thesis:_for_x_being_set_st_x_in_n_+_1_holds_ (EmptyBag_(n_+_1))_._x_=_((EmptyBag_n)_bag_extend_0)_._x let x be set ; ::_thesis: ( x in n + 1 implies (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1 ) assume x in n + 1 ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1 then x in succ n by NAT_1:38; then A2: x in n \/ {n} by ORDINAL1:def_1; percases ( x in n or x in {n} ) by A2, XBOOLE_0:def_3; supposeA3: x in n ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1 thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52 .= (EmptyBag n) . x by PRE_POLY:52 .= (((EmptyBag n) bag_extend 0) | n) . x by Def1 .= ((EmptyBag n) bag_extend 0) . x by A3, FUNCT_1:49 ; ::_thesis: verum end; supposeA4: x in {n} ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1 thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52 .= ((EmptyBag n) bag_extend 0) . n by Def1 .= ((EmptyBag n) bag_extend 0) . x by A4, TARSKI:def_1 ; ::_thesis: verum end; end; end; ( dom (EmptyBag (n + 1)) = n + 1 & dom ((EmptyBag n) bag_extend 0) = n + 1 ) by PARTFUN1:def_2; hence EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 by A1, FUNCT_1:2; ::_thesis: verum end; 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 ) proof let n be Ordinal; ::_thesis: for b, b1 being bag of n holds ( b1 in rng (divisors b) iff b1 divides b ) let b, b1 be bag of n; ::_thesis: ( b1 in rng (divisors b) iff b1 divides b ) consider S being non empty finite Subset of (Bags n) such that A1: divisors b = SgmX ((BagOrder n),S) and A2: for p being bag of n holds ( p in S iff p divides b ) by PRE_POLY:def_16; field (BagOrder n) = Bags n by ORDERS_1:15; then A3: BagOrder n linearly_orders S by ORDERS_1:37, ORDERS_1:38; hereby ::_thesis: ( b1 divides b implies b1 in rng (divisors b) ) assume b1 in rng (divisors b) ; ::_thesis: b1 divides b then b1 in S by A1, A3, PRE_POLY:def_2; hence b1 divides b by A2; ::_thesis: verum end; assume b1 divides b ; ::_thesis: b1 in rng (divisors b) then b1 in S by A2; hence b1 in rng (divisors b) by A1, A3, PRE_POLY:def_2; ::_thesis: verum end; 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} proof let X be non empty set ; ::_thesis: for x being Element of X holds support (UnitBag x) = {x} let x be Element of X; ::_thesis: support (UnitBag x) = {x} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_support_(UnitBag_x)_implies_a_in_{x}_)_&_(_a_in_{x}_implies_a_in_support_(UnitBag_x)_)_) let a be set ; ::_thesis: ( ( a in support (UnitBag x) implies a in {x} ) & ( a in {x} implies a in support (UnitBag x) ) ) hereby ::_thesis: ( a in {x} implies a in support (UnitBag x) ) assume A1: a in support (UnitBag x) ; ::_thesis: a in {x} now__::_thesis:_not_a_<>_x assume a <> x ; ::_thesis: contradiction then ((EmptyBag X) +* (x,1)) . a = (EmptyBag X) . a by FUNCT_7:32 .= 0 by PRE_POLY:52 ; hence contradiction by A1, PRE_POLY:def_7; ::_thesis: verum end; hence a in {x} by TARSKI:def_1; ::_thesis: verum end; EmptyBag X = X --> 0 by PRE_POLY:def_13; then A2: dom (EmptyBag X) = X by FUNCOP_1:13; assume a in {x} ; ::_thesis: a in support (UnitBag x) then a = x by TARSKI:def_1; then (UnitBag x) . a = 1 by A2, FUNCT_7:31; hence a in support (UnitBag x) by PRE_POLY:def_7; ::_thesis: verum end; hence support (UnitBag x) = {x} by TARSKI:1; ::_thesis: verum end; 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 ) ) proof let X be non empty set ; ::_thesis: 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 ) ) let x be Element of X; ::_thesis: ( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds (UnitBag x) . y = 0 ) ) A1: dom (X --> 0) = X by FUNCOP_1:13; thus (UnitBag x) . x = ((X --> 0) +* (x,1)) . x by PRE_POLY:def_13 .= 1 by A1, FUNCT_7:31 ; ::_thesis: for y being Element of X st x <> y holds (UnitBag x) . y = 0 let y be Element of X; ::_thesis: ( x <> y implies (UnitBag x) . y = 0 ) assume x <> y ; ::_thesis: (UnitBag x) . y = 0 hence (UnitBag x) . y = (EmptyBag X) . y by FUNCT_7:32 .= 0 by PRE_POLY:52 ; ::_thesis: verum end; 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 proof let X be non empty set ; ::_thesis: for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds x1 = x2 let x1, x2 be Element of X; ::_thesis: ( UnitBag x1 = UnitBag x2 implies x1 = x2 ) assume that A1: UnitBag x1 = UnitBag x2 and A2: x1 <> x2 ; ::_thesis: contradiction 1 = (UnitBag x2) . x1 by A1, Th9 .= 0 by A2, Th9 ; hence contradiction ; ::_thesis: verum 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 proof let X be non empty Ordinal; ::_thesis: 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 let x be Element of X; ::_thesis: for L being non trivial well-unital doubleLoopStr for e being Function of X,L holds eval ((UnitBag x),e) = e . x let L be non trivial well-unital doubleLoopStr ; ::_thesis: for e being Function of X,L holds eval ((UnitBag x),e) = e . x let e be Function of X,L; ::_thesis: eval ((UnitBag x),e) = e . x reconsider edx = e . x as Element of L ; support (UnitBag x) = {x} by Th8; hence eval ((UnitBag x),e) = (power L) . ((e . x),((UnitBag x) . x)) by POLYNOM2:15 .= (power L) . ((e . x),(0 + 1)) by Th9 .= ((power L) . (edx,0)) * edx by GROUP_1:def_7 .= (1_ L) * edx by GROUP_1:def_7 .= e . x by GROUP_1:def_4 ; ::_thesis: verum end; 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 & ( for b being bag of X st b <> UnitBag x holds (1_1 (x,L)) . b = 0. L ) ) proof let X be set ; ::_thesis: 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 ) ) let L be non trivial unital doubleLoopStr ; ::_thesis: 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 ) ) let x be Element of X; ::_thesis: ( (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 ) ) dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7 .= Bags X by FUNCOP_1:13 ; hence (1_1 (x,L)) . (UnitBag x) = 1_ L by FUNCT_7:31; ::_thesis: for b being bag of X st b <> UnitBag x holds (1_1 (x,L)) . b = 0. L let b be bag of X; ::_thesis: ( b <> UnitBag x implies (1_1 (x,L)) . b = 0. L ) assume b <> UnitBag x ; ::_thesis: (1_1 (x,L)) . b = 0. L hence (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32 .= 0. L by POLYNOM1:22 ; ::_thesis: verum 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)} proof let X be set ; ::_thesis: 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)} let x be Element of X; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)} let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; ::_thesis: Support (1_1 (x,L)) = {(UnitBag x)} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Support_(1_1_(x,L))_implies_a_in_{(UnitBag_x)}_)_&_(_a_in_{(UnitBag_x)}_implies_a_in_Support_(1_1_(x,L))_)_) let a be set ; ::_thesis: ( ( a in Support (1_1 (x,L)) implies a in {(UnitBag x)} ) & ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) ) ) hereby ::_thesis: ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) ) assume A1: a in Support (1_1 (x,L)) ; ::_thesis: a in {(UnitBag x)} then reconsider b = a as Element of Bags X ; now__::_thesis:_not_a_<>_UnitBag_x assume a <> UnitBag x ; ::_thesis: contradiction then (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32 .= 0. L by POLYNOM1:22 ; hence contradiction by A1, POLYNOM1:def_3; ::_thesis: verum end; hence a in {(UnitBag x)} by TARSKI:def_1; ::_thesis: verum end; assume A2: a in {(UnitBag x)} ; ::_thesis: a in Support (1_1 (x,L)) then a = UnitBag x by TARSKI:def_1; then (1_1 (x,L)) . a <> 0. L by Th12; hence a in Support (1_1 (x,L)) by A2, POLYNOM1:def_3; ::_thesis: verum end; hence Support (1_1 (x,L)) = {(UnitBag x)} by TARSKI:1; ::_thesis: verum 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 ; cluster 1_1 (x,L) -> finite-Support ; coherence 1_1 (x,L) is finite-Support proof Support (1_1 (x,L)) = {(UnitBag x)} by Th13; hence 1_1 (x,L) is finite-Support by POLYNOM1:def_4; ::_thesis: verum end; 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 proof let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; ::_thesis: 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 let X be non empty set ; ::_thesis: for x1, x2 being Element of X st 1_1 (x1,L) = 1_1 (x2,L) holds x1 = x2 let x1, x2 be Element of X; ::_thesis: ( 1_1 (x1,L) = 1_1 (x2,L) implies x1 = x2 ) assume that A1: 1_1 (x1,L) = 1_1 (x2,L) and A2: x1 <> x2 ; ::_thesis: contradiction 1_ L = (1_1 (x2,L)) . (UnitBag x1) by A1, Th12 .= 0. L by A2, Th10, Th12 ; hence contradiction ; ::_thesis: verum 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 proof let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for x being Element of (Polynom-Ring L) for p being sequence of L st x = p holds - x = - p let x be Element of (Polynom-Ring L); ::_thesis: for p being sequence of L st x = p holds - x = - p let p be sequence of L; ::_thesis: ( x = p implies - x = - p ) assume A1: x = p ; ::_thesis: - x = - p reconsider x9 = x as Polynomial of L by POLYNOM3:def_10; A2: now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_ (p_-_p)_._i_=_(0_._L)_._i let i be set ; ::_thesis: ( i in NAT implies (p - p) . i = (0_. L) . i ) assume A3: i in NAT ; ::_thesis: (p - p) . i = (0_. L) . i then reconsider i9 = i as Element of NAT ; thus (p - p) . i = (p . i9) - (p . i9) by POLYNOM3:27 .= 0. L by RLVECT_1:15 .= (0_. L) . i by A3, FUNCOP_1:7 ; ::_thesis: verum end; reconsider mx = - x9 as Element of (Polynom-Ring L) by POLYNOM3:def_10; ( dom (0_. L) = NAT & dom (p - p) = NAT ) by FUNCT_2:def_1; then A4: p - p = 0_. L by A2, FUNCT_1:2; x + mx = x9 + (- x9) by POLYNOM3:def_10 .= 0. (Polynom-Ring L) by A1, A4, POLYNOM3:def_10 ; then x = - mx by RLVECT_1:6; hence - x = - p by A1, RLVECT_1:17; ::_thesis: verum 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 proof let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: 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 let x, y be Element of (Polynom-Ring L); ::_thesis: for p, q being sequence of L st x = p & y = q holds x - y = p - q let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x - y = p - q ) assume that A1: x = p and A2: y = q ; ::_thesis: x - y = p - q A3: - y = - q by A2, Th15; thus x - y = x + (- y) by RLVECT_1:def_11 .= p - q by A1, A3, POLYNOM3:def_10 ; ::_thesis: verum 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); 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 } is non empty Subset of I proof I c= I ; then reconsider I9 = I as non empty Subset of I ; defpred S1[ Element of I, Element of NAT ] means for p being Polynomial of L st $1 = p holds $2 = len p; set u = { 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 } ; A1: now__::_thesis:_for_x_being_Element_of_I_ex_y_being_Element_of_NAT_st_S1[x,y] let x be Element of I; ::_thesis: ex y being Element of NAT st S1[x,y] reconsider x9 = x as Polynomial of L by POLYNOM3:def_10; for p being Polynomial of L st x = p holds len x9 = len p ; hence ex y being Element of NAT st S1[x,y] ; ::_thesis: verum end; consider f being Function of I,NAT such that A2: for x being Element of I holds S1[x,f . x] from FUNCT_2:sch_3(A1); min (f .: I9) in f .: I by XXREAL_2:def_7; then consider x being set such that A3: x in dom f and x in I and A4: min (f .: I9) = f . x by FUNCT_1:def_6; reconsider x = x as Element of I by A3; now__::_thesis:_for_x9,_y9_being_Polynomial_of_L_st_x9_=_x_&_y9_in_I_holds_ len_x9_<=_len_y9 let x9, y9 be Polynomial of L; ::_thesis: ( x9 = x & y9 in I implies len x9 <= len y9 ) assume that A5: x9 = x and A6: y9 in I ; ::_thesis: len x9 <= len y9 dom f = I by FUNCT_2:def_1; then f . y9 in f .: I by A6, FUNCT_1:def_6; then f . x <= f . y9 by A4, XXREAL_2:def_7; then len x9 <= f . y9 by A2, A5; hence len x9 <= len y9 by A2, A6; ::_thesis: verum end; then A7: x in { 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 } c= I proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { 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 } or x in I ) assume x in { 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 } ; ::_thesis: x in I then ex x99 being Element of I st ( x99 = x & ( for x9, y9 being Polynomial of L st x9 = x99 & y9 in I holds len x9 <= len y9 ) ) ; hence x in I ; ::_thesis: verum end; hence { 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 by A7; ::_thesis: verum end; 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 } ; 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 ) proof let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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 ) let I be non empty Subset of (Polynom-Ring L); ::_thesis: for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds ( i1 in I & len i1 <= len i2 ) let i1, i2 be Polynomial of L; ::_thesis: ( i1 in minlen I & i2 in I implies ( i1 in I & len i1 <= len i2 ) ) assume that A1: i1 in minlen I and A2: i2 in I ; ::_thesis: ( i1 in I & len i1 <= len i2 ) ex i19 being Element of I st ( i19 = i1 & ( for x9, y9 being Polynomial of L st x9 = i19 & y9 in I holds len x9 <= len y9 ) ) by A1; hence ( i1 in I & len i1 <= len i2 ) by A2; ::_thesis: verum 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; 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 ex b1 being Polynomial of L st for x being Nat holds ( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) ) proof reconsider x = (0_. L) +* (n,a) as sequence of L ; now__::_thesis:_for_i_being_Nat_st_i_>=_n_+_1_holds_ x_._i_=_0._L let i be Nat; ::_thesis: ( i >= n + 1 implies x . i = 0. L ) A1: i in NAT by ORDINAL1:def_12; assume i >= n + 1 ; ::_thesis: x . i = 0. L then i > n by NAT_1:13; hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32 .= 0. L by A1, FUNCOP_1:7 ; ::_thesis: verum end; then reconsider x = x as Polynomial of L by ALGSEQ_1:def_1; now__::_thesis:_for_i_being_Nat_holds_ (_(_i_=_n_implies_x_._i_=_a_)_&_(_i_<>_n_implies_x_._i_=_0._L_)_) let i be Nat; ::_thesis: ( ( i = n implies x . i = a ) & ( i <> n implies x . i = 0. L ) ) A2: i in NAT by ORDINAL1:def_12; thus ( i = n implies x . i = a ) ::_thesis: ( i <> n implies x . i = 0. L ) proof A3: dom (0_. L) = NAT by FUNCT_2:def_1; assume i = n ; ::_thesis: x . i = a hence x . i = a by A2, A3, FUNCT_7:31; ::_thesis: verum end; thus ( i <> n implies x . i = 0. L ) ::_thesis: verum proof assume i <> n ; ::_thesis: x . i = 0. L hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32 .= 0. L by A2, FUNCOP_1:7 ; ::_thesis: verum end; end; hence ex b1 being Polynomial of L st for x being Nat holds ( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Polynomial of L st ( for x being Nat holds ( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) ) ) & ( for x being Nat holds ( ( x = n implies b2 . x = a ) & ( x <> n implies b2 . x = 0. L ) ) ) holds b1 = b2 proof let u, v be Polynomial of L; ::_thesis: ( ( for x being Nat holds ( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) ) & ( for x being Nat holds ( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ) implies u = v ) assume that A4: for x being Nat holds ( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) and A5: for x being Nat holds ( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ; ::_thesis: u = v A6: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ u_._x_=_v_._x let x be set ; ::_thesis: ( x in NAT implies u . b1 = v . b1 ) assume A7: x in NAT ; ::_thesis: u . b1 = v . b1 percases ( x = n or x <> n ) ; supposeA8: x = n ; ::_thesis: u . b1 = v . b1 hence u . x = a by A4 .= v . x by A5, A8 ; ::_thesis: verum end; supposeA9: x <> n ; ::_thesis: u . b1 = v . b1 hence u . x = 0. L by A4, A7 .= v . x by A5, A7, A9 ; ::_thesis: verum end; end; end; ( dom u = NAT & dom v = NAT ) by FUNCT_2:def_1; hence u = v by A6, FUNCT_1:2; ::_thesis: verum end; 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 ) & ( 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 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 ) proof let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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 ) let n be Element of NAT ; ::_thesis: 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 ) let a be Element of L; ::_thesis: ( ( 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 ) A1: now__::_thesis:_(_a_=_0._L_implies_len_(monomial_(a,n))_=_0_) assume A2: a = 0. L ; ::_thesis: len (monomial (a,n)) = 0 now__::_thesis:_for_i_being_Nat_st_i_>=_0_holds_ (monomial_(a,n))_._i_=_0._L let i be Nat; ::_thesis: ( i >= 0 implies (monomial (a,n)) . b1 = 0. L ) assume i >= 0 ; ::_thesis: (monomial (a,n)) . b1 = 0. L percases ( i = n or i <> n ) ; suppose i = n ; ::_thesis: (monomial (a,n)) . b1 = 0. L thus (monomial (a,n)) . i = 0. L by A2, Def5; ::_thesis: verum end; suppose i <> n ; ::_thesis: (monomial (a,n)) . b1 = 0. L hence (monomial (a,n)) . i = 0. L by Def5; ::_thesis: verum end; end; end; then 0 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def_2; hence len (monomial (a,n)) = 0 by ALGSEQ_1:def_3; ::_thesis: verum end; now__::_thesis:_(_a_<>_0._L_implies_len_(monomial_(a,n))_=_n_+_1_) now__::_thesis:_for_i_being_Nat_st_i_>=_n_+_1_holds_ (monomial_(a,n))_._i_=_0._L let i be Nat; ::_thesis: ( i >= n + 1 implies (monomial (a,n)) . i = 0. L ) assume i >= n + 1 ; ::_thesis: (monomial (a,n)) . i = 0. L then i > n by NAT_1:13; hence (monomial (a,n)) . i = 0. L by Def5; ::_thesis: verum end; then n + 1 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def_2; then A3: len (monomial (a,n)) <= n + 1 by ALGSEQ_1:def_3; assume a <> 0. L ; ::_thesis: len (monomial (a,n)) = n + 1 then (monomial (a,n)) . n <> 0. L by Def5; then len (monomial (a,n)) > n by ALGSEQ_1:8; then len (monomial (a,n)) >= n + 1 by NAT_1:13; hence len (monomial (a,n)) = n + 1 by A3, XXREAL_0:1; ::_thesis: verum end; hence ( ( 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 ) by A1; ::_thesis: verum 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) proof let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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) let n, x be Element of NAT ; ::_thesis: for a being Element of L for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x) let a be Element of L; ::_thesis: for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x) let p be Polynomial of L; ::_thesis: ((monomial (a,n)) *' p) . (x + n) = a * (p . x) consider r being FinSequence of the carrier of L such that A1: len r = (x + n) + 1 and A2: ((monomial (a,n)) *' p) . (x + n) = Sum r and A3: for k being Element of NAT st k in dom r holds r . k = ((monomial (a,n)) . (k -' 1)) * (p . (((x + n) + 1) -' k)) by POLYNOM3:def_9; len r = n + (1 + x) by A1; then consider b, c being FinSequence of the carrier of L such that A4: len b = n and A5: len c = 1 + x and A6: r = b ^ c by FINSEQ_2:23; consider d, e being FinSequence of the carrier of L such that A7: len d = 1 and len e = x and A8: c = d ^ e by A5, FINSEQ_2:23; A9: dom d c= dom c by A8, FINSEQ_1:26; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_b_holds_ b_._i_=_0._L A10: dom b c= dom r by A6, FINSEQ_1:26; let i be Element of NAT ; ::_thesis: ( i in dom b implies b . i = 0. L ) A11: i - 1 < i by XREAL_1:146; assume A12: i in dom b ; ::_thesis: b . i = 0. L then A13: i <= n by A4, FINSEQ_3:25; 1 <= i by A12, FINSEQ_3:25; then A14: i -' 1 = i - 1 by XREAL_1:233; thus b . i = r . i by A6, A12, FINSEQ_1:def_7 .= ((monomial (a,n)) . (i -' 1)) * (p . (((x + n) + 1) -' i)) by A3, A12, A10 .= (0. L) * (p . (((x + n) + 1) -' i)) by A13, A14, A11, Def5 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then A15: Sum b = 0. L by POLYNOM3:1; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_e_holds_ e_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom e implies e . i = 0. L ) A16: (n + (1 + i)) -' 1 = ((n + i) + 1) -' 1 .= n + i by NAT_D:34 ; assume A17: i in dom e ; ::_thesis: e . i = 0. L then A18: 1 + i in dom c by A7, A8, FINSEQ_1:28; i >= 1 by A17, FINSEQ_3:25; then n + i >= n + 1 by XREAL_1:6; then A19: n + i > n by NAT_1:13; thus e . i = c . (1 + i) by A7, A8, A17, FINSEQ_1:def_7 .= r . (n + (1 + i)) by A4, A6, A18, FINSEQ_1:def_7 .= ((monomial (a,n)) . ((n + (1 + i)) -' 1)) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A3, A4, A6, A18, FINSEQ_1:28 .= (0. L) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A19, A16, Def5 .= 0. L by VECTSP_1:7 ; ::_thesis: verum end; then A20: Sum e = 0. L by POLYNOM3:1; A21: 1 in dom d by A7, FINSEQ_3:25; then d . 1 = c . 1 by A8, FINSEQ_1:def_7 .= r . (n + 1) by A4, A6, A21, A9, FINSEQ_1:def_7 .= ((monomial (a,n)) . ((n + 1) -' 1)) * (p . (((x + n) + 1) -' (n + 1))) by A3, A4, A6, A21, A9, FINSEQ_1:28 .= ((monomial (a,n)) . n) * (p . ((x + (n + 1)) -' (n + 1))) by NAT_D:34 .= ((monomial (a,n)) . n) * (p . x) by NAT_D:34 .= a * (p . x) by Def5 ; then d = <*(a * (p . x))*> by A7, FINSEQ_1:40; then Sum d = a * (p . x) by RLVECT_1:44; then Sum c = (a * (p . x)) + (0. L) by A8, A20, RLVECT_1:41 .= a * (p . x) by RLVECT_1:4 ; hence ((monomial (a,n)) *' p) . (x + n) = (0. L) + (a * (p . x)) by A2, A6, A15, RLVECT_1:41 .= a * (p . x) by RLVECT_1:4 ; ::_thesis: verum 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 proof let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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 let n, x be Element of NAT ; ::_thesis: for a being Element of L for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a let a be Element of L; ::_thesis: for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a let p be Polynomial of L; ::_thesis: (p *' (monomial (a,n))) . (x + n) = (p . x) * a consider r being FinSequence of the carrier of L such that A1: len r = (x + n) + 1 and A2: (p *' (monomial (a,n))) . (x + n) = Sum r and A3: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' k)) by POLYNOM3:def_9; len r = x + (n + 1) by A1; then consider b, c being FinSequence of the carrier of L such that A4: len b = x and A5: len c = n + 1 and A6: r = b ^ c by FINSEQ_2:23; consider d, e being FinSequence of the carrier of L such that A7: len d = 1 and A8: len e = n and A9: c = d ^ e by A5, FINSEQ_2:23; A10: dom d c= dom c by A9, FINSEQ_1:26; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_e_holds_ e_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom e implies e . i = 0. L ) A11: n > n - 1 by XREAL_1:146; assume A12: i in dom e ; ::_thesis: e . i = 0. L then A13: 1 + i in dom c by A7, A9, FINSEQ_1:28; i <= n by A8, A12, FINSEQ_3:25; then x + i <= x + n by XREAL_1:6; then (x + i) + 1 <= (x + n) + 1 by XREAL_1:6; then A14: ((x + n) + 1) -' (x + (1 + i)) = ((x + n) + 1) - (x + (1 + i)) by XREAL_1:233; 1 <= i by A12, FINSEQ_3:25; then A15: n - i <= n - 1 by XREAL_1:13; thus e . i = c . (1 + i) by A7, A9, A12, FINSEQ_1:def_7 .= r . (x + (1 + i)) by A4, A6, A13, FINSEQ_1:def_7 .= (p . ((x + (1 + i)) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + (1 + i)))) by A3, A4, A6, A13, FINSEQ_1:28 .= (p . ((x + (1 + i)) -' 1)) * (0. L) by A14, A15, A11, Def5 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; then A16: Sum e = 0. L by POLYNOM3:1; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_b_holds_ b_._i_=_0._L let i be Element of NAT ; ::_thesis: ( i in dom b implies b . i = 0. L ) A17: dom b c= dom r by A6, FINSEQ_1:26; assume A18: i in dom b ; ::_thesis: b . i = 0. L then i <= x by A4, FINSEQ_3:25; then i + n <= x + n by XREAL_1:6; then i + n < (x + n) + 1 by NAT_1:13; then A19: n < ((x + n) + 1) - i by XREAL_1:20; then A20: ((x + n) + 1) - i = ((x + n) + 1) -' i by XREAL_0:def_2; thus b . i = r . i by A6, A18, FINSEQ_1:def_7 .= (p . (i -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' i)) by A3, A18, A17 .= (p . (i -' 1)) * (0. L) by A19, A20, Def5 .= 0. L by VECTSP_1:6 ; ::_thesis: verum end; then A21: Sum b = 0. L by POLYNOM3:1; A22: 1 in dom d by A7, FINSEQ_3:25; then d . 1 = c . 1 by A9, FINSEQ_1:def_7 .= r . (x + 1) by A4, A6, A22, A10, FINSEQ_1:def_7 .= (p . ((x + 1) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + 1))) by A3, A4, A6, A22, A10, FINSEQ_1:28 .= (p . x) * ((monomial (a,n)) . ((n + (x + 1)) -' (x + 1))) by NAT_D:34 .= (p . x) * ((monomial (a,n)) . n) by NAT_D:34 .= (p . x) * a by Def5 ; then d = <*((p . x) * a)*> by A7, FINSEQ_1:40; then Sum d = (p . x) * a by RLVECT_1:44; then Sum c = ((p . x) * a) + (0. L) by A9, A16, RLVECT_1:41 .= (p . x) * a by RLVECT_1:4 ; hence (p *' (monomial (a,n))) . (x + n) = (0. L) + ((p . x) * a) by A2, A6, A21, RLVECT_1:41 .= (p . x) * a by RLVECT_1:4 ; ::_thesis: verum 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 proof let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1 let p, q be Polynomial of L; ::_thesis: len (p *' q) <= ((len p) + (len q)) -' 1 now__::_thesis:_for_i_being_Nat_st_i_>=_((len_p)_+_(len_q))_-'_1_holds_ (p_*'_q)_._i_=_0._L let i be Nat; ::_thesis: ( i >= ((len p) + (len q)) -' 1 implies (p *' q) . i = 0. L ) A1: ((len p) + (len q)) -' 1 >= ((len p) + (len q)) - 1 by XREAL_0:def_2; i in NAT by ORDINAL1:def_12; then consider r being FinSequence of the carrier of L such that A2: len r = i + 1 and A3: (p *' q) . i = Sum r and A4: for k being Element of NAT st k in dom r holds r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def_9; assume i >= ((len p) + (len q)) -' 1 ; ::_thesis: (p *' q) . i = 0. L then i >= (len p) + ((len q) - 1) by A1, XXREAL_0:2; then len p <= i - ((len q) - 1) by XREAL_1:19; then A5: - (len p) >= - ((i - (len q)) + 1) by XREAL_1:24; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ r_._k_=_0._L let k be Element of NAT ; ::_thesis: ( k in dom r implies r . b1 = 0. L ) assume A6: k in dom r ; ::_thesis: r . b1 = 0. L then A7: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A4; k in Seg (len r) by A6, FINSEQ_1:def_3; then k <= i + 1 by A2, FINSEQ_1:1; then A8: (i + 1) - k >= 0 by XREAL_1:48; percases ( k -' 1 < len p or k -' 1 >= len p ) ; suppose k -' 1 < len p ; ::_thesis: r . b1 = 0. L then k - 1 < len p by XREAL_0:def_2; then - (k - 1) > - (len p) by XREAL_1:24; then 1 - k > ((len q) - 1) - i by A5, XXREAL_0:2; then i + (1 - k) > (len q) - 1 by XREAL_1:19; then (i + 1) -' k > (len q) - 1 by A8, XREAL_0:def_2; then (i + 1) -' k >= ((len q) - 1) + 1 by INT_1:7; then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A7, VECTSP_1:6; ::_thesis: verum end; suppose k -' 1 >= len p ; ::_thesis: r . b1 = 0. L then p . (k -' 1) = 0. L by ALGSEQ_1:8; hence r . k = 0. L by A7, VECTSP_1:7; ::_thesis: verum end; end; end; hence (p *' q) . i = 0. L by A3, POLYNOM3:1; ::_thesis: verum end; then ((len p) + (len q)) -' 1 is_at_least_length_of p *' q by ALGSEQ_1:def_2; hence len (p *' q) <= ((len p) + (len q)) -' 1 by ALGSEQ_1:def_3; ::_thesis: verum end; 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 proof let R, S be non empty doubleLoopStr ; ::_thesis: for I being Ideal of R for P being Function of R,S st P is RingIsomorphism holds P .: I is Ideal of S let I be Ideal of R; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds P .: I is Ideal of S let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P .: I is Ideal of S ) set Q = P .: I; assume A1: P is RingIsomorphism ; ::_thesis: P .: I is Ideal of S A2: now__::_thesis:_for_p,_x_being_Element_of_S_st_x_in_P_.:_I_holds_ p_*_x_in_P_.:_I let p, x be Element of S; ::_thesis: ( x in P .: I implies p * x in P .: I ) assume x in P .: I ; ::_thesis: p * x in P .: I then consider x9 being set such that A3: x9 in the carrier of R and A4: x9 in I and A5: x = P . x9 by FUNCT_2:64; reconsider x9 = x9 as Element of R by A3; A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21; then rng P = the carrier of S by QUOFIELD:def_19; then consider p9 being set such that A7: p9 in dom P and A8: p = P . p9 by FUNCT_1:def_3; reconsider p9 = p9 as Element of R by A7; A9: p9 * x9 in I by A4, IDEAL_1:def_2; P is RingHomomorphism by A6, QUOFIELD:def_19; then P is multiplicative by QUOFIELD:def_18; then p * x = P . (p9 * x9) by A5, A8, GROUP_6:def_6; hence p * x in P .: I by A9, FUNCT_2:35; ::_thesis: verum end; A10: now__::_thesis:_for_p,_x_being_Element_of_S_st_x_in_P_.:_I_holds_ x_*_p_in_P_.:_I let p, x be Element of S; ::_thesis: ( x in P .: I implies x * p in P .: I ) assume x in P .: I ; ::_thesis: x * p in P .: I then consider x9 being set such that A11: x9 in the carrier of R and A12: x9 in I and A13: x = P . x9 by FUNCT_2:64; reconsider x9 = x9 as Element of R by A11; A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21; then rng P = the carrier of S by QUOFIELD:def_19; then consider p9 being set such that A15: p9 in dom P and A16: p = P . p9 by FUNCT_1:def_3; reconsider p9 = p9 as Element of R by A15; A17: x9 * p9 in I by A12, IDEAL_1:def_3; P is RingHomomorphism by A14, QUOFIELD:def_19; then P is multiplicative by QUOFIELD:def_18; then x * p = P . (x9 * p9) by A13, A16, GROUP_6:def_6; hence x * p in P .: I by A17, FUNCT_2:35; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_S_st_x_in_P_.:_I_&_y_in_P_.:_I_holds_ x_+_y_in_P_.:_I let x, y be Element of S; ::_thesis: ( x in P .: I & y in P .: I implies x + y in P .: I ) assume that A18: x in P .: I and A19: y in P .: I ; ::_thesis: x + y in P .: I consider x9 being set such that A20: x9 in the carrier of R and A21: x9 in I and A22: x = P . x9 by A18, FUNCT_2:64; consider y9 being set such that A23: y9 in the carrier of R and A24: y9 in I and A25: y = P . y9 by A19, FUNCT_2:64; reconsider x9 = x9, y9 = y9 as Element of R by A20, A23; A26: x9 + y9 in I by A21, A24, IDEAL_1:def_1; ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21; then P is RingHomomorphism by QUOFIELD:def_19; then P is additive by QUOFIELD:def_18; then x + y = P . (x9 + y9) by A22, A25, VECTSP_1:def_20; hence x + y in P .: I by A26, FUNCT_2:35; ::_thesis: verum end; hence P .: I is Ideal of S by A2, A10, IDEAL_1:def_1, IDEAL_1:def_2, IDEAL_1:def_3; ::_thesis: verum 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 proof let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds f . (0. R) = 0. S let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies f . (0. R) = 0. S ) assume f is RingHomomorphism ; ::_thesis: f . (0. R) = 0. S then A1: f is additive by QUOFIELD:def_18; f . (0. R) = f . ((0. R) + (0. R)) by RLVECT_1:4 .= (f . (0. R)) + (f . (0. R)) by A1, VECTSP_1:def_20 ; then 0. S = ((f . (0. R)) + (f . (0. R))) + (- (f . (0. R))) by RLVECT_1:def_10 .= (f . (0. R)) + ((f . (0. R)) + (- (f . (0. R)))) by RLVECT_1:def_3 .= (f . (0. R)) + (0. S) by RLVECT_1:def_10 .= f . (0. R) by RLVECT_1:4 ; hence f . (0. R) = 0. S ; ::_thesis: verum 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 proof let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 let F be non empty Subset of R; ::_thesis: 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 let G be non empty Subset of S; ::_thesis: 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 let P be Function of R,S; ::_thesis: 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 let lc be LinearCombination of F; ::_thesis: 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 let LC be LinearCombination of G; ::_thesis: 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 let E be FinSequence of [: the carrier of R, the carrier of R, the carrier of R:]; ::_thesis: ( 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)) ) implies P . (Sum lc) = Sum LC ) assume that A1: P is RingHomomorphism and A2: len lc = len LC and A3: E represents lc and A4: 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)) ; ::_thesis: P . (Sum lc) = Sum LC defpred S1[ Element of NAT ] means for lc9 being LinearCombination of F for LC9 being LinearCombination of G st lc9 = lc | (Seg $1) & LC9 = LC | (Seg $1) holds P . (Sum lc9) = Sum LC9; A5: ( P is additive & P is multiplicative ) by A1, QUOFIELD:def_18; A6: dom lc = dom LC by A2, FINSEQ_3:29; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let lc9 be LinearCombination of F; ::_thesis: for LC9 being LinearCombination of G st lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) holds P . (Sum lc9) = Sum LC9 let LC9 be LinearCombination of G; ::_thesis: ( lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) implies P . (Sum lc9) = Sum LC9 ) assume that A9: lc9 = lc | (Seg (k + 1)) and A10: LC9 = LC | (Seg (k + 1)) ; ::_thesis: P . (Sum lc9) = Sum LC9 percases ( len lc < k + 1 or len lc >= k + 1 ) ; supposeA11: len lc < k + 1 ; ::_thesis: P . (Sum lc9) = Sum LC9 then A12: len lc <= k by NAT_1:13; A13: lc9 = lc by A9, A11, FINSEQ_3:49 .= lc | (Seg k) by A12, FINSEQ_3:49 ; LC9 = LC by A2, A10, A11, FINSEQ_3:49 .= LC | (Seg k) by A2, A12, FINSEQ_3:49 ; hence P . (Sum lc9) = Sum LC9 by A8, A13; ::_thesis: verum end; supposeA14: len lc >= k + 1 ; ::_thesis: P . (Sum lc9) = Sum LC9 set i = k + 1; reconsider LCk = LC | (Seg k) as LinearCombination of G by IDEAL_1:41; reconsider lck = lc | (Seg k) as LinearCombination of F by IDEAL_1:41; 1 <= k + 1 by NAT_1:11; then A15: k + 1 in dom lc by A14, FINSEQ_3:25; then A16: lc . (k + 1) = lc /. (k + 1) by PARTFUN1:def_6; A17: LC . (k + 1) = LC /. (k + 1) by A6, A15, PARTFUN1:def_6; lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*> by A15, FINSEQ_5:10; hence P . (Sum lc9) = P . ((Sum lck) + (lc /. (k + 1))) by A9, A16, FVSUM_1:71 .= (P . (Sum lck)) + (P . (lc /. (k + 1))) by A5, VECTSP_1:def_20 .= (Sum LCk) + (P . (lc /. (k + 1))) by A8 .= (Sum LCk) + (P . ((((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3)) * ((E /. (k + 1)) `3_3))) by A3, A15, A16, IDEAL_1:def_11 .= (Sum LCk) + ((P . (((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5, GROUP_6:def_6 .= (Sum LCk) + (((P . ((E /. (k + 1)) `1_3)) * (P . ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5, GROUP_6:def_6 .= (Sum LCk) + (LC /. (k + 1)) by A4, A6, A15, A17 .= Sum (LCk ^ <*(LC /. (k + 1))*>) by FVSUM_1:71 .= Sum LC9 by A6, A10, A15, A17, FINSEQ_5:10 ; ::_thesis: verum end; end; end; end; A18: ( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) ) by FINSEQ_3:49; A19: S1[ 0 ] proof let lc9 be LinearCombination of F; ::_thesis: for LC9 being LinearCombination of G st lc9 = lc | (Seg 0) & LC9 = LC | (Seg 0) holds P . (Sum lc9) = Sum LC9 let LC9 be LinearCombination of G; ::_thesis: ( lc9 = lc | (Seg 0) & LC9 = LC | (Seg 0) implies P . (Sum lc9) = Sum LC9 ) assume that A20: lc9 = lc | (Seg 0) and A21: LC9 = LC | (Seg 0) ; ::_thesis: P . (Sum lc9) = Sum LC9 thus P . (Sum lc9) = P . (Sum (<*> the carrier of R)) by A20 .= P . (0. R) by RLVECT_1:43 .= 0. S by A1, Th23 .= Sum (<*> the carrier of S) by RLVECT_1:43 .= Sum LC9 by A21 ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A7); hence P . (Sum lc) = Sum LC by A2, A18; ::_thesis: verum 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 proof let R, S be non empty doubleLoopStr ; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds P " is RingIsomorphism let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P " is RingIsomorphism ) assume A1: P is RingIsomorphism ; ::_thesis: P " is RingIsomorphism then A2: P is RingEpimorphism by QUOFIELD:def_21; then A3: rng P = the carrier of S by QUOFIELD:def_19; P is RingMonomorphism by A1, QUOFIELD:def_21; then A4: P is one-to-one by QUOFIELD:def_20; P is RingHomomorphism by A2, QUOFIELD:def_19; then A5: ( P is additive & P is multiplicative & P is unity-preserving ) by QUOFIELD:def_18; for x, y being Element of S holds ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) proof A6: P is onto by A3, FUNCT_2:def_3; A7: (P ") . (1_ S) = (P ") . (P . (1_ R)) by A5, GROUP_1:def_13 .= (P ") . (P . (1_ R)) by A4, A6, TOPS_2:def_4 .= 1_ R by A4, FUNCT_2:26 ; let x, y be Element of S; ::_thesis: ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) consider x9 being set such that A8: x9 in the carrier of R and A9: P . x9 = x by A3, FUNCT_2:11; reconsider x9 = x9 as Element of R by A8; A10: x9 = (P ") . (P . x9) by A4, FUNCT_2:26 .= (P ") . x by A4, A9, A6, TOPS_2:def_4 ; consider y9 being set such that A11: y9 in the carrier of R and A12: P . y9 = y by A3, FUNCT_2:11; reconsider y9 = y9 as Element of R by A11; A13: y9 = (P ") . (P . y9) by A4, FUNCT_2:26 .= (P ") . y by A6, A4, A12, TOPS_2:def_4 ; A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12, GROUP_6:def_6 .= (P ") . (P . (x9 * y9)) by A4, A6, TOPS_2:def_4 .= ((P ") . x) * ((P ") . y) by A4, A10, A13, FUNCT_2:26 ; (P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12, VECTSP_1:def_20 .= (P ") . (P . (x9 + y9)) by A4, A6, TOPS_2:def_4 .= ((P ") . x) + ((P ") . y) by A4, A10, A13, FUNCT_2:26 ; hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by A14, A7; ::_thesis: verum end; then ( P " is additive & P " is multiplicative & P " is unity-preserving ) by VECTSP_1:def_20, GROUP_1:def_13, GROUP_6:def_6; then A15: P " is RingHomomorphism by QUOFIELD:def_18; A16: rng P = [#] S by A2, QUOFIELD:def_19; then rng (P ") = [#] R by A4, TOPS_2:49 .= the carrier of R ; then A17: P " is RingEpimorphism by A15, QUOFIELD:def_19; P " is one-to-one by A4, A16, TOPS_2:50; then P " is RingMonomorphism by A15, QUOFIELD:def_20; hence P " is RingIsomorphism by A17, QUOFIELD:def_21; ::_thesis: verum end; 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 proof let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: 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 let F be non empty Subset of R; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds P .: (F -Ideal) = (P .: F) -Ideal let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P .: (F -Ideal) = (P .: F) -Ideal ) assume A1: P is RingIsomorphism ; ::_thesis: P .: (F -Ideal) = (P .: F) -Ideal now__::_thesis:_for_x_being_set_st_x_in_(P_.:_F)_-Ideal_holds_ x_in_P_.:_(F_-Ideal) let x be set ; ::_thesis: ( x in (P .: F) -Ideal implies x in P .: (F -Ideal) ) A2: dom P = the carrier of R by FUNCT_2:def_1; assume A3: x in (P .: F) -Ideal ; ::_thesis: x in P .: (F -Ideal) then consider lc being LinearCombination of P .: F such that A4: x = Sum lc by IDEAL_1:60; consider E being FinSequence of [: the carrier of S, the carrier of S, the carrier of S:] such that A5: E represents lc by IDEAL_1:35; P is RingMonomorphism by A1, QUOFIELD:def_21; then A6: P is one-to-one by QUOFIELD:def_20; P is RingEpimorphism by A1, QUOFIELD:def_21; then A7: rng P = the carrier of S by QUOFIELD:def_19; then P is onto by FUNCT_2:def_3; then A8: P " = P " by A6, TOPS_2:def_4; (P ") .: (P .: F) = P " (P .: F) by A6, FUNCT_1:85; then consider lc9 being LinearCombination of F such that A9: ( len lc = len lc9 & ( for i being set st i in dom lc9 holds lc9 . i = (((P ") . ((E /. i) `1_3)) * ((P ") . ((E /. i) `2_3))) * ((P ") . ((E /. i) `3_3)) ) ) by A6, A8, A5, FUNCT_1:82, IDEAL_1:36; P " is RingIsomorphism by A1, Th25; then P " is RingMonomorphism by QUOFIELD:def_21; then P " is RingHomomorphism by QUOFIELD:def_20; then (P ") . x = Sum lc9 by A4, A5, A9, Th24; then (P ") . x in F -Ideal by IDEAL_1:60; then P . ((P ") . x) in P .: (F -Ideal) by A2, FUNCT_1:def_6; hence x in P .: (F -Ideal) by A3, A6, A7, A8, FUNCT_1:35; ::_thesis: verum end; then A10: (P .: F) -Ideal c= P .: (F -Ideal) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_P_.:_(F_-Ideal)_holds_ x_in_(P_.:_F)_-Ideal let x be set ; ::_thesis: ( x in P .: (F -Ideal) implies x in (P .: F) -Ideal ) assume x in P .: (F -Ideal) ; ::_thesis: x in (P .: F) -Ideal then consider x9 being set such that x9 in the carrier of R and A11: x9 in F -Ideal and A12: x = P . x9 by FUNCT_2:64; consider lc9 being LinearCombination of F such that A13: x9 = Sum lc9 by A11, IDEAL_1:60; consider E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] such that A14: E represents lc9 by IDEAL_1:35; consider lc being LinearCombination of P .: F such that A15: ( len lc9 = len 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)) ) ) by A14, IDEAL_1:36; P is RingMonomorphism by A1, QUOFIELD:def_21; then P is RingHomomorphism by QUOFIELD:def_20; then x = Sum lc by A12, A13, A14, A15, Th24; hence x in (P .: F) -Ideal by IDEAL_1:60; ::_thesis: verum end; then P .: (F -Ideal) c= (P .: F) -Ideal by TARSKI:def_3; hence P .: (F -Ideal) = (P .: F) -Ideal by A10, XBOOLE_0:def_10; ::_thesis: verum end; 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 & R is Noetherian holds S is Noetherian proof let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds S is Noetherian let P be Function of R,S; ::_thesis: ( P is RingIsomorphism & R is Noetherian implies S is Noetherian ) assume that A1: P is RingIsomorphism and A2: R is Noetherian ; ::_thesis: S is Noetherian now__::_thesis:_for_I_being_Ideal_of_S_holds_I_is_finitely_generated P is RingEpimorphism by A1, QUOFIELD:def_21; then A3: rng P = the carrier of S by QUOFIELD:def_19; let I be Ideal of S; ::_thesis: I is finitely_generated P is RingMonomorphism by A1, QUOFIELD:def_21; then A4: P is one-to-one by QUOFIELD:def_20; reconsider PI = (P ") .: I as Ideal of R by A1, Th22, Th25; PI is finitely_generated by A2, IDEAL_1:def_26; then consider F being non empty finite Subset of R such that A5: (P ") .: I = F -Ideal by IDEAL_1:def_25; P is onto by A3, FUNCT_2:def_3; then P " = P " by A4, TOPS_2:def_4; then P .: ((P ") .: I) = P .: (P " I) by A4, FUNCT_1:85; then P .: ((P ") .: I) = I by A3, FUNCT_1:77; then I = (P .: F) -Ideal by A1, A5, Th26; hence I is finitely_generated ; ::_thesis: verum end; hence S is Noetherian by IDEAL_1:def_26; ::_thesis: verum end; 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 proof deffunc H1( set ) -> Element of bool [:(Bags {}),{$1}:] = (Bags {}) --> $1; let R be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism consider P being Function such that A1: dom P = the carrier of R and A2: for x being set st x in the carrier of R holds P . x = H1(x) from FUNCT_1:sch_3(); now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_P_implies_y_in_the_carrier_of_(Polynom-Ring_(0,R))_)_&_(_y_in_the_carrier_of_(Polynom-Ring_(0,R))_implies_y_in_rng_P_)_) let y be set ; ::_thesis: ( ( y in rng P implies y in the carrier of (Polynom-Ring (0,R)) ) & ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) ) hereby ::_thesis: ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) assume y in rng P ; ::_thesis: y in the carrier of (Polynom-Ring (0,R)) then consider x being set such that A3: x in the carrier of R and A4: y = P . x by A1, FUNCT_1:def_3; reconsider x = x as Element of R by A3; reconsider y9 = (Bags {}) --> x as Function of (Bags {}),R ; Support y9 is finite by PRE_POLY:51; then y9 is finite-Support Series of 0,R by POLYNOM1:def_4; then y9 in the carrier of (Polynom-Ring (0,R)) by POLYNOM1:def_10; hence y in the carrier of (Polynom-Ring (0,R)) by A2, A4; ::_thesis: verum end; assume y in the carrier of (Polynom-Ring (0,R)) ; ::_thesis: y in rng P then reconsider y9 = y as Function of (Bags {}),R by POLYNOM1:def_10; A5: dom y9 = Bags {} by FUNCT_2:def_1; then A6: rng y9 = {(y9 . {})} by FUNCT_1:4, PRE_POLY:51; then y9 . {} in rng y9 by TARSKI:def_1; then reconsider x = y9 . {} as Element of R ; y9 = (Bags {}) --> (y9 . {}) by A5, A6, FUNCOP_1:9; then y = P . x by A2; hence y in rng P by A1, FUNCT_1:def_3; ::_thesis: verum end; then A7: rng P = the carrier of (Polynom-Ring (0,R)) by TARSKI:1; then reconsider P = P as Function of R,(Polynom-Ring (0,R)) by A1, FUNCT_2:1; A8: EmptyBag {} = {} --> 0 ; now__::_thesis:_for_x,_y_being_Element_of_R_holds_(P_._x)_+_(P_._y)_=_P_._(x_+_y) let x, y be Element of R; ::_thesis: (P . x) + (P . y) = P . (x + y) reconsider Px = P . x, Py = P . y, Pxy = P . (x + y) as Polynomial of 0,R by POLYNOM1:def_10; now__::_thesis:_for_z_being_bag_of_0_holds_Pxy_._z_=_(Px_._z)_+_(Py_._z) let z be bag of 0 ; ::_thesis: Pxy . z = (Px . z) + (Py . z) A9: z in Bags {} by PRE_POLY:def_12; A10: Py . z = ((Bags {}) --> y) . z by A2 .= y by A9, FUNCOP_1:7 ; A11: Px . z = ((Bags {}) --> x) . z by A2 .= x by A9, FUNCOP_1:7 ; Pxy . z = ((Bags {}) --> (x + y)) . z by A2 .= x + y by A9, FUNCOP_1:7 ; hence Pxy . z = (Px . z) + (Py . z) by A11, A10; ::_thesis: verum end; then Pxy = Px + Py by POLYNOM1:16; hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def_10; ::_thesis: verum end; then A12: P is additive by VECTSP_1:def_20; now__::_thesis:_for_x,_y_being_Element_of_R_holds_(P_._x)_*_(P_._y)_=_P_._(x_*_y) let x, y be Element of R; ::_thesis: (P . x) * (P . y) = P . (x * y) reconsider Px = P . x, Py = P . y, Pxy = P . (x * y) as Polynomial of 0,R by POLYNOM1:def_10; now__::_thesis:_for_b_being_bag_of_0_ex_s_being_FinSequence_of_the_carrier_of_R_st_ (_Pxy_._b_=_Sum_s_&_len_s_=_len_(decomp_b)_&_(_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_ ex_b1,_b2_being_bag_of_0_st_ (_(decomp_b)_/._k_=_<*b1,b2*>_&_s_/._k_=_(Px_._b1)_*_(Py_._b2)_)_)_) reconsider s = <*(x * y)*> as FinSequence of the carrier of R ; let b be bag of 0 ; ::_thesis: ex s being FinSequence of the carrier of R st ( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) ) take s = s; ::_thesis: ( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) ) A13: b in Bags {} by PRE_POLY:def_12; thus Pxy . b = ((Bags {}) --> (x * y)) . b by A2 .= x * y by A13, FUNCOP_1:7 .= Sum s by RLVECT_1:44 ; ::_thesis: ( len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) ) A14: decomp b = <*<*{},{}*>*> by Th2; A15: len s = 1 by FINSEQ_1:39; hence len s = len (decomp b) by A14, FINSEQ_1:39; ::_thesis: for k being Element of NAT st k in dom s holds ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) A16: len (decomp b) = 1 by A14, FINSEQ_1:39; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_ ex_b1,_b2_being_bag_of_0_st_ (_(decomp_b)_/._k_=_<*b1,b2*>_&_s_/._k_=_(Px_._b1)_*_(Py_._b2)_) set b1 = {} ; set b2 = {} ; let k be Element of NAT ; ::_thesis: ( k in dom s implies ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) A17: {} in Bags {} by PRE_POLY:51, TARSKI:def_1; then reconsider b1 = {} , b2 = {} as bag of 0 ; A18: Px . b1 = ((Bags {}) --> x) . b1 by A2 .= x by A17, FUNCOP_1:7 ; A19: Py . b2 = ((Bags {}) --> y) . b2 by A2 .= y by A17, FUNCOP_1:7 ; assume A20: k in dom s ; ::_thesis: ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) then A21: ( 1 <= k & k <= 1 ) by A15, FINSEQ_3:25; then A22: k = 1 by XXREAL_0:1; take b1 = b1; ::_thesis: ex b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) take b2 = b2; ::_thesis: ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) k in dom (decomp b) by A16, A21, FINSEQ_3:25; hence (decomp b) /. k = (decomp b) . 1 by A22, PARTFUN1:def_6 .= <*b1,b2*> by A14, FINSEQ_1:40 ; ::_thesis: s /. k = (Px . b1) * (Py . b2) thus s /. k = s . 1 by A20, A22, PARTFUN1:def_6 .= (Px . b1) * (Py . b2) by A18, A19, FINSEQ_1:40 ; ::_thesis: verum end; hence for k being Element of NAT st k in dom s holds ex b1, b2 being bag of 0 st ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; ::_thesis: verum end; then Pxy = Px *' Py by POLYNOM1:def_9; hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def_10; ::_thesis: verum end; then A23: P is multiplicative by GROUP_6:def_6; take P ; ::_thesis: P is RingIsomorphism reconsider f0 = {{}} --> (0. R), f1 = {{}} --> (1_ R) as Function of {{}}, the carrier of R ; A24: dom f1 = {{}} by FUNCT_2:def_1; A25: dom f0 = {{}} by FUNCT_2:def_1; then A26: {} in dom ({{}} --> (0. R)) by TARSKI:def_1; 1_ (Polynom-Ring (0,R)) = 1_ (0,R) by POLYNOM1:31 .= (0_ (0,R)) +* ({},(1_ R)) by A8, POLYNOM1:def_8 .= ({{}} --> (0. R)) +* ({},(1_ R)) by POLYNOM1:def_7, PRE_POLY:51 .= ({{}} --> (0. R)) +* ({} .--> (1_ R)) by A26, FUNCT_7:def_3 .= {{}} --> (1_ R) by A25, A24, FUNCT_4:19 .= P . (1_ R) by A2, PRE_POLY:51 ; then P is unity-preserving by GROUP_1:def_13; then A27: P is RingHomomorphism by A12, A23, QUOFIELD:def_18; then A28: P is RingEpimorphism by A7, QUOFIELD:def_19; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_P_&_x2_in_dom_P_&_P_._x1_=_P_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom P & x2 in dom P & P . x1 = P . x2 implies x1 = x2 ) assume that A29: x1 in dom P and A30: x2 in dom P ; ::_thesis: ( P . x1 = P . x2 implies x1 = x2 ) assume P . x1 = P . x2 ; ::_thesis: x1 = x2 then (Bags {}) --> x1 = P . x2 by A2, A29; then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A30; hence x1 = x2 by FUNCT_4:6; ::_thesis: verum end; then P is one-to-one by FUNCT_1:def_4; then P is RingMonomorphism by A27, QUOFIELD:def_20; hence P is RingIsomorphism by A28, QUOFIELD:def_21; ::_thesis: verum end; 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 ) & p1 . b = Sum (g * F) ) proof let R be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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 ) & p1 . b = Sum (g * F) ) let n be Element of NAT ; ::_thesis: 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) ) let b be bag of n; ::_thesis: 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) ) let p1 be Polynomial of n,R; ::_thesis: 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) ) let F be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: ( p1 = Sum F implies 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) ) ) assume A1: p1 = Sum F ; ::_thesis: 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) ) set CR = the carrier of R; set PNR = Polynom-Ring (n,R); set CPNR = the carrier of (Polynom-Ring (n,R)); defpred S1[ Element of the carrier of (Polynom-Ring (n,R)), Element of the carrier of R] means for p being Polynomial of n,R st p = $1 holds $2 = p . b; A2: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_(n,R))_ex_y_being_Element_of_the_carrier_of_R_st_S1[x,y] let x be Element of the carrier of (Polynom-Ring (n,R)); ::_thesis: ex y being Element of the carrier of R st S1[x,y] reconsider x9 = x as Polynomial of n,R by POLYNOM1:def_10; S1[x,x9 . b] ; hence ex y being Element of the carrier of R st S1[x,y] ; ::_thesis: verum end; consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that A3: for x being Element of the carrier of (Polynom-Ring (n,R)) holds S1[x,g . x] from FUNCT_2:sch_3(A2); take g ; ::_thesis: ( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) ) now__::_thesis:_for_p_being_Polynomial_of_n,R_holds_g_._p_=_p_._b let p be Polynomial of n,R; ::_thesis: g . p = p . b reconsider p9 = p as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10; S1[p9,g . p9] by A3; hence g . p = p . b ; ::_thesis: verum end; hence for p being Polynomial of n,R holds g . p = p . b ; ::_thesis: p1 . b = Sum (g * F) defpred S2[ Nat] means for F9 being FinSequence of the carrier of (Polynom-Ring (n,R)) for p19 being Polynomial of n,R st len F9 <= $1 & p19 = Sum F9 holds p19 . b = Sum (g * F9); A4: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A5: S2[k] ; ::_thesis: S2[k + 1] now__::_thesis:_for_F9_being_FinSequence_of_the_carrier_of_(Polynom-Ring_(n,R)) for_p19_being_Polynomial_of_n,R_st_len_F9_<=_k_+_1_&_p19_=_Sum_F9_holds_ p19_._b_=_Sum_(g_*_F9) let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: for p19 being Polynomial of n,R st len F9 <= k + 1 & p19 = Sum F9 holds b3 . b = Sum (g * b2) let p19 be Polynomial of n,R; ::_thesis: ( len F9 <= k + 1 & p19 = Sum F9 implies b2 . b = Sum (g * b1) ) assume that A6: len F9 <= k + 1 and A7: p19 = Sum F9 ; ::_thesis: b2 . b = Sum (g * b1) percases ( len F9 < k + 1 or len F9 >= k + 1 ) ; suppose len F9 < k + 1 ; ::_thesis: b2 . b = Sum (g * b1) then len F9 <= k by NAT_1:13; hence p19 . b = Sum (g * F9) by A5, A7; ::_thesis: verum end; suppose len F9 >= k + 1 ; ::_thesis: b2 . b = Sum (g * b1) then len F9 = k + 1 by A6, XXREAL_0:1; then consider p, q being FinSequence such that A8: len p = k and A9: len q = 1 and A10: F9 = p ^ q by FINSEQ_2:22; rng q c= rng F9 by A10, FINSEQ_1:30; then rng q c= the carrier of (Polynom-Ring (n,R)) by XBOOLE_1:1; then reconsider q = q as FinSequence of the carrier of (Polynom-Ring (n,R)) by FINSEQ_1:def_4; rng p c= rng F9 by A10, FINSEQ_1:29; then rng p c= the carrier of (Polynom-Ring (n,R)) by XBOOLE_1:1; then reconsider p = p as FinSequence of the carrier of (Polynom-Ring (n,R)) by FINSEQ_1:def_4; A11: Sum F9 = (Sum p) + (Sum q) by A10, RLVECT_1:41; reconsider p9 = Sum p as Polynomial of n,R by POLYNOM1:def_10; A12: g * F9 = (g * p) ^ (g * q) by A10, FINSEQOP:9; 1 in dom q by A9, FINSEQ_3:25; then q . 1 in rng q by FUNCT_1:def_3; then reconsider q9 = q . 1 as Element of the carrier of (Polynom-Ring (n,R)) ; reconsider q99 = q9 as Polynomial of n,R by POLYNOM1:def_10; A13: q = <*q9*> by A9, FINSEQ_1:40; then g * q = <*(g . q9)*> by FINSEQ_2:35 .= <*(q99 . b)*> by A3 ; then A14: Sum (g * q) = q99 . b by RLVECT_1:44; q9 = Sum q by A13, RLVECT_1:44; then A15: p19 = p9 + q99 by A7, A11, POLYNOM1:def_10; p9 . b = Sum (g * p) by A5, A8; hence p19 . b = (Sum (g * p)) + (Sum (g * q)) by A14, A15, POLYNOM1:15 .= Sum (g * F9) by A12, RLVECT_1:41 ; ::_thesis: verum end; end; end; hence S2[k + 1] ; ::_thesis: verum end; A16: S2[ 0 ] proof let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: for p19 being Polynomial of n,R st len F9 <= 0 & p19 = Sum F9 holds p19 . b = Sum (g * F9) let p19 be Polynomial of n,R; ::_thesis: ( len F9 <= 0 & p19 = Sum F9 implies p19 . b = Sum (g * F9) ) assume that A17: len F9 <= 0 and A18: p19 = Sum F9 ; ::_thesis: p19 . b = Sum (g * F9) A19: F9 = <*> the carrier of (Polynom-Ring (n,R)) by A17; then g * F9 = <*> the carrier of R ; then A20: Sum (g * F9) = 0. R by RLVECT_1:43; p19 = 0. (Polynom-Ring (n,R)) by A18, A19, RLVECT_1:43 .= 0_ (n,R) by POLYNOM1:def_10 ; hence p19 . b = Sum (g * F9) by A20, POLYNOM1:22; ::_thesis: verum end; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A16, A4); then S2[ len F] ; hence p1 . b = Sum (g * F) by A1; ::_thesis: verum 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 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 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 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) proof set CR = the carrier of R; set PNR = Polynom-Ring (n,R); set PN1R = Polynom-Ring ((n + 1),R); set PRPNR = Polynom-Ring (Polynom-Ring (n,R)); set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R))); set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); defpred S1[ Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), Element of the carrier of (Polynom-Ring ((n + 1),R))] means 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 p1 = $1 & p3 = $2 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n); A1: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_((n_+_1),R))_st_S1[x,y] let x be Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y] reconsider p1 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; defpred S2[ Element of Bags (n + 1), Element of the carrier of R] means for p2 being Polynomial of n,R st p2 = p1 . ($1 . n) holds $2 = p2 . ($1 | n); deffunc H1( set ) -> set = { b where b is Element of Bags (n + 1) : ( b . n = $1 & ( for p2 being Polynomial of n,R st p2 = p1 . $1 holds b | n in Support p2 ) ) } ; A2: now__::_thesis:_for_k_being_set_st_k_in_NAT_holds_ H1(k)_in_bool_(Bags_(n_+_1)) let k be set ; ::_thesis: ( k in NAT implies H1(k) in bool (Bags (n + 1)) ) assume k in NAT ; ::_thesis: H1(k) in bool (Bags (n + 1)) set Ak = H1(k); H1(k) c= Bags (n + 1) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in H1(k) or b in Bags (n + 1) ) assume b in H1(k) ; ::_thesis: b in Bags (n + 1) then ex b9 being Element of Bags (n + 1) st ( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds b9 | n in Support p2 ) ) ; hence b in Bags (n + 1) ; ::_thesis: verum end; hence H1(k) in bool (Bags (n + 1)) ; ::_thesis: verum end; consider A being Function of NAT,(bool (Bags (n + 1))) such that A3: for k being set st k in NAT holds A . k = H1(k) from FUNCT_2:sch_2(A2); now__::_thesis:_for_X_being_set_st_X_in_A_.:_(len_p1)_holds_ X_is_finite let X be set ; ::_thesis: ( X in A .: (len p1) implies b1 is finite ) assume X in A .: (len p1) ; ::_thesis: b1 is finite then consider k being Element of NAT such that k in len p1 and A4: X = A . k by FUNCT_2:65; reconsider p2 = p1 . k as Polynomial of n,R by POLYNOM1:def_10; A5: A . k = { b where b is Element of Bags (n + 1) : ( b . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds b | n in Support p2 ) ) } by A3; percases ( Support p2 = {} or Support p2 <> {} ) ; supposeA6: Support p2 = {} ; ::_thesis: b1 is finite now__::_thesis:_not_A_._k_<>_{} assume A . k <> {} ; ::_thesis: contradiction then consider b being set such that A7: b in A . k by XBOOLE_0:def_1; ex b9 being Element of Bags (n + 1) st ( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds b9 | n in Support p2 ) ) by A5, A7; hence contradiction by A6; ::_thesis: verum end; hence X is finite by A4; ::_thesis: verum end; supposeA8: Support p2 <> {} ; ::_thesis: b1 is finite then consider b2 being set such that A9: b2 in Support p2 by XBOOLE_0:def_1; reconsider b2 = b2 as Element of Bags n by A9; A10: (b2 bag_extend k) . n = k by Def1; for p2 being Polynomial of n,R st p2 = p1 . k holds (b2 bag_extend k) | n in Support p2 by A9, Def1; then b2 bag_extend k in A . k by A5, A10; then reconsider Ak = A . k as non empty set ; reconsider Supportp2 = Support p2 as non empty set by A8; defpred S3[ Element of Ak, Element of Supportp2] means for b being Element of Bags (n + 1) st $1 = b holds $2 = b | n; A11: now__::_thesis:_for_x_being_Element_of_Ak_ex_y_being_Element_of_Supportp2_st_S3[x,y] let x be Element of Ak; ::_thesis: ex y being Element of Supportp2 st S3[x,y] x in A . k ; then consider b being Element of Bags (n + 1) such that A12: b = x and b . n = k and A13: for p2 being Polynomial of n,R st p2 = p1 . k holds b | n in Support p2 by A5; reconsider bn = b | n as Element of Supportp2 by A13; S3[x,bn] by A12; hence ex y being Element of Supportp2 st S3[x,y] ; ::_thesis: verum end; consider f being Function of Ak,Supportp2 such that A14: for x being Element of Ak holds S3[x,f . x] from FUNCT_2:sch_3(A11); A15: dom f = Ak by FUNCT_2:def_1; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A16: x1 in dom f and A17: x2 in dom f and A18: f . x1 = f . x2 ; ::_thesis: x1 = x2 f . x1 in Supportp2 by A16, FUNCT_2:5; then reconsider fx1 = f . x1 as Element of Bags n ; consider b1 being Element of Bags (n + 1) such that A19: b1 = x1 and A20: b1 . n = k and for p2 being Polynomial of n,R st p2 = p1 . k holds b1 | n in Support p2 by A5, A15, A16; b1 | n = f . x1 by A14, A16, A19; then A21: b1 = fx1 bag_extend k by A20, Def1; consider b2 being Element of Bags (n + 1) such that A22: b2 = x2 and A23: b2 . n = k and for p2 being Polynomial of n,R st p2 = p1 . k holds b2 | n in Support p2 by A5, A15, A17; b2 | n = f . x1 by A14, A17, A18, A22; hence x1 = x2 by A19, A21, A22, A23, Def1; ::_thesis: verum end; then A24: f is one-to-one by FUNCT_1:def_4; rng f c= Supportp2 ; then card Ak c= card Supportp2 by A15, A24, CARD_1:10; hence X is finite by A4; ::_thesis: verum end; end; end; then A25: union (A .: (len p1)) is finite by FINSET_1:7; A26: now__::_thesis:_for_b_being_Element_of_Bags_(n_+_1)_ex_r_being_Element_of_the_carrier_of_R_st_S2[b,r] let b be Element of Bags (n + 1); ::_thesis: ex r being Element of the carrier of R st S2[b,r] reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by XREAL_1:29; then reconsider bn = b | n as bag of n by Th3; S2[b,p2 . bn] ; hence ex r being Element of the carrier of R st S2[b,r] ; ::_thesis: verum end; consider y being Function of (Bags (n + 1)), the carrier of R such that A27: for b being Element of Bags (n + 1) holds S2[b,y . b] from FUNCT_2:sch_3(A26); reconsider y = y as Function of (Bags (n + 1)),R ; reconsider y = y as Series of (n + 1),R ; Support y c= union (A .: (len p1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support y or x in union (A .: (len p1)) ) A28: dom A = NAT by FUNCT_2:def_1; assume A29: x in Support y ; ::_thesis: x in union (A .: (len p1)) then reconsider x9 = x as Element of Bags (n + 1) ; reconsider p2 = p1 . (x9 . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by XREAL_1:29; then reconsider xn = x9 | n as Element of Bags n by Th3; y . x9 <> 0. R by A29, POLYNOM1:def_3; then A30: p2 . xn <> 0. R by A27; then p2 <> 0_ (n,R) by POLYNOM1:22; then p2 <> 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10; then A31: x9 . n < len p1 by ALGSEQ_1:8; len p1 = { i where i is Element of NAT : i < len p1 } by AXIOMS:4; then x9 . n in len p1 by A31; then A32: A . (x9 . n) in A .: (len p1) by A28, FUNCT_1:def_6; A33: A . (x9 . n) = { b where b is Element of Bags (n + 1) : ( b . n = x9 . n & ( for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds b | n in Support p2 ) ) } by A3; for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds xn in Support p2 by A30, POLYNOM1:def_3; then x in A . (x9 . n) by A33; hence x in union (A .: (len p1)) by A32, TARSKI:def_4; ::_thesis: verum end; then y is finite-Support by A25, POLYNOM1:def_4; then reconsider y9 = y as Element of the carrier of (Polynom-Ring ((n + 1),R)) by POLYNOM1:def_10; now__::_thesis:_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_p1_=_x_&_p3_=_y9_&_p2_=_p1_._(b_._n)_holds_ p3_._b_=_p2_._(b_|_n) let p1 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for p2 being Polynomial of n,R for p3 being Polynomial of (n + 1),R for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (n + 1),R for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let p3 be Polynomial of (n + 1),R; ::_thesis: for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let b be bag of n + 1; ::_thesis: ( p1 = x & p3 = y9 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) ) A34: b is Element of Bags (n + 1) by PRE_POLY:def_12; assume ( p1 = x & p3 = y9 & p2 = p1 . (b . n) ) ; ::_thesis: p3 . b = p2 . (b | n) hence p3 . b = p2 . (b | n) by A27, A34; ::_thesis: verum end; hence ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y] ; ::_thesis: verum end; consider P being Function of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), the carrier of (Polynom-Ring ((n + 1),R)) such that A35: for x being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) holds S1[x,P . x] from FUNCT_2:sch_3(A1); reconsider P = P as Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) ; take P ; ::_thesis: 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 = P . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) now__::_thesis:_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_=_P_._p1_&_p2_=_p1_._(b_._n)_holds_ p3_._b_=_p2_._(b_|_n) let p1 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for p2 being Polynomial of n,R for p3 being Polynomial of (n + 1),R for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (n + 1),R for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let p3 be Polynomial of (n + 1),R; ::_thesis: for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) let b be bag of n + 1; ::_thesis: ( p3 = P . p1 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) ) A36: p1 in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def_10; assume ( p3 = P . p1 & p2 = p1 . (b . n) ) ; ::_thesis: p3 . b = p2 . (b | n) hence p3 . b = p2 . (b | n) by A35, A36; ::_thesis: verum end; hence 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 = P . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) ; ::_thesis: verum end; 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 & 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 = b2 . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) ) holds b1 = b2 proof let A, B be Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)); ::_thesis: ( ( 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 = A . 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 . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) ) implies A = B ) set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R))); set PNR = Polynom-Ring (n,R); assume A37: 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 = A . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) ; ::_thesis: ( ex p1 being Polynomial of (Polynom-Ring (n,R)) ex p2 being Polynomial of n,R ex p3 being Polynomial of (n + 1),R ex b being bag of n + 1 st ( p3 = B . p1 & p2 = p1 . (b . n) & not p3 . b = p2 . (b | n) ) or A = B ) assume A38: 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 . p1 & p2 = p1 . (b . n) holds p3 . b = p2 . (b | n) ; ::_thesis: A = B now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_holds_ A_._x_=_B_._x let x be set ; ::_thesis: ( x in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) implies A . x = B . x ) assume A39: x in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) ; ::_thesis: A . x = B . x then reconsider x9 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; ( A . x in the carrier of (Polynom-Ring ((n + 1),R)) & B . x in the carrier of (Polynom-Ring ((n + 1),R)) ) by A39, FUNCT_2:5; then reconsider Ax = A . x, Bx = B . x as Polynomial of (n + 1),R by POLYNOM1:def_10; now__::_thesis:_for_b_being_set_st_b_in_Bags_(n_+_1)_holds_ Ax_._b_=_Bx_._b let b be set ; ::_thesis: ( b in Bags (n + 1) implies Ax . b = Bx . b ) assume b in Bags (n + 1) ; ::_thesis: Ax . b = Bx . b then reconsider b9 = b as Element of Bags (n + 1) ; reconsider p2 = x9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by NAT_1:13; then reconsider bn = b9 | n as Element of Bags n by Th3; thus Ax . b = p2 . bn by A37 .= Bx . b by A38 ; ::_thesis: verum end; hence A . x = B . x by FUNCT_2:12; ::_thesis: verum end; hence A = B by FUNCT_2:12; ::_thesis: verum end; 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 & 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 proof set P = upm (n,R); set PNR = Polynom-Ring (n,R); thus upm (n,R) is additive ::_thesis: verum proof let x, y be Element of (Polynom-Ring (Polynom-Ring (n,R))); :: according to VECTSP_1:def_20 ::_thesis: (upm (n,R)) . (x + y) = ((upm (n,R)) . x) + ((upm (n,R)) . y) reconsider x9 = x, y9 = y, xy9 = x + y as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; reconsider Pxy = (upm (n,R)) . (x + y), Px = (upm (n,R)) . x, Py = (upm (n,R)) . y as Polynomial of (n + 1),R by POLYNOM1:def_10; A1: xy9 = x9 + y9 by POLYNOM3:def_10; now__::_thesis:_for_b_being_set_st_b_in_Bags_(n_+_1)_holds_ Pxy_._b_=_(Px_+_Py)_._b let b be set ; ::_thesis: ( b in Bags (n + 1) implies Pxy . b = (Px + Py) . b ) assume b in Bags (n + 1) ; ::_thesis: Pxy . b = (Px + Py) . b then reconsider b9 = b as bag of n + 1 ; reconsider xybn = (x9 + y9) . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10; reconsider xbn = x9 . (b9 . n), ybn = y9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by XREAL_1:29; then reconsider bn = b9 | n as bag of n by Th3; A2: ( xbn . bn = Px . b9 & ybn . bn = Py . b9 ) by Def6; (x9 + y9) . (b9 . n) = (x9 . (b9 . n)) + (y9 . (b9 . n)) by NORMSP_1:def_2; then xybn = xbn + ybn by POLYNOM1:def_10; hence Pxy . b = (xbn + ybn) . bn by A1, Def6 .= (Px . b9) + (Py . b9) by A2, POLYNOM1:15 .= (Px + Py) . b by POLYNOM1:15 ; ::_thesis: verum end; hence (upm (n,R)) . (x + y) = Px + Py by FUNCT_2:12 .= ((upm (n,R)) . x) + ((upm (n,R)) . y) by POLYNOM1:def_10 ; ::_thesis: verum end; end; cluster upm (n,R) -> multiplicative ; coherence upm (n,R) is multiplicative proof set P = upm (n,R); set CR = the carrier of R; set PNR = Polynom-Ring (n,R); set CPNR = the carrier of (Polynom-Ring (n,R)); thus upm (n,R) is multiplicative ::_thesis: verum proof let x9, y9 be Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))); :: according to GROUP_6:def_6 ::_thesis: (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9) reconsider x = x9, y = y9, xy = x9 * y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; reconsider Pxy = (upm (n,R)) . (x9 * y9), PxPy = ((upm (n,R)) . x9) * ((upm (n,R)) . y9), Px = (upm (n,R)) . x9, Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def_10; A3: xy = x *' y by POLYNOM3:def_10; A4: PxPy = Px *' Py by POLYNOM1:def_10; now__::_thesis:_for_b9_being_set_st_b9_in_Bags_(n_+_1)_holds_ Pxy_._b9_=_PxPy_._b9 let b9 be set ; ::_thesis: ( b9 in Bags (n + 1) implies Pxy . b9 = PxPy . b9 ) assume b9 in Bags (n + 1) ; ::_thesis: Pxy . b9 = PxPy . b9 then reconsider b = b9 as Element of Bags (n + 1) ; consider r being FinSequence of the carrier of (Polynom-Ring (n,R)) such that A5: len r = (b . n) + 1 and A6: xy . (b . n) = Sum r and A7: for k being Element of NAT st k in dom r holds r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A3, POLYNOM3:def_9; n < n + 1 by NAT_1:13; then reconsider bn = b | n as Element of Bags n by Th3; defpred S1[ set , set ] means for p, q being Polynomial of n,R for fcr being FinSequence of the carrier of R for i being Element of NAT st i = R & p = x . (i -' 1) & q = y . (((b . n) + 1) -' i) & fcr = n holds ( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds ex b1, b2 being bag of n st ( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) ); reconsider xybn = xy . (b . n) as Polynomial of n,R by POLYNOM1:def_10; consider u being FinSequence of the carrier of R such that A8: PxPy . b = Sum u and A9: len u = len (decomp b) and A10: for k being Element of NAT st k in dom u holds ex b1, b2 being bag of n + 1 st ( (decomp b) /. k = <*b1,b2*> & u /. k = (Px . b1) * (Py . b2) ) by A4, POLYNOM1:def_9; A11: now__::_thesis:_for_e9_being_set_st_e9_in_dom_r_holds_ ex_u_being_set_st_ (_u_in_the_carrier_of_R_*_&_S1[e9,u]_) let e9 be set ; ::_thesis: ( e9 in dom r implies ex u being set st ( u in the carrier of R * & S1[e9,u] ) ) assume e9 in dom r ; ::_thesis: ex u being set st ( u in the carrier of R * & S1[e9,u] ) then reconsider e = e9 as Element of NAT ; reconsider p = x . (e -' 1), q = y . (((b . n) + 1) -' e) as Polynomial of n,R by POLYNOM1:def_10; consider fcr being FinSequence of the carrier of R such that A12: ( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds ex b1, b2 being bag of n st ( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def_9; A13: fcr in the carrier of R * by FINSEQ_1:def_11; S1[e,fcr] by A12; hence ex u being set st ( u in the carrier of R * & S1[e9,u] ) by A13; ::_thesis: verum end; consider s being Function of (dom r),( the carrier of R *) such that A14: for e being set st e in dom r holds S1[e,s . e] from FUNCT_2:sch_1(A11); A15: rng s c= the carrier of R * ; A16: dom s = dom r by FUNCT_2:def_1; then ex n being Nat st dom s = Seg n by FINSEQ_1:def_2; then s is FinSequence-like by FINSEQ_1:def_2; then reconsider s = s as FinSequence of the carrier of R * by A15, FINSEQ_1:def_4; consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that A17: for p being Polynomial of n,R holds g . p = p . bn and A18: xybn . bn = Sum (g * r) by A6, Th29; A19: Sum (g * r) = Pxy . b by A18, Def6; 0 + 1 <= len r by A5, XREAL_1:6; then A20: 1 in dom s by A16, FINSEQ_3:25; A21: now__::_thesis:_len_(s_._1)_<>_0 reconsider p9 = x . (1 -' 1), q9 = y . (((b . n) + 1) -' 1) as Polynomial of n,R by POLYNOM1:def_10; s /. 1 is FinSequence of the carrier of R ; then A22: s . 1 is FinSequence of the carrier of R by A20, PARTFUN1:def_6; ( p9 = x . (1 -' 1) & q9 = y . (((b . n) + 1) -' 1) ) ; hence len (s . 1) <> 0 by A14, A16, A20, A22; ::_thesis: verum end; defpred S2[ set , set ] means for i, n1 being Element of NAT for b1 being bag of n + 1 st n1 = R & b1 = (divisors b) . n1 & i in dom (divisors bn) & (divisors bn) . i = b1 | n holds ( (b1 . n) + 1 in dom s & i in dom (s . ((b1 . n) + 1)) & n = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i ); set t = FlattenSeq s; A23: now__::_thesis:_for_n19_being_set_st_n19_in_dom_u_holds_ ex_n29_being_set_st_ (_n29_in_dom_(FlattenSeq_s)_&_S2[n19,n29]_) let n19 be set ; ::_thesis: ( n19 in dom u implies ex n29 being set st ( n29 in dom (FlattenSeq s) & S2[n19,n29] ) ) assume A24: n19 in dom u ; ::_thesis: ex n29 being set st ( n29 in dom (FlattenSeq s) & S2[n19,n29] ) then reconsider n1 = n19 as Element of NAT ; dom u = dom (decomp b) by A9, FINSEQ_3:29 .= dom (divisors b) by PRE_POLY:def_17 ; then A25: (divisors b) . n1 in rng (divisors b) by A24, FUNCT_1:def_3; then reconsider b1 = (divisors b) . n1 as bag of n + 1 ; A26: b1 divides b by A25, Th7; then b1 . n <= b . n by PRE_POLY:def_11; then A27: (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6; n < n + 1 by NAT_1:13; then reconsider b1n = b1 | n as Element of Bags n by Th3; reconsider p = x . (((b1 . n) + 1) -' 1), q = y . (((b . n) + 1) -' ((b1 . n) + 1)) as Polynomial of n,R by POLYNOM1:def_10; A28: ( p = x . (((b1 . n) + 1) -' 1) & q = y . (((b . n) + 1) -' ((b1 . n) + 1)) ) ; b1n divides bn by A26, Th4; then b1n in rng (divisors bn) by Th7; then consider i being set such that A29: i in dom (divisors bn) and A30: b1n = (divisors bn) . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A29; set n2 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i; A31: (b1 . n) + 1 >= 1 + 0 by XREAL_1:6; then A32: (b1 . n) + 1 in dom s by A5, A16, A27, FINSEQ_3:25; then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5; then len (s . ((b1 . n) + 1)) = len (decomp bn) by A14, A16, A32, A28; then A33: dom (s . ((b1 . n) + 1)) = dom (decomp bn) by FINSEQ_3:29 .= dom (divisors bn) by PRE_POLY:def_17 ; then A34: (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s) by A29, A32, PRE_POLY:30; for i9, n19 being Element of NAT for b19 being bag of n + 1 st n19 = n1 & b19 = (divisors b) . n19 & i9 in dom (divisors bn) & (divisors bn) . i9 = b19 | n holds ( (b19 . n) + 1 in dom s & i9 in dom (s . ((b19 . n) + 1)) & (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b19 . n) + 1) -' 1)))) + i9 ) by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:25, FUNCT_1:def_4; hence ex n29 being set st ( n29 in dom (FlattenSeq s) & S2[n19,n29] ) by A34; ::_thesis: verum end; consider p being Function of (dom u),(dom (FlattenSeq s)) such that A35: for x being set st x in dom u holds S2[x,p . x] from FUNCT_2:sch_1(A23); 1 in dom (Card s) by A20, CARD_3:def_2; then Sum (Card s) >= (Card s) . 1 by POLYNOM3:4; then Sum (Card s) > 0 by A20, A21, CARD_3:def_2; then len (FlattenSeq s) > 0 by PRE_POLY:27; then A36: FlattenSeq s <> {} ; then A37: dom p = dom u by FUNCT_2:def_1; now__::_thesis:_for_n19,_n29_being_set_st_n19_in_dom_p_&_n29_in_dom_p_&_p_._n19_=_p_._n29_holds_ n19_=_n29 let n19, n29 be set ; ::_thesis: ( n19 in dom p & n29 in dom p & p . n19 = p . n29 implies n19 = n29 ) assume that A38: n19 in dom p and A39: n29 in dom p and A40: p . n19 = p . n29 ; ::_thesis: n19 = n29 dom p = dom u by A36, FUNCT_2:def_1; then reconsider n1 = n19, n2 = n29 as Element of NAT by A38, A39; A41: dom u = dom (decomp b) by A9, FINSEQ_3:29 .= dom (divisors b) by PRE_POLY:def_17 ; then A42: (divisors b) . n1 in rng (divisors b) by A38, FUNCT_1:def_3; then reconsider b1 = (divisors b) . n1 as bag of n + 1 ; A43: (divisors b) . n2 in rng (divisors b) by A39, A41, FUNCT_1:def_3; then reconsider b2 = (divisors b) . n2 as bag of n + 1 ; n < n + 1 by NAT_1:13; then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3; A44: ( (Card s) | (((b1 . n) + 1) -' 1) = Card (s | (((b1 . n) + 1) -' 1)) & (Card s) | (((b2 . n) + 1) -' 1) = Card (s | (((b2 . n) + 1) -' 1)) ) by POLYNOM3:16; b2 divides b by A43, Th7; then b2n divides bn by Th4; then b2n in rng (divisors bn) by Th7; then consider i2 being set such that A45: i2 in dom (divisors bn) and A46: b2n = (divisors bn) . i2 by FUNCT_1:def_3; reconsider i2 = i2 as Element of NAT by A45; A47: ( (b2 . n) + 1 in dom s & i2 in dom (s . ((b2 . n) + 1)) ) by A35, A39, A45, A46; b1 divides b by A42, Th7; then b1n divides bn by Th4; then b1n in rng (divisors bn) by Th7; then consider i1 being set such that A48: i1 in dom (divisors bn) and A49: b1n = (divisors bn) . i1 by FUNCT_1:def_3; reconsider i1 = i1 as Element of NAT by A48; A50: p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1 by A35, A38, A48, A49; A51: p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2 by A35, A39, A45, A46; A52: b2 is Element of Bags (n + 1) by PRE_POLY:def_12; ( (b1 . n) + 1 in dom s & i1 in dom (s . ((b1 . n) + 1)) ) by A35, A38, A48, A49; then A53: ( (b1 . n) + 1 = (b2 . n) + 1 & i1 = i2 ) by A40, A50, A47, A51, A44, POLYNOM3:22; b1 is Element of Bags (n + 1) by PRE_POLY:def_12; then b1 = b1n bag_extend (b1 . n) by Def1 .= b2 by A49, A46, A53, A52, Def1 ; hence n19 = n29 by A38, A39, A41, FUNCT_1:def_4; ::_thesis: verum end; then A54: p is one-to-one by FUNCT_1:def_4; dom (FlattenSeq s) c= rng p proof let n19 be set ; :: according to TARSKI:def_3 ::_thesis: ( not n19 in dom (FlattenSeq s) or n19 in rng p ) assume A55: n19 in dom (FlattenSeq s) ; ::_thesis: n19 in rng p then reconsider n1 = n19 as Element of NAT ; consider i, j being Element of NAT such that A56: i in dom s and A57: j in dom (s . i) and A58: n1 = (Sum (Card (s | (i -' 1)))) + j and (s . i) . j = (FlattenSeq s) . n1 by A55, PRE_POLY:29; s . i in the carrier of R * by A16, A56, FUNCT_2:5; then A59: s . i is FinSequence of the carrier of R by FINSEQ_1:def_11; reconsider bj = (divisors bn) /. j as bag of n ; set bij = bj bag_extend (i -' 1); reconsider p9 = x . (i -' 1), q9 = y . (((b . n) + 1) -' i) as Polynomial of n,R by POLYNOM1:def_10; A60: (bj bag_extend (i -' 1)) . n = i -' 1 by Def1; 1 <= i by A56, FINSEQ_3:25; then A61: ((bj bag_extend (i -' 1)) . n) + 1 = i by A60, XREAL_1:235; A62: dom u = dom (decomp b) by A9, FINSEQ_3:29 .= dom (divisors b) by PRE_POLY:def_17 ; ( p9 = x . (i -' 1) & q9 = y . (((b . n) + 1) -' i) ) ; then len (s . i) = len (decomp bn) by A14, A16, A56, A59; then A63: dom (s . i) = dom (decomp bn) by FINSEQ_3:29 .= dom (divisors bn) by PRE_POLY:def_17 ; then A64: bj = (divisors bn) . j by A57, PARTFUN1:def_6; then bj in rng (divisors bn) by A57, A63, FUNCT_1:def_3; then A65: bj divides bn by Th7; now__::_thesis:_for_k_being_set_holds_(bj_bag_extend_(i_-'_1))_._k_<=_b_._k let k be set ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1 percases ( k in n + 1 or not k in n + 1 ) ; supposeA66: k in n + 1 ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1 now__::_thesis:_(bj_bag_extend_(i_-'_1))_._k_<=_b_._k percases ( k in n or not k in n ) ; supposeA67: k in n ; ::_thesis: (bj bag_extend (i -' 1)) . k <= b . k then A68: b . k = bn . k by FUNCT_1:49; (bj bag_extend (i -' 1)) . k = ((bj bag_extend (i -' 1)) | n) . k by A67, FUNCT_1:49 .= bj . k by Def1 ; hence (bj bag_extend (i -' 1)) . k <= b . k by A65, A68, PRE_POLY:def_11; ::_thesis: verum end; supposeA69: not k in n ; ::_thesis: (bj bag_extend (i -' 1)) . k <= b . k A70: 1 <= i by A56, FINSEQ_3:25; i <= (b . n) + 1 by A5, A16, A56, FINSEQ_3:25; then A71: i - 1 <= ((b . n) + 1) - 1 by XREAL_1:9; n + 1 = succ n by NAT_1:38 .= n \/ {n} by ORDINAL1:def_1 ; then k in {n} by A66, A69, XBOOLE_0:def_3; then A72: k = n by TARSKI:def_1; then (bj bag_extend (i -' 1)) . k = i -' 1 by Def1; hence (bj bag_extend (i -' 1)) . k <= b . k by A72, A70, A71, XREAL_1:233; ::_thesis: verum end; end; end; hence (bj bag_extend (i -' 1)) . k <= b . k ; ::_thesis: verum end; supposeA73: not k in n + 1 ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1 dom (bj bag_extend (i -' 1)) = n + 1 by PARTFUN1:def_2; hence (bj bag_extend (i -' 1)) . k <= b . k by A73, FUNCT_1:def_2; ::_thesis: verum end; end; end; then bj bag_extend (i -' 1) divides b by PRE_POLY:def_11; then bj bag_extend (i -' 1) in rng (divisors b) by Th7; then consider k being set such that A74: k in dom (divisors b) and A75: bj bag_extend (i -' 1) = (divisors b) . k by FUNCT_1:def_3; A76: dom p = dom u by A36, FUNCT_2:def_1; (divisors bn) . j = (bj bag_extend (i -' 1)) | n by A64, Def1; then p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j by A35, A57, A63, A74, A75, A62; hence n19 in rng p by A58, A74, A76, A62, A61, FUNCT_1:def_3; ::_thesis: verum end; then A77: rng p = dom (FlattenSeq s) by XBOOLE_0:def_10; len (Sum s) = len s by MATRLIN:def_6; then A78: dom (Sum s) = dom r by A16, FINSEQ_3:29; A79: now__::_thesis:_for_k_being_Nat_st_k_in_dom_r_holds_ (Sum_s)_._k_=_(g_*_r)_._k let k be Nat; ::_thesis: ( k in dom r implies (Sum s) . k = (g * r) . k ) reconsider p = x . (k -' 1), q = y . (((b . n) + 1) -' k) as Polynomial of n,R by POLYNOM1:def_10; reconsider pq9 = p *' q as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10; assume A80: k in dom r ; ::_thesis: (Sum s) . k = (g * r) . k then reconsider sk = s . k as Element of the carrier of R * by FUNCT_2:5; reconsider sk = sk as FinSequence of the carrier of R ; A81: r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A7, A80 .= pq9 by POLYNOM1:def_10 ; ( (Sum s) /. k = (Sum s) . k & s /. k = s . k ) by A16, A78, A80, PARTFUN1:def_6; hence (Sum s) . k = Sum sk by A78, A80, MATRLIN:def_6 .= (p *' q) . bn by A14, A80 .= g . (r . k) by A17, A81 .= (g * r) . k by A80, FUNCT_1:13 ; ::_thesis: verum end; A82: now__::_thesis:_for_n1_being_Element_of_NAT_st_n1_in_dom_u_holds_ u_._n1_=_(FlattenSeq_s)_._(p_._n1) let n1 be Element of NAT ; ::_thesis: ( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) ) reconsider b19 = (divisors b) /. n1 as bag of n + 1 ; assume A83: n1 in dom u ; ::_thesis: u . n1 = (FlattenSeq s) . (p . n1) then consider b1, b2 being bag of n + 1 such that A84: (decomp b) /. n1 = <*b1,b2*> and A85: u /. n1 = (Px . b1) * (Py . b2) by A10; A86: dom u = dom (decomp b) by A9, FINSEQ_3:29; then A87: <*b1,b2*> = <*b19,(b -' b19)*> by A83, A84, PRE_POLY:def_17; then A88: b1 = b19 by FINSEQ_1:77; reconsider xb1n = x . (b1 . n), yb2n = y . (b2 . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by NAT_1:13; then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3; A89: u . n1 = (Px . b1) * (Py . b2) by A83, A85, PARTFUN1:def_6 .= (xb1n . b1n) * (Py . b2) by Def6 .= (xb1n . b1n) * (yb2n . b2n) by Def6 ; A90: b2 = b -' b19 by A87, FINSEQ_1:77; A91: n1 in dom (divisors b) by A83, A86, PRE_POLY:def_17; then A92: b1 = (divisors b) . n1 by A88, PARTFUN1:def_6; then b1 in rng (divisors b) by A91, FUNCT_1:def_3; then A93: b1 divides b by Th7; then b1n divides bn by Th4; then b1n in rng (divisors bn) by Th7; then consider i being set such that A94: i in dom (divisors bn) and A95: b1n = (divisors bn) . i by FUNCT_1:def_3; reconsider i = i as Element of NAT by A94; A96: b1 . n <= b . n by A93, PRE_POLY:def_11; then (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6; then A97: ((b . n) + 1) -' ((b1 . n) + 1) = ((b . n) + 1) - ((b1 . n) + 1) by XREAL_1:233 .= (((b . n) - (b1 . n)) + 1) - 1 .= (b . n) -' (b1 . n) by A96, XREAL_1:233 .= b2 . n by A88, A90, PRE_POLY:def_6 ; A98: ((b1 . n) + 1) -' 1 = ((b1 . n) + 1) - 1 by NAT_D:37 .= b1 . n ; then A99: xb1n = x . (((b1 . n) + 1) -' 1) ; A100: (b1 . n) + 1 in dom s by A35, A83, A92, A94, A95; then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5; then reconsider sb1n1 = s . ((b1 . n) + 1) as FinSequence of the carrier of R ; A101: i in dom (s . ((b1 . n) + 1)) by A35, A83, A92, A94, A95; then consider B1, B2 being bag of n such that A102: (decomp bn) /. i = <*B1,B2*> and A103: sb1n1 /. i = (xb1n . B1) * (yb2n . B2) by A14, A16, A100, A98, A97; p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i by A35, A83, A92, A94, A95; then A104: (FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i by A100, A101, PRE_POLY:30; reconsider B19 = (divisors bn) /. i as bag of n ; A105: dom (divisors bn) = dom (decomp bn) by PRE_POLY:def_17; then A106: <*B1,B2*> = <*B19,(bn -' B19)*> by A94, A102, PRE_POLY:def_17; then A107: B1 = B19 by FINSEQ_1:77; then A108: B1 = b1n by A94, A95, PARTFUN1:def_6; yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) by A97; then len sb1n1 = len (decomp bn) by A14, A16, A100, A99; then A109: dom sb1n1 = dom (divisors bn) by A105, FINSEQ_3:29; B2 = bn -' B19 by A106, FINSEQ_1:77; then B2 = b2n by A88, A90, A107, A108, Th5; hence u . n1 = (FlattenSeq s) . (p . n1) by A89, A94, A104, A103, A108, A109, PARTFUN1:def_6; ::_thesis: verum end; dom r = dom (g * r) by FINSEQ_3:120; then Sum s = g * r by A78, A79, FINSEQ_1:13; then A110: Sum (FlattenSeq s) = Pxy . b by A19, POLYNOM1:14; A111: len u = card (dom u) by CARD_1:62 .= card p by A37, CARD_1:62 .= card (dom (FlattenSeq s)) by A54, A77, PRE_POLY:19 .= len (FlattenSeq s) by CARD_1:62 ; then A112: dom u = dom (FlattenSeq s) by FINSEQ_3:29; then p is Permutation of (dom u) by A54, A77, FUNCT_2:57; hence Pxy . b9 = PxPy . b9 by A110, A8, A82, A111, A112, RLVECT_2:6; ::_thesis: verum end; hence (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9) by FUNCT_2:12; ::_thesis: verum end; end; cluster upm (n,R) -> unity-preserving ; coherence upm (n,R) is unity-preserving proof set P = upm (n,R); set PNR = Polynom-Ring (n,R); set PN1R = Polynom-Ring ((n + 1),R); set PRPNR = Polynom-Ring (Polynom-Ring (n,R)); set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); reconsider p1 = 1_ (Polynom-Ring (Polynom-Ring (n,R))) as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; reconsider p19 = 1_ (Polynom-Ring ((n + 1),R)) as Polynomial of (n + 1),R by POLYNOM1:def_10; (upm (n,R)) . (1_ (Polynom-Ring (Polynom-Ring (n,R)))) in the carrier of (Polynom-Ring ((n + 1),R)) ; then reconsider p3 = (upm (n,R)) . p1 as Polynomial of (n + 1),R by POLYNOM1:def_10; now__::_thesis:_for_x_being_set_st_x_in_Bags_(n_+_1)_holds_ p3_._x_=_p19_._x let x be set ; ::_thesis: ( x in Bags (n + 1) implies p3 . x = p19 . x ) assume x in Bags (n + 1) ; ::_thesis: p3 . x = p19 . x then reconsider b = x as Element of Bags (n + 1) ; reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def_10; A113: p3 . b = p2 . (b | n) by Def6; now__::_thesis:_p3_._b_=_p19_._b percases ( ( b | n = EmptyBag n & b . n = 0 ) or b | n <> EmptyBag n or b . n <> 0 ) ; supposeA114: ( b | n = EmptyBag n & b . n = 0 ) ; ::_thesis: p3 . b = p19 . b then A115: b = (EmptyBag n) bag_extend 0 by Def1 .= EmptyBag (n + 1) by Th6 ; p2 = (1_. (Polynom-Ring (n,R))) . 0 by A114, POLYNOM3:def_10 .= 1_ (Polynom-Ring (n,R)) by POLYNOM3:30 .= 1_ (n,R) by POLYNOM1:31 ; hence p3 . b = 1_ R by A113, A114, POLYNOM1:25 .= (1_ ((n + 1),R)) . b by A115, POLYNOM1:25 .= p19 . b by POLYNOM1:31 ; ::_thesis: verum end; supposeA116: ( b | n <> EmptyBag n or b . n <> 0 ) ; ::_thesis: p3 . b = p19 . b A117: now__::_thesis:_p3_._b_=_0._R n < n + 1 by NAT_1:13; then A118: b | n is bag of n by Th3; A119: p2 = (1_. (Polynom-Ring (n,R))) . (b . n) by POLYNOM3:def_10; percases ( b . n = 0 or b . n <> 0 ) ; supposeA120: b . n = 0 ; ::_thesis: p3 . b = 0. R then p2 = 1_ (Polynom-Ring (n,R)) by A119, POLYNOM3:30 .= 1_ (n,R) by POLYNOM1:31 ; hence p3 . b = 0. R by A113, A116, A118, A120, POLYNOM1:25; ::_thesis: verum end; suppose b . n <> 0 ; ::_thesis: p3 . b = 0. R then p2 = 0. (Polynom-Ring (n,R)) by A119, POLYNOM3:30 .= 0_ (n,R) by POLYNOM1:def_10 ; hence p3 . b = 0. R by A113, A118, POLYNOM1:22; ::_thesis: verum end; end; end; b <> (EmptyBag n) bag_extend 0 by A116, Def1; then b <> EmptyBag (n + 1) by Th6; hence p3 . b = (1_ ((n + 1),R)) . b by A117, POLYNOM1:25 .= p19 . b by POLYNOM1:31 ; ::_thesis: verum end; end; end; hence p3 . x = p19 . x ; ::_thesis: verum end; then p19 = p3 by FUNCT_2:12; hence upm (n,R) is unity-preserving by GROUP_1:def_13; ::_thesis: verum end; cluster upm (n,R) -> one-to-one ; coherence upm (n,R) is one-to-one proof set P = upm (n,R); set PNR = Polynom-Ring (n,R); set PRPNR = Polynom-Ring (Polynom-Ring (n,R)); now__::_thesis:_for_x9,_y9_being_Element_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_st_(upm_(n,R))_._x9_=_(upm_(n,R))_._y9_holds_ x9_=_y9 let x9, y9 be Element of (Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ( (upm (n,R)) . x9 = (upm (n,R)) . y9 implies x9 = y9 ) reconsider x = x9, y = y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; reconsider Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def_10; assume A121: (upm (n,R)) . x9 = (upm (n,R)) . y9 ; ::_thesis: x9 = y9 now__::_thesis:_for_bn9_being_set_st_bn9_in_NAT_holds_ x_._bn9_=_y_._bn9 let bn9 be set ; ::_thesis: ( bn9 in NAT implies x . bn9 = y . bn9 ) assume bn9 in NAT ; ::_thesis: x . bn9 = y . bn9 then reconsider bn = bn9 as Element of NAT ; reconsider xbn = x . bn, ybn = y . bn as Polynomial of n,R by POLYNOM1:def_10; now__::_thesis:_for_b9_being_set_st_b9_in_Bags_n_holds_ xbn_._b9_=_ybn_._b9 let b9 be set ; ::_thesis: ( b9 in Bags n implies xbn . b9 = ybn . b9 ) assume b9 in Bags n ; ::_thesis: xbn . b9 = ybn . b9 then reconsider b = b9 as bag of n ; set bn1 = b bag_extend bn; A122: ( (b bag_extend bn) | n = b & (b bag_extend bn) . n = bn ) by Def1; then xbn . b = Py . (b bag_extend bn) by A121, Def6 .= ybn . b by A122, Def6 ; hence xbn . b9 = ybn . b9 ; ::_thesis: verum end; hence x . bn9 = y . bn9 by FUNCT_2:12; ::_thesis: verum end; hence x9 = y9 by FUNCT_2:12; ::_thesis: verum end; hence upm (n,R) is one-to-one by WAYBEL_1:def_1; ::_thesis: verum end; 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 & 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 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) proof set CR = the carrier of R; set PNR = Polynom-Ring (n,R); set PN1R = Polynom-Ring ((n + 1),R); set PRPNR = Polynom-Ring (Polynom-Ring (n,R)); set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R))); set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); set CPNR = the carrier of (Polynom-Ring (n,R)); defpred S1[ Element of the carrier of (Polynom-Ring ((n + 1),R)), Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R)))] means 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 p1 = $1 & p3 = $2 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i); A1: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_((n_+_1),R))_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_st_S1[x,y] let x be Element of the carrier of (Polynom-Ring ((n + 1),R)); ::_thesis: ex y being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) st S1[x,y] reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def_10; defpred S2[ Element of NAT , Element of the carrier of (Polynom-Ring (n,R))] means for p2 being Polynomial of n,R for b being bag of n st p2 = $2 holds p2 . b = p1 . (b bag_extend $1); A2: now__::_thesis:_for_i_being_Element_of_NAT_ex_p29_being_Element_of_the_carrier_of_(Polynom-Ring_(n,R))_st_S2[i,p29] let i be Element of NAT ; ::_thesis: ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S2[i,p29] deffunc H1( Element of Bags n) -> Element of the carrier of R = p1 . ($1 bag_extend i); consider p2 being Function of (Bags n), the carrier of R such that A3: for b being Element of Bags n holds p2 . b = H1(b) from FUNCT_2:sch_4(); reconsider p2 = p2 as Function of (Bags n),R ; reconsider p2 = p2 as Series of n,R ; now__::_thesis:_Support_p2_is_finite percases ( Support p1 = {} or Support p2 = {} or ( Support p1 <> {} & Support p2 <> {} ) ) ; supposeA4: Support p1 = {} ; ::_thesis: Support p2 is finite now__::_thesis:_(_Support_p2_<>_{}_implies_Support_p1_<>_{}_) assume Support p2 <> {} ; ::_thesis: Support p1 <> {} then consider b being set such that A5: b in Support p2 by XBOOLE_0:def_1; reconsider b = b as Element of Bags n by A5; p2 . b <> 0. R by A5, POLYNOM1:def_3; then p1 . (b bag_extend i) <> 0. R by A3; hence Support p1 <> {} by POLYNOM1:def_3; ::_thesis: verum end; hence Support p2 is finite by A4; ::_thesis: verum end; suppose Support p2 = {} ; ::_thesis: Support p2 is finite hence Support p2 is finite ; ::_thesis: verum end; supposeA6: ( Support p1 <> {} & Support p2 <> {} ) ; ::_thesis: Support p2 is finite then reconsider Supportp2 = Support p2 as non empty Subset of (Bags n) ; reconsider Supportp1 = Support p1 as non empty Subset of (Bags (n + 1)) by A6; defpred S3[ Element of Supportp2, set ] means $2 = $1 bag_extend i; A7: now__::_thesis:_for_x_being_Element_of_Supportp2_ex_y_being_Element_of_Supportp1_st_S3[x,y] let x be Element of Supportp2; ::_thesis: ex y being Element of Supportp1 st S3[x,y] ( x is Element of Bags n & p2 . x <> 0. R ) by POLYNOM1:def_3; then p1 . (x bag_extend i) <> 0. R by A3; then x bag_extend i in Support p1 by POLYNOM1:def_3; hence ex y being Element of Supportp1 st S3[x,y] ; ::_thesis: verum end; consider f being Function of Supportp2,Supportp1 such that A8: for x being Element of Supportp2 holds S3[x,f . x] from FUNCT_2:sch_3(A7); A9: dom f = Supportp2 by FUNCT_2:def_1; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A10: x1 in dom f and A11: x2 in dom f and A12: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider x19 = x1, x29 = x2 as Element of Bags n by A9, A10, A11; A13: x19 bag_extend i = f . x1 by A8, A10 .= x29 bag_extend i by A8, A11, A12 ; x19 = (x19 bag_extend i) | n by Def1 .= x29 by A13, Def1 ; hence x1 = x2 ; ::_thesis: verum end; then A14: f is one-to-one by FUNCT_1:def_4; rng f c= Supportp1 ; then card Supportp2 c= card Supportp1 by A9, A14, CARD_1:10; hence Support p2 is finite ; ::_thesis: verum end; end; end; then p2 is finite-Support by POLYNOM1:def_4; then reconsider p29 = p2 as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10; take p29 = p29; ::_thesis: S2[i,p29] now__::_thesis:_for_p299_being_Polynomial_of_n,R for_b_being_bag_of_n_st_p299_=_p29_holds_ p299_._b_=_p1_._(b_bag_extend_i) let p299 be Polynomial of n,R; ::_thesis: for b being bag of n st p299 = p29 holds p299 . b = p1 . (b bag_extend i) let b be bag of n; ::_thesis: ( p299 = p29 implies p299 . b = p1 . (b bag_extend i) ) A15: b is Element of Bags n by PRE_POLY:def_12; assume p299 = p29 ; ::_thesis: p299 . b = p1 . (b bag_extend i) hence p299 . b = p1 . (b bag_extend i) by A3, A15; ::_thesis: verum end; hence S2[i,p29] ; ::_thesis: verum end; consider p3 being Function of NAT, the carrier of (Polynom-Ring (n,R)) such that A16: for x being Element of NAT holds S2[x,p3 . x] from FUNCT_2:sch_3(A2); reconsider p3 = p3 as sequence of (Polynom-Ring (n,R)) ; now__::_thesis:_p3_is_finite-Support percases ( Support p1 = {} or Support p1 <> {} ) ; supposeA17: Support p1 = {} ; ::_thesis: p3 is finite-Support now__::_thesis:_for_i_being_Nat_st_i_>=_0_holds_ p3_._i_=_0._(Polynom-Ring_(n,R)) let i be Nat; ::_thesis: ( i >= 0 implies p3 . i = 0. (Polynom-Ring (n,R)) ) assume i >= 0 ; ::_thesis: p3 . i = 0. (Polynom-Ring (n,R)) reconsider i1 = i as Element of NAT by ORDINAL1:def_12; reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def_10; A18: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_ p2_._x_=_((Bags_n)_-->_(0._R))_._x let x be set ; ::_thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x ) assume x in Bags n ; ::_thesis: p2 . x = ((Bags n) --> (0. R)) . x then reconsider x9 = x as Element of Bags n ; p1 . (x9 bag_extend i) = 0. R by A17, POLYNOM1:def_3; then p2 . x9 = 0. R by A16; hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:7; ::_thesis: verum end; ( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCT_2:def_1; then p2 = (Bags n) --> (0. R) by A18, FUNCT_1:2; hence p3 . i = 0_ (n,R) by POLYNOM1:def_7 .= 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10 ; ::_thesis: verum end; hence p3 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum end; suppose Support p1 <> {} ; ::_thesis: p3 is finite-Support then reconsider Supportp1 = Support p1 as non empty finite Subset of (Bags (n + 1)) ; deffunc H1( Element of Bags (n + 1)) -> Element of NAT = $1 . n; consider f being Function of (Bags (n + 1)),NAT such that A19: for x being Element of Bags (n + 1) holds f . x = H1(x) from FUNCT_2:sch_4(); reconsider j = max (f .: Supportp1) as Element of NAT by ORDINAL1:def_12; now__::_thesis:_for_i_being_Nat_st_i_>=_j_+_1_holds_ p3_._i_=_0._(Polynom-Ring_(n,R)) let i be Nat; ::_thesis: ( i >= j + 1 implies p3 . i = 0. (Polynom-Ring (n,R)) ) reconsider i1 = i as Element of NAT by ORDINAL1:def_12; reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def_10; assume A20: i >= j + 1 ; ::_thesis: p3 . i = 0. (Polynom-Ring (n,R)) A21: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_ p2_._x_=_((Bags_n)_-->_(0._R))_._x let x be set ; ::_thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x ) assume x in Bags n ; ::_thesis: p2 . x = ((Bags n) --> (0. R)) . x then reconsider x9 = x as Element of Bags n ; i > j by A20, NAT_1:13; then A22: not i in f .: Supportp1 by XXREAL_2:def_8; f . (x9 bag_extend i) = (x9 bag_extend i) . n by A19 .= i by Def1 ; then not x9 bag_extend i in Supportp1 by A22, FUNCT_2:35; then p1 . (x9 bag_extend i) = 0. R by POLYNOM1:def_3; then p2 . x9 = 0. R by A16; hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:7; ::_thesis: verum end; ( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCT_2:def_1; then p2 = (Bags n) --> (0. R) by A21, FUNCT_1:2; hence p3 . i = 0_ (n,R) by POLYNOM1:def_7 .= 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10 ; ::_thesis: verum end; hence p3 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum end; end; end; then reconsider y = p3 as Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def_10; take y = y; ::_thesis: S1[x,y] thus S1[x,y] by A16; ::_thesis: verum end; consider P being Function of the carrier of (Polynom-Ring ((n + 1),R)), the carrier of (Polynom-Ring (Polynom-Ring (n,R))) such that A23: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) holds S1[x,P . x] from FUNCT_2:sch_3(A1); reconsider P = P as Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) ; take P ; ::_thesis: 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 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) now__::_thesis:_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_=_P_._p1_&_p2_=_p3_._i_holds_ p2_._b_=_p1_._(b_bag_extend_i) let p1 be Polynomial of (n + 1),R; ::_thesis: 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 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (Polynom-Ring (n,R)) for i being Element of NAT for b being bag of n st p3 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) let p3 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for i being Element of NAT for b being bag of n st p3 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) let i be Element of NAT ; ::_thesis: for b being bag of n st p3 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) let b be bag of n; ::_thesis: ( p3 = P . p1 & p2 = p3 . i implies p2 . b = p1 . (b bag_extend i) ) A24: p1 in the carrier of (Polynom-Ring ((n + 1),R)) by POLYNOM1:def_10; assume ( p3 = P . p1 & p2 = p3 . i ) ; ::_thesis: p2 . b = p1 . (b bag_extend i) hence p2 . b = p1 . (b bag_extend i) by A23, A24; ::_thesis: verum end; hence 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 = P . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) ; ::_thesis: verum end; 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 & 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 = b2 . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) ) holds b1 = b2 proof set PNR = Polynom-Ring (n,R); set PN1R = Polynom-Ring ((n + 1),R); set PRPNR = Polynom-Ring (Polynom-Ring (n,R)); set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); let A, B be Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ( ( 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 = A . 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 . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) ) implies A = B ) assume A25: 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 = A . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) ; ::_thesis: ( ex p1 being Polynomial of (n + 1),R ex p2 being Polynomial of n,R ex p3 being Polynomial of (Polynom-Ring (n,R)) ex i being Element of NAT ex b being bag of n st ( p3 = B . p1 & p2 = p3 . i & not p2 . b = p1 . (b bag_extend i) ) or A = B ) assume A26: 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 . p1 & p2 = p3 . i holds p2 . b = p1 . (b bag_extend i) ; ::_thesis: A = B now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Polynom-Ring_((n_+_1),R))_holds_ A_._x_=_B_._x let x be set ; ::_thesis: ( x in the carrier of (Polynom-Ring ((n + 1),R)) implies A . x = B . x ) assume A27: x in the carrier of (Polynom-Ring ((n + 1),R)) ; ::_thesis: A . x = B . x then reconsider x99 = x as Element of the carrier of (Polynom-Ring ((n + 1),R)) ; reconsider x9 = x as Polynomial of (n + 1),R by A27, POLYNOM1:def_10; reconsider Ax = A . x99, Bx = B . x99 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_ Ax_._i_=_Bx_._i let i be set ; ::_thesis: ( i in NAT implies Ax . i = Bx . i ) assume i in NAT ; ::_thesis: Ax . i = Bx . i then reconsider i9 = i as Element of NAT ; reconsider Axi = Ax . i9, Bxi = Bx . i9 as Polynomial of n,R by POLYNOM1:def_10; now__::_thesis:_for_b_being_set_st_b_in_Bags_n_holds_ Axi_._b_=_Bxi_._b let b be set ; ::_thesis: ( b in Bags n implies Axi . b = Bxi . b ) assume b in Bags n ; ::_thesis: Axi . b = Bxi . b then reconsider b9 = b as bag of n ; thus Axi . b = x9 . (b9 bag_extend i9) by A25 .= Bxi . b by A26 ; ::_thesis: verum end; hence Ax . i = Bx . i by FUNCT_2:12; ::_thesis: verum end; hence A . x = B . x by FUNCT_2:12; ::_thesis: verum end; hence A = B by FUNCT_2:12; ::_thesis: verum end; 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 & 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 proof let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: 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 let n be Element of NAT ; ::_thesis: for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p let p be Element of (Polynom-Ring ((n + 1),R)); ::_thesis: (upm (n,R)) . ((mpu (n,R)) . p) = p set PNR = Polynom-Ring (n,R); reconsider p9 = p as Polynomial of (n + 1),R by POLYNOM1:def_10; reconsider upmmpup = (upm (n,R)) . ((mpu (n,R)) . p) as Polynomial of (n + 1),R by POLYNOM1:def_10; reconsider mpup = (mpu (n,R)) . p as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10; now__::_thesis:_for_b9_being_set_st_b9_in_Bags_(n_+_1)_holds_ upmmpup_._b9_=_p9_._b9 let b9 be set ; ::_thesis: ( b9 in Bags (n + 1) implies upmmpup . b9 = p9 . b9 ) assume b9 in Bags (n + 1) ; ::_thesis: upmmpup . b9 = p9 . b9 then reconsider b = b9 as Element of Bags (n + 1) ; reconsider mpupbn = mpup . (b . n) as Polynomial of n,R by POLYNOM1:def_10; n < n + 1 by NAT_1:13; then reconsider bn = b | n as bag of n by Th3; A1: b = bn bag_extend (b . n) by Def1; thus upmmpup . b9 = mpupbn . bn by Def6 .= p9 . b9 by A1, Def7 ; ::_thesis: verum end; hence (upm (n,R)) . ((mpu (n,R)) . p) = p by FUNCT_2:12; ::_thesis: verum end; 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 proof let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: 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 let n be Element of NAT ; ::_thesis: ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism set PN1R = Polynom-Ring ((n + 1),R); set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R))); set CPN1R = the carrier of (Polynom-Ring ((n + 1),R)); set P = upm (n,R); A1: upm (n,R) is RingHomomorphism by QUOFIELD:def_18; then A2: upm (n,R) is RingMonomorphism by QUOFIELD:def_20; now__::_thesis:_for_p_being_set_st_p_in_the_carrier_of_(Polynom-Ring_((n_+_1),R))_holds_ p_in_rng_(upm_(n,R)) let p be set ; ::_thesis: ( p in the carrier of (Polynom-Ring ((n + 1),R)) implies p in rng (upm (n,R)) ) assume p in the carrier of (Polynom-Ring ((n + 1),R)) ; ::_thesis: p in rng (upm (n,R)) then reconsider p9 = p as Element of the carrier of (Polynom-Ring ((n + 1),R)) ; ( dom (upm (n,R)) = the carrier of (Polynom-Ring (Polynom-Ring (n,R))) & (upm (n,R)) . ((mpu (n,R)) . p9) = p9 ) by Th30, FUNCT_2:def_1; hence p in rng (upm (n,R)) by FUNCT_1:def_3; ::_thesis: verum end; then the carrier of (Polynom-Ring ((n + 1),R)) c= rng (upm (n,R)) by TARSKI:def_3; then rng (upm (n,R)) = the carrier of (Polynom-Ring ((n + 1),R)) by XBOOLE_0:def_10; then upm (n,R) is RingEpimorphism by A1, QUOFIELD:def_19; then upm (n,R) is RingIsomorphism by A2, QUOFIELD:def_21; hence ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism ; ::_thesis: verum end; 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 proof set cR = the carrier of R; set PR = Polynom-Ring R; set cPR = the carrier of (Polynom-Ring R); now__::_thesis:_Polynom-Ring_R_is_Noetherian 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_26; 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__::_thesis:_for_n_being_Element_of_NAT_ for_x_being_Subset_of_the_carrier_of_(Polynom-Ring_R)_ex_y_being_Subset_of_the_carrier_of_(Polynom-Ring_R)_st_S1[n,x,y] 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] percases ( 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; supposeA3: 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 x9 = x as non empty Subset of the carrier of (Polynom-Ring R) ; set B = I \ (x9 -Ideal); now__::_thesis:_not_I_\_(x9_-Ideal)_=_{} assume I \ (x9 -Ideal) = {} ; ::_thesis: contradiction then A4: I c= x9 -Ideal by XBOOLE_1:37; x9 -Ideal c= I -Ideal by A3, IDEAL_1:57; then x9 -Ideal c= I by IDEAL_1:44; hence contradiction by A1, A3, A4, XBOOLE_0:def_10; ::_thesis: verum end; then reconsider B = I \ (x9 -Ideal) as non empty Subset of the carrier of (Polynom-Ring R) ; consider r being set such that A5: r in minlen B by XBOOLE_0:def_1; minlen B c= the carrier of (Polynom-Ring R) by XBOOLE_1:1; then reconsider r = r as Element of the carrier of (Polynom-Ring R) by A5; S1[n,x,x9 \/ {r}] by A5; 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 A6: ( 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[ 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 ); defpred S3[ Element of NAT ] means F . R is non empty finite Subset of I; A7: now__::_thesis:_for_n_being_Element_of_NAT_st_S3[n]_holds_ S3[n_+_1] let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume S3[n] ; ::_thesis: S3[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 A = Fn and A8: B = I \ (A -Ideal) and A9: ex r being Element of the carrier of (Polynom-Ring R) st ( r in minlen B & F . (n + 1) = Fn \/ {r} ) by A6; consider r being Element of the carrier of (Polynom-Ring R) such that A10: r in minlen B and A11: F . (n + 1) = Fn \/ {r} by A9; r in I by A8, A10, XBOOLE_0:def_5; then {r} c= I by ZFMISC_1:31; hence S3[n + 1] by A11, XBOOLE_1:8; ::_thesis: verum end; 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 A6, TARSKI:def_1; hence x in I by IDEAL_1:2; ::_thesis: verum end; then A12: S3[ 0 ] by A6; A13: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A12, A7); A14: now__::_thesis:_for_x_being_Element_of_NAT_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_R)_st_S2[x,y] let x be Element of NAT ; ::_thesis: ex y being Element of the carrier of (Polynom-Ring R) st S2[x,y] ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st ( A = F . x & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st ( r in minlen B & F . (x + 1) = (F . x) \/ {r} ) ) by A6, A13; hence ex y being Element of the carrier of (Polynom-Ring R) st S2[x,y] ; ::_thesis: verum end; consider f being Function of NAT, the carrier of (Polynom-Ring R) such that A15: for x being Element of NAT holds S2[x,f . x] from FUNCT_2:sch_3(A14); A16: 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 ) defpred S4[ Element of NAT ] means F . i c= F . (i + R); assume i <= j ; ::_thesis: F . i c= F . j then consider m being Nat such that A17: j = i + m by NAT_1:10; A18: for m being Element of NAT st S4[m] holds S4[m + 1] proof let m be Element of NAT ; ::_thesis: ( S4[m] implies S4[m + 1] ) ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st ( A = F . (i + m) & B = I \ (A -Ideal) & 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 A6, A13; then A19: F . (i + m) c= F . ((i + m) + 1) by XBOOLE_1:7; assume F . i c= F . (i + m) ; ::_thesis: S4[m + 1] hence S4[m + 1] by A19, XBOOLE_1:1; ::_thesis: verum end; A20: S4[ 0 ] ; A21: for m being Element of NAT holds S4[m] from NAT_1:sch_1(A20, A18); m in NAT by ORDINAL1:def_12; hence F . i c= F . j by A17, A21; ::_thesis: verum end; A22: 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 A23: A = F . n and A24: B = I \ (A -Ideal) and n = i and F . (n + 1) = (F . n) \/ {(f . i)} and A25: f . i in minlen B by A15; F . n c= A -Ideal by A23, IDEAL_1:def_14; then A26: not f . i in F . n by A24, A25, XBOOLE_0:def_5; ( F . 0 c= F . n & 0. (Polynom-Ring R) in F . 0 ) by A6, A16, TARSKI:def_1; hence f . i <> 0. (Polynom-Ring R) by A26; ::_thesis: verum end; A27: now__::_thesis:_for_i_being_Element_of_NAT_ for_fi_being_Polynomial_of_R_st_fi_=_f_._i_holds_ (len_fi)_-_1_>=_0 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 A22; then fi <> 0_. R by POLYNOM3:def_10; then len fi <> 0 by POLYNOM4:5; then len fi >= 0 + 1 by NAT_1:13; hence (len fi) - 1 >= 0 by XREAL_1:19; ::_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) ); A28: now__::_thesis:_for_x_being_Element_of_NAT_ex_y_being_Element_of_the_carrier_of_R_st_S4[x,y] 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_10; 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 A29: for x being Element of NAT holds S4[x,a . x] from FUNCT_2:sch_3(A28); 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:96; then consider m being Element of NAT such that A30: a . (m + 1) in (rng (a | (m + 1))) -Ideal by IDEAL_1:97; reconsider fm1 = f . (m + 1) as Polynomial of R by POLYNOM3:def_10; 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) ) ); A31: 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 = m + 1 & F . (n + 1) = (F . n) \/ {(f . (m + 1))} & f . (m + 1) in minlen B ) by A15; A32: 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 that A33: i <= j and A34: fi = f . i and A35: fj = f . j ; ::_thesis: len fi <= len fj consider k being Nat such that A36: j = i + k by A33, NAT_1:10; defpred S6[ Element of NAT ] means for fk being Polynomial of R st fk = f . (i + R) holds len fi <= len fk; A37: now__::_thesis:_for_k_being_Element_of_NAT_st_S6[k]_holds_ S6[k_+_1] let k be Element of NAT ; ::_thesis: ( S6[k] implies S6[k + 1] ) assume A38: S6[k] ; ::_thesis: S6[k + 1] now__::_thesis:_for_fk1_being_Polynomial_of_R_st_fk1_=_f_._(i_+_(k_+_1))_holds_ len_fi_<=_len_fk1 reconsider fk = f . (i + k) as Polynomial of R by POLYNOM3:def_10; let fk1 be Polynomial of R; ::_thesis: ( fk1 = f . (i + (k + 1)) implies len fi <= len fk1 ) A39: len fi <= len fk by A38; 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 and A41: B = I \ (A -Ideal) and A42: n = i + k and F . (n + 1) = (F . n) \/ {(f . (i + k))} and A43: f . (i + k) in minlen B by A15; consider n9 being Element of NAT , A9, B9 being non empty Subset of the carrier of (Polynom-Ring R) such that A44: A9 = F . n9 and A45: B9 = I \ (A9 -Ideal) and A46: n9 = i + (k + 1) and F . (n9 + 1) = (F . n9) \/ {(f . (i + (k + 1)))} and A47: f . (i + (k + 1)) in minlen B9 by A15; A48: f . (i + (k + 1)) in I by A45, A47, XBOOLE_0:def_5; i + (k + 1) = (i + k) + 1 ; then i + k < i + (k + 1) by NAT_1:13; then A -Ideal c= A9 -Ideal by A16, A40, A42, A44, A46, IDEAL_1:57; then not f . (i + (k + 1)) in A -Ideal by A45, A47, XBOOLE_0:def_5; then A49: f . (i + (k + 1)) in B by A41, A48, XBOOLE_0:def_5; assume fk1 = f . (i + (k + 1)) ; ::_thesis: len fi <= len fk1 then len fk <= len fk1 by A43, A49, Th17; hence len fi <= len fk1 by A39, XXREAL_0:2; ::_thesis: verum end; hence S6[k + 1] ; ::_thesis: verum end; A50: S6[ 0 ] by A34; A51: for k being Element of NAT holds S6[k] from NAT_1:sch_1(A50, A37); k in NAT by ORDINAL1:def_12; hence len fi <= len fj by A35, A36, A51; ::_thesis: verum end; A52: 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] ) percases ( 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, b9, w being Element of the carrier of R such that A53: e = (u * b9) * w and A54: b9 in rng (a | (Segm (m + 1))) ; consider n being set such that A55: n in dom (a | (Segm (m + 1))) and A56: b9 = (a | (Segm (m + 1))) . n by A54, FUNCT_1:def_3; set c9 = w; set a9 = u; set z9 = monomial (w,0); A57: (len fm1) -' 1 = ((len fm1) -' 1) + 0 ; reconsider n = n as Element of NAT by A55; set y = f . n; reconsider y9 = f . n as Polynomial of R by POLYNOM3:def_10; set x9 = monomial (u,((len fm1) -' (len y9))); dom (a | (Segm (m + 1))) = (dom a) /\ (Segm (m + 1)) by RELAT_1:61 .= NAT /\ (Segm (m + 1)) by FUNCT_2:def_1 .= Segm (m + 1) by XBOOLE_1:28 ; then A58: n < m + 1 by A55, NAT_1:44; then len y9 <= len fm1 by A32; then (len y9) - (len y9) <= (len fm1) - (len y9) by XREAL_1:9; then A59: (len fm1) -' (len y9) = (len fm1) - (len y9) by XREAL_0:def_2; then len (monomial (u,((len fm1) -' (len y9)))) <= ((len fm1) - (len y9)) + 1 by Th18; then A60: (len (monomial (u,((len fm1) -' (len y9))))) + ((len y9) - 1) <= ((len fm1) - ((len y9) - 1)) + ((len y9) - 1) by XREAL_1:6; A61: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) -' 1 by Th21; A62: (len y9) - 1 >= 0 by A27; then 0 + 0 <= ((len y9) - 1) + (len (monomial (u,((len fm1) -' (len y9))))) ; then len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) - 1 by A61, XREAL_0:def_2; then A63: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= len fm1 by A60, XXREAL_0:2; (len fm1) - 1 >= 0 by A27; then A64: (len fm1) -' 1 = ((len fm1) - (len y9)) + ((len y9) - 1) by XREAL_0:def_2 .= ((len y9) -' 1) + ((len fm1) -' (len y9)) by A59, A62, XREAL_0:def_2 ; reconsider x = monomial (u,((len fm1) -' (len y9))), z = monomial (w,0) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10; set p = (x * (f . n)) * z; A65: x * (f . n) = (monomial (u,((len fm1) -' (len y9)))) *' y9 by POLYNOM3:def_10; then A66: (x * (f . n)) * z = ((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0)) by POLYNOM3:def_10; reconsider p = (x * (f . n)) * z as Polynomial of R by POLYNOM3:def_10; A67: ex n9 being Element of NAT ex A being Polynomial of R st ( n9 = n & A = f . n9 & a . n = A . ((len A) -' 1) ) by A29; b9 = a . n by A55, A56, FUNCT_1:47; then ((monomial (u,((len fm1) -' (len y9)))) *' y9) . ((len fm1) -' 1) = u * b9 by A67, A64, Th19; then A68: (u * b9) * w = p . ((len fm1) -' 1) by A66, A57, Th20; ex n9 being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st ( A = F . n9 & B = I \ (A -Ideal) & n9 = n & F . (n9 + 1) = (F . n9) \/ {(f . n)} & f . n in minlen B ) by A15; then {(f . n)} c= F . (n + 1) by XBOOLE_1:7; then A69: f . n in F . (n + 1) by ZFMISC_1:31; len (monomial (w,0)) <= 0 + 1 by Th18; then (len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0))) <= (len fm1) + 1 by A63, XREAL_1:7; then A70: ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 <= ((len fm1) + 1) -' 1 by NAT_D:42; len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 by Th21; then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) -' 1 by A70, XXREAL_0:2; then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) - 1 by XREAL_0:def_2; then A71: len p <= (len fm1) + 0 by A65, POLYNOM3:def_10; n + 1 <= m + 1 by A58, NAT_1:13; then F . (n + 1) c= F . (m + 1) by A16; hence ex d being set st ( d in the carrier of (Polynom-Ring R) & S5[e,d] ) by A53, A68, A71, A69; ::_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 d being set st ( d in the carrier of (Polynom-Ring R) & S5[e,d] ) ; ::_thesis: verum end; end; end; consider LCT being Function of the carrier of R, the carrier of (Polynom-Ring R) such that A72: for e being set st e in the carrier of R holds S5[e,LCT . e] from FUNCT_2:sch_1(A52); 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))); consider lc being LinearCombination of rng (a | (Segm (m + 1))) such that A73: a . (m + 1) = Sum lc by A30, IDEAL_1:60; A74: 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 ) set LC = LCT * lc; dom LCT = the carrier of R by FUNCT_2:def_1; then rng lc c= dom LCT ; then A75: dom lc = dom (LCT * lc) by RELAT_1:27; then A76: len lc = len (LCT * lc) by FINSEQ_3:29; LCT * lc is LinearCombination of FM1 proof let i be set ; :: according to IDEAL_1:def_8 ::_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 A77: 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 A78: lc /. i = (u * a) * v by A75, A77, IDEAL_1:def_8; A79: lc /. i = lc . i by A75, A77, PARTFUN1:def_6; consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that A80: ( LCT . (lc /. i) = p & p = (x * y) * z ) and (u * a) * v = p . ((len fm1) -' 1) and len p <= len fm1 and A81: y in F . (m + 1) by A72, A78; reconsider y = y as Element of FM1 by A81; reconsider x = x, z = z as Element of (Polynom-Ring R) ; (LCT * lc) /. i = (LCT * lc) . i by A77, PARTFUN1:def_6 .= (x * y) * z by A75, A77, A79, A80, FUNCT_1:13 ; 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 A76; ::_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 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 ) 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 ); A82: ex n being Element of NAT st n = len lc ; A83: 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 A84: 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 A85: 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 ) percases ( 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 A84; ::_thesis: verum end; supposeA86: 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 A87: len lc = k + 1 by A85, 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 percases ( k = 0 or k > 0 ) ; supposeA88: 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 A87, FINSEQ_1:2, FINSEQ_1:def_3; then A89: 1 in dom lc by TARSKI:def_1; then consider u, w being Element of R, v being Element of rng (a | (Segm (m + 1))) such that A90: lc /. 1 = (u * v) * w by IDEAL_1:def_8; A91: lc . 1 = lc /. 1 by A89, PARTFUN1:def_6; then consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that A92: LCT . (lc . 1) = p and p = (x * y) * z and A93: (u * v) * w = p . ((len fm1) -' 1) and A94: len p <= len fm1 and y in F . (m + 1) by A72, A90; A95: lc = <*(lc . 1)*> by A87, A88, FINSEQ_1:40; then A96: Sum lc = p . ((len fm1) -' 1) by A90, A91, A93, RLVECT_1:44; consider LC being LinearCombination of FM1 such that A97: LC = LCT * lc and len LC = len lc by A74; LC = <*(LCT . ((u * v) * w))*> by A95, A90, A91, A97, FINSEQ_2:35; then Sum LC = p by A90, A91, A92, RLVECT_1:44; 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 A94, A97, A96; ::_thesis: verum end; supposeA98: 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 ) consider LC being LinearCombination of FM1 such that A99: LC = LCT * lc and len LC = len lc by A74; not lc is empty by A86; then consider p being LinearCombination of rng (a | (Segm (m + 1))), e being Element of the carrier of R such that A100: lc = p ^ <*e*> and A101: <*e*> is LinearCombination of rng (a | (Segm (m + 1))) by IDEAL_1:32; len <*e*> = 0 + 1 by FINSEQ_1:39; then len <*e*> <= k by A98, NAT_1:13; then consider LCe being LinearCombination of FM1, sLCe being Polynomial of R such that A102: LCe = LCT * <*e*> and A103: sLCe = Sum LCe and A104: sLCe . ((len fm1) -' 1) = Sum <*e*> and A105: len sLCe <= len fm1 by A84, A101; len lc = (len p) + (len <*e*>) by A100, FINSEQ_1:22 .= (len p) + 1 by FINSEQ_1:39 ; then consider LCp being LinearCombination of FM1, sLCp being Polynomial of R such that A106: LCp = LCT * p and A107: sLCp = Sum LCp and A108: sLCp . ((len fm1) -' 1) = Sum p and A109: len sLCp <= len fm1 by A84, A87; set sLC = sLCp + sLCe; A110: Sum lc = (Sum p) + e by A100, FVSUM_1:71 .= (sLCp . ((len fm1) -' 1)) + (sLCe . ((len fm1) -' 1)) by A108, A104, RLVECT_1:44 .= (sLCp + sLCe) . ((len fm1) -' 1) by NORMSP_1:def_2 ; A111: now__::_thesis:_len_(sLCp_+_sLCe)_<=_len_fm1 percases ( 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:6; hence len (sLCp + sLCe) <= len fm1 by A105, 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:6; hence len (sLCp + sLCe) <= len fm1 by A109, XXREAL_0:2; ::_thesis: verum end; end; end; dom LCT = the carrier of R by FUNCT_2:def_1; then (rng p) \/ (rng <*e*>) c= dom LCT ; then ex LCTp, LCTe being FinSequence st ( LCTp = LCT * p & LCTe = LCT * <*e*> & LCT * (p ^ <*e*>) = LCTp ^ LCTe ) by Th1; then Sum LC = (Sum LCp) + (Sum LCe) by A100, A106, A102, A99, RLVECT_1:41 .= sLCp + sLCe by A107, A103, POLYNOM3:def_10 ; 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, A110, A111; ::_thesis: verum end; end; end; end; end; end; end; A112: 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 A113: 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 A114: lc = <*> the carrier of R ; consider LC being LinearCombination of FM1 such that A115: LC = LCT * lc and A116: len lc = len LC by A74; 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 A115; ::_thesis: ( p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 ) LC = <*> the carrier of (Polynom-Ring R) by A113, A116; then Sum LC = 0. (Polynom-Ring R) by RLVECT_1:43 .= p by POLYNOM3:def_10 ; 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:7 .= Sum lc by A114, RLVECT_1:43 ; ::_thesis: len p <= len fm1 thus len p <= len fm1 by POLYNOM4:3; ::_thesis: verum end; for k being Element of NAT holds S6[k] from NAT_1:sch_1(A112, A83); 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 A82; ::_thesis: verum end; then consider LC being LinearCombination of FM1, sLC being Polynomial of R such that LC = LCT * lc and A117: sLC = Sum LC and A118: sLC . ((len fm1) -' 1) = Sum lc and A119: len sLC <= len fm1 ; A120: sLC in FM1 -Ideal by A117, IDEAL_1:60; set f9 = fm1 - sLC; A121: now__::_thesis:_not_len_(fm1_-_sLC)_=_len_fm1 ex n being Element of NAT ex A being Polynomial of R st ( n = m + 1 & A = f . n & a . (m + 1) = A . ((len A) -' 1) ) by A29; then A122: (fm1 - sLC) . ((len fm1) -' 1) = (fm1 . ((len fm1) -' 1)) - (fm1 . ((len fm1) -' 1)) by A73, A118, POLYNOM3:27 .= 0. R by RLVECT_1:15 ; (len fm1) - 1 >= 0 by A27; then A123: ((len fm1) -' 1) + 1 = ((len fm1) - 1) + 1 by XREAL_0:def_2 .= len fm1 ; assume len (fm1 - sLC) = len fm1 ; ::_thesis: contradiction hence contradiction by A123, A122, ALGSEQ_1:10; ::_thesis: verum end; A124: (fm1 - sLC) + sLC = fm1 + (sLC + (- sLC)) by POLYNOM3:26 .= fm1 + (sLC - sLC) .= fm1 + (0_. R) by POLYNOM3:29 .= fm1 by POLYNOM3:28 ; A125: now__::_thesis:_not_fm1_-_sLC_in_FM1_-Ideal reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10; assume A126: fm1 - sLC in FM1 -Ideal ; ::_thesis: contradiction reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10; f . (m + 1) = f9 + sLC by A124, POLYNOM3:def_10; then fm1 in FM1 -Ideal by A120, A126, IDEAL_1:def_1; hence contradiction by A31, XBOOLE_0:def_5; ::_thesis: verum end; len (- sLC) <= len fm1 by A119, POLYNOM4:8; then len (fm1 - sLC) <= len fm1 by POLYNOM4:6; then A127: len (fm1 - sLC) < len fm1 by A121, XXREAL_0:1; fm1 - sLC in I proof reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10; reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10; FM1 is Subset of I by A13; then FM1 -Ideal c= I -Ideal by IDEAL_1:57; then A128: FM1 -Ideal c= I by IDEAL_1:44; ( f . (m + 1) in I & f9 = (f . (m + 1)) - sLC ) by A31, Th16, XBOOLE_0:def_5; hence fm1 - sLC in I by A120, A128, IDEAL_1:15; ::_thesis: verum end; then fm1 - sLC in I \ (FM1 -Ideal) by A125, XBOOLE_0:def_5; hence contradiction by A127, A31, Th17; ::_thesis: verum end; hence Polynom-Ring R is Noetherian ; ::_thesis: verum end; 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 proof let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: ( R is Noetherian implies for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian ) assume A1: R is Noetherian ; ::_thesis: for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian defpred S1[ Element of NAT ] means Polynom-Ring ($1,R) is Noetherian ; A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] ex P being Function of (Polynom-Ring (Polynom-Ring (k,R))),(Polynom-Ring ((k + 1),R)) st P is RingIsomorphism by Th31; hence S1[k + 1] by A3, Th27; ::_thesis: verum end; ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism by Th28; then A4: S1[ 0 ] by A1, Th27; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); ::_thesis: verum end; theorem Th33: :: HILBASIS:33 for F being Field holds F is Noetherian proof let F be Field; ::_thesis: F is Noetherian let I be Ideal of F; :: according to IDEAL_1:def_26 ::_thesis: I is finitely_generated percases ( I = {(0. F)} or I = the carrier of F ) by IDEAL_1:22; supposeA1: I = {(0. F)} ; ::_thesis: I is finitely_generated reconsider s0F = {(0. F)} as non empty finite Subset of F ; {(0. F)} = s0F -Ideal by IDEAL_1:47; hence I is finitely_generated by A1; ::_thesis: verum end; supposeA2: I = the carrier of F ; ::_thesis: I is finitely_generated reconsider s1F = {(1_ F)} as non empty finite Subset of F ; the carrier of F = s1F -Ideal by IDEAL_1:51; hence I is finitely_generated by A2; ::_thesis: verum end; end; end; theorem :: HILBASIS:34 for F being Field for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian proof let F be Field; ::_thesis: for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian let n be Element of NAT ; ::_thesis: Polynom-Ring (n,F) is Noetherian F is Noetherian by Th33; hence Polynom-Ring (n,F) is Noetherian by Th32; ::_thesis: verum end; 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 proof deffunc H1( set ) -> set = $1; let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive 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; 0 in NAT ; then 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 set ; :: 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_10; ::_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 A1, IDEAL_1:96; 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 FUNCT_7:sch_2(A7, A2); A9: { H1(n) where n is Element of X : H2(n) in C } c= NAT proof let x be set ; :: 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: 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; set c = the Element of C; the Element of C in C ; then 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 ; m1 in NAT ; then 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 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 FINSEQ_2:sch_1(); 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 A18, PARTFUN1:def_6 .= (u * a) * v by A17, A18 ; ::_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_CN assume 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; assume A21: i in dom LC ; ::_thesis: 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, IDEAL_1:def_11; y in C ; then 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 by FUNCOP_1:7 ; 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, VECTSP_1:6 ; 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, VECTSP_1:6 .= 0. R by VECTSP_1:6 ; ::_thesis: verum end; dom (X --> (0. R)) = X by FUNCOP_1:13; 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, GROUP_1:def_4 ; 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 end;