:: Hilbert Basis Theorem
:: by Jonathan Backer and Piotr Rudnicki
::
:: Received November 27, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, ORDINAL4,
NAT_1, XXREAL_0, ARYTM_3, PRE_POLY, CARD_1, FUNCOP_1, PARTFUN1, SUBSET_1,
ARYTM_1, FUNCT_4, ORDINAL1, PBOOLE, FINSET_1, ORDERS_1, VECTSP_1,
ZFMISC_1, ALGSTR_0, POLYNOM2, GROUP_1, POLYNOM1, SUPINF_2, RLVECT_1,
ALGSEQ_1, LATTICES, POLYNOM3, STRUCT_0, CARD_3, CARD_FIL, QUOFIELD,
MSSUBFAM, IDEAL_1, PRELAMB, BINOP_1, FUNCT_2, HILBASIS, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PBOOLE, RELAT_1, FINSET_1,
FUNCT_1, PARTFUN1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
RELSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FUNCT_4, BINOP_1, XXREAL_2,
MCART_1, FINSEQOP, FINSEQ_2, FUNCT_7, PRE_POLY, DOMAIN_1, STRUCT_0,
ALGSTR_0, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1, NORMSP_1, POLYNOM1,
POLYNOM2, POLYNOM3, ALGSEQ_1, NAT_D, IDEAL_1, TOPS_2, GRCAT_1, WSIERP_1,
ORDERS_1, GROUP_6, QUOFIELD, RECDEF_1, MATRLIN;
constructors FINSEQOP, NAT_D, REAL_1, WSIERP_1, TOPS_2, ALGSEQ_1, GRCAT_1,
GROUP_6, MATRIX_1, TRIANG_1, QUOFIELD, POLYNOM2, POLYNOM3, IDEAL_1,
RECDEF_1, XXREAL_2, DOMAIN_1, BINARITH, RELSET_1, FUNCT_7, MATRLIN,
VFUNCT_1, FUNCT_4, MOD_4, RINGCAT1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_5,
PRE_CIRC, STRUCT_0, VECTSP_1, ALGSTR_1, WAYBEL_2, GCD_1, PRE_POLY,
POLYNOM1, POLYNOM2, POLYNOM3, IDEAL_1, VALUED_0, ALGSTR_0, XXREAL_2,
VFUNCT_1, FUNCT_2, RELSET_1, MOD_4, RINGCAT1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, IDEAL_1, VECTSP_1, GROUP_6;
equalities FUNCOP_1, POLYNOM3, STRUCT_0, ORDINAL1;
expansions TARSKI, FUNCT_2, IDEAL_1, VECTSP_1, GROUP_6;
theorems TARSKI, ZFMISC_1, RLVECT_1, FUNCT_1, FUNCT_2, POLYNOM1, NAT_1,
AXIOMS, FVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, POLYNOM3, FUNCOP_1,
ALGSEQ_1, INT_1, FUNCT_7, IDEAL_1, POLYNOM4, FUNCT_4, RELAT_1, CARD_1,
MATRLIN, CARD_3, ORDINAL1, WAYBEL_1, ORDERS_1, FINSET_1, FINSEQOP,
POLYNOM2, TOPS_2, FINSEQ_5, GROUP_1, XBOOLE_0, XBOOLE_1, RLVECT_2,
XREAL_1, XXREAL_0, NORMSP_1, PARTFUN1, XXREAL_2, NAT_D, XREAL_0,
PRE_POLY, PBOOLE, AFINSQ_1;
schemes NAT_1, RECDEF_1, FUNCT_1, FUNCT_2, FINSEQ_2, FUNCT_7;
begin :: Preliminaries
theorem Th1:
for A,B being FinSequence, f being Function st rng A \/ rng B c=
dom f ex fA, fB being FinSequence st fA = f*A & fB = f*B & f*(A^B) = fA^fB
proof
let A,B being FinSequence, f being Function;
assume
A1: rng A \/ rng B c= dom f;
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, 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
let k be Nat;
assume 1 <=k & k <= len fAB;
then
A11: k in dom fAB by FINSEQ_3:25;
per cases;
suppose
A12: k in dom fA;
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;
end;
suppose
not k in dom fA;
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;
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 thesis by A10,FINSEQ_1:14;
end;
theorem Th2:
for b being bag of {} holds decomp b = <* <* {}, {} *> *>
proof
let b be bag of {};
A1: EmptyBag 0 = {} --> 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 thesis by A4,FINSEQ_1:40;
end;
theorem Th3:
for i,j being Nat, b being bag of j st i <= j holds (b
|i) is Element of Bags i
proof
let i,j being Nat, b being bag of j;
assume
A1: i <= j;
Segm i c= Segm j
proof
let x be object;
assume x in Segm i;
then x in {y where y is Nat : y < i } by AXIOMS:4;
then consider x9 being 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 Nat : y < j };
hence thesis by A2,AXIOMS:4;
end;
hence thesis by PRE_POLY:def 12;
end;
theorem Th4:
for i, j being set, b1, b2 being bag of j, 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, b1,b2 be bag of j, b19,b29 be bag of i;
assume that
A1: b19=(b1|i) & b29=(b2|i) and
A2: b1 divides b2;
now
let k be object;
A3: dom b19 = i by PARTFUN1:def 2
.= dom b29 by PARTFUN1:def 2;
per cases;
suppose
A4: not k in dom b19;
then b19.k = {} by FUNCT_1:def 2
.= b29.k by A3,A4,FUNCT_1:def 2;
hence b19.k <= b29.k;
end;
suppose
k in dom b19;
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;
end;
end;
hence thesis by PRE_POLY:def 11;
end;
theorem Th5:
for i,j be set, b1, b2 being bag of j, 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, b1, b2 being bag of j, b19, b29 being bag of i;
assume that
A1: b19=(b1|i) and
A2: b29=(b2|i);
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
let x be object;
assume
A7: x in j /\ i;
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;
end;
dom (b1 -' b2) = j by PARTFUN1:def 2;
then
A8: dom ((b1 -' b2)|i) = j /\ i by RELAT_1:61;
A9: now
let x be object;
assume
A10: x in j /\ i;
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;
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;
dom (b19 + b29) = i by PARTFUN1:def 2
.= j /\ i by A1,A3,PARTFUN1:def 2;
hence thesis by A5,A6,FUNCT_1:2;
end;
definition
let n,k be Nat, b be bag of n;
func b bag_extend k -> Element of Bags (n+1) means
:Def1:
it|n = b & it.n = k;
existence
proof
set b1 = b +* (n .--> k);
A1: dom b = n by PARTFUN1:def 2;
A2: dom b1 = dom b \/ dom (n .--> k) by FUNCT_4:def 1
.= dom b \/ {n}
.= Segm n \/ {n} by PARTFUN1:def 2
.= Segm(n+1) by AFINSQ_1:2;
then b1 is ManySortedSet of n+1 by PARTFUN1:def 2,RELAT_1:def 18;
then reconsider b1 as Element of Bags (n+1) by PRE_POLY:def 12;
take b1;
A3: dom (b1|n) = Segm(n+1) /\ Segm n by A2,RELAT_1:61
.= (Segm n \/ {n}) /\ Segm n by AFINSQ_1:2
.= Segm n by XBOOLE_1:21;
now
let x be object;
assume
A4: x in n;
then
A5: x in dom b \/ dom (n .--> k) by A1,XBOOLE_0:def 3;
A6: now
assume x in dom (n .--> k);
then x in {n};
then A: x = n by TARSKI:def 1; then
reconsider x as set;
not x in x;
hence contradiction by A4,A;
end;
thus (b1|n).x=b1.x by A3,A4,FUNCT_1:47
.= b.x by A5,A6,FUNCT_4:def 1;
end;
hence b1|n = b by A3,A1,FUNCT_1:2;
n in {n} by TARSKI:def 1;
then
A7: n in dom (n .--> k);
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;
end;
uniqueness
proof
let b1,b2 be Element of Bags (n+1);
assume that
A8: b1|n = b and
A9: b1.n = k and
A10: b2|n = b and
A11: b2.n = k;
A12: dom b1 = n+1 by PARTFUN1:def 2;
A13: now
let x be object;
assume
A14: x in Segm(n+1);
then
A15: x in Segm n \/ {n} by AFINSQ_1:2;
per cases;
suppose
x in {n};
then x = n by TARSKI:def 1;
hence b1.x = b2.x by A9,A11;
end;
suppose
not x in {n};
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;
end;
end;
dom b2 = n+1 by PARTFUN1:def 2;
hence thesis by A12,A13,FUNCT_1:2;
end;
end;
theorem Th6:
for n being Nat holds EmptyBag (n+1) = (EmptyBag n) bag_extend 0
proof
let n being Nat;
A1: now
let x be object;
assume x in Segm(n+1);
then
A2: x in Segm n \/ {n} by AFINSQ_1:2;
per cases by A2,XBOOLE_0:def 3;
suppose
A3: x in n;
thus (EmptyBag(n+1)).x = 0 by PBOOLE:5
.= (EmptyBag n).x by PBOOLE:5
.= (((EmptyBag n) bag_extend 0)|n).x by Def1
.= ((EmptyBag n) bag_extend 0).x by A3,FUNCT_1:49;
end;
suppose
A4: x in {n};
thus (EmptyBag(n+1)).x = 0 by PBOOLE:5
.= ((EmptyBag n) bag_extend 0).n by Def1
.= ((EmptyBag n) bag_extend 0).x by A4,TARSKI:def 1;
end;
end;
dom (EmptyBag (n+1)) = n+1 & dom ((EmptyBag n) bag_extend 0) = n+1 by
PARTFUN1:def 2;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th7:
for n be Ordinal, b, b1 be bag of n holds b1 in rng divisors b
iff b1 divides b
proof
let n be Ordinal, b, b1 be bag of n;
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,38;
hereby
assume b1 in rng divisors b;
then b1 in S by A1,A3,PRE_POLY:def 2;
hence b1 divides b by A2;
end;
assume b1 divides b;
then b1 in S by A2;
hence thesis by A1,A3,PRE_POLY:def 2;
end;
definition
let X be set, x be Element of X;
func UnitBag x -> Element of Bags X equals
(EmptyBag X)+*(x, 1);
coherence by PRE_POLY:def 12;
end;
theorem Th8:
for X being non empty set, x being Element of X holds support UnitBag x = {x}
proof
let X be non empty set, x be Element of X;
now
let a be object;
hereby
assume
A1: a in support UnitBag x;
now
assume a <> x;
then ((EmptyBag X)+*(x, 1)).a = (EmptyBag X).a by FUNCT_7:32
.= 0 by PBOOLE:5;
hence contradiction by A1,PRE_POLY:def 7;
end;
hence a in {x} by TARSKI:def 1;
end;
EmptyBag X = X --> 0 by PBOOLE:def 3;
then
A2: dom (EmptyBag X) = X;
assume a in {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;
end;
hence thesis by TARSKI:2;
end;
theorem Th9:
for X being non empty set, 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, x be Element of X;
A1: dom (X -->0) = X;
thus (UnitBag x).x = ((X --> 0)+*(x, 1)).x by PBOOLE:def 3
.= 1 by A1,FUNCT_7:31;
let y be Element of X;
assume x <> y;
hence (UnitBag x).y = (EmptyBag X).y by FUNCT_7:32
.= 0 by PBOOLE:5;
end;
theorem Th10:
for X being non empty set, x1, x2 being Element of X st UnitBag
x1 = UnitBag x2 holds x1 = x2
proof
let X be non empty set, x1, x2 be Element of X such that
A1: UnitBag x1 = UnitBag x2 and
A2: x1 <> x2;
1 = (UnitBag x2).x1 by A1,Th9
.= 0 by A2,Th9;
hence contradiction;
end;
theorem Th11:
for X being non empty Ordinal, x be Element of X, L being
well-unital non trivial doubleLoopStr, e being Function of X, L
holds eval(UnitBag x, e) = e.x
proof
let X be non empty Ordinal, x be Element of X, L be well-unital
non trivial doubleLoopStr, e be Function of X, L;
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;
end;
definition
let X be set, x be Element of X, L be unital non empty multLoopStr_0;
func 1_1(x,L) -> Series of X, L equals
0_(X,L)+*(UnitBag x,1_L);
coherence;
end;
theorem Th12:
for X being set, L being unital non trivial
doubleLoopStr, x be 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, L be unital non trivial doubleLoopStr, x be
Element of X;
dom (0_(X,L)) = dom ((Bags X) --> 0.L) by POLYNOM1:def 8
.= Bags X;
hence 1_1(x,L).UnitBag x = 1_L by FUNCT_7:31;
let b be bag of X;
assume b <> UnitBag x;
hence 1_1(x,L).b = (0_(X,L)).b by FUNCT_7:32
.= 0.L by POLYNOM1:22;
end;
theorem Th13:
for X being set, x being Element of X, L being add-associative
right_zeroed right_complementable well-unital right-distributive
non trivial doubleLoopStr holds Support 1_1(x,L) = {UnitBag x}
proof
let X be set, x be Element of X, L be add-associative right_zeroed
right_complementable well-unital right-distributive non trivial
doubleLoopStr;
now
let a be object;
hereby
assume
A1: a in Support 1_1(x,L);
then reconsider b = a as Element of Bags X;
now
assume a <> UnitBag x;
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 4;
end;
hence a in {UnitBag x} by TARSKI:def 1;
end;
assume
A2: a in {UnitBag x};
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 4;
end;
hence thesis by TARSKI:2;
end;
registration
let X be Ordinal, x be Element of X, L be add-associative right_zeroed
right_complementable well-unital right-distributive non trivial
doubleLoopStr;
cluster 1_1(x,L) -> finite-Support;
coherence
proof
Support 1_1(x,L) = {UnitBag x} by Th13;
hence thesis by POLYNOM1:def 5;
end;
end;
theorem Th14:
for L being add-associative right_zeroed right_complementable
well-unital right-distributive non trivial doubleLoopStr, X being
non empty set, x1, x2 being Element of X st 1_1(x1,L) = 1_1(x2,L) holds x1 = x2
proof
let L be add-associative right_zeroed right_complementable well-unital
right-distributive non trivial doubleLoopStr, X be non empty set,
x1, x2 be Element of X such that
A1: 1_1(x1,L) = 1_1(x2,L) and
A2: x1 <> x2;
1_L = 1_1(x2,L).UnitBag x1 by A1,Th12
.= 0.L by A2,Th10,Th12;
hence contradiction;
end;
theorem Th15:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, x being Element of Polynom-Ring L, p be
sequence of L st x = p holds -x = -p
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, x being Element of Polynom-Ring L, p be sequence of L;
assume
A1: x = p;
reconsider x9=x as Polynomial of L by POLYNOM3:def 10;
A2: now
let i be object;
assume
A3: i in NAT;
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;
end;
reconsider mx=-x9 as Element of Polynom-Ring L by POLYNOM3:def 10;
A4: p-p = 0_.L by A2;
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 thesis by A1,RLVECT_1:17;
end;
theorem Th16:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, x, y being Element of Polynom-Ring L, p
, q be sequence of L st x = p & y = q holds x-y = p-q
proof
let L being add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr, x,y being Element of Polynom-Ring L, p,q be sequence
of L;
assume that
A1: x = p and
A2: y = 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;
end;
definition
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr;
let I be non empty Subset of Polynom-Ring L;
func minlen(I) -> non empty Subset of I equals
{ 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
proof
I c= I;
then reconsider I9=I as non empty Subset of I;
defpred P[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
let x be Element of I;
reconsider x9=x as Polynomial of L by POLYNOM3:def 10;
for p be Polynomial of L st x=p holds len x9 = len p;
hence ex y being Element of NAT st P[x,y];
end;
consider f being Function of I,NAT such that
A2: for x being Element of I holds P[x,f.x] from FUNCT_2:sch 3(A1);
min (f.:I9) in f.:I by XXREAL_2:def 7;
then consider x being object 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 as Element of I by A3;
now
let x9,y9 being Polynomial of L;
assume that
A5: x9=x and
A6: y9 in I;
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;
end;
then
A7: x in u;
u c= I
proof
let x be object;
assume x in u;
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 thesis;
end;
hence thesis by A7;
end;
end;
theorem Th17:
for L be right_zeroed add-associative right_complementable
well-unital distributive non empty doubleLoopStr, I be non empty Subset of
Polynom-Ring L, i1, i2 be Polynomial of L st i1 in minlen(I) & i2 in I holds i1
in I & len i1 <= len i2
proof
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, I be non empty Subset of Polynom-Ring L
, i1, i2 be Polynomial of L;
assume that
A1: i1 in minlen(I) and
A2: i2 in I;
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 thesis by A2;
end;
definition
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, n be Nat, a be Element of L;
func monomial(a,n) -> Polynomial of L means
:Def5:
for x being Nat holds (x = n implies it.x = a) & (x <> n implies it.x = 0.L);
existence
proof
reconsider x = 0_.(L)+*(n,a) as sequence of L;
now
let i be Nat;
A1: i in NAT by ORDINAL1:def 12;
assume i >= n+1;
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;
end;
then reconsider x as Polynomial of L by ALGSEQ_1:def 1;
now
let i be Nat;
A2: i in NAT by ORDINAL1:def 12;
thus i = n implies x.i = a
proof
A3: dom 0_.(L) = NAT;
assume i = n;
hence thesis by A2,A3,FUNCT_7:31;
end;
thus i <> n implies x.i = 0.L
proof
assume i <> n;
hence x.i = (NAT --> 0.L).i by FUNCT_7:32
.= 0.L by A2,FUNCOP_1:7;
end;
end;
hence thesis;
end;
uniqueness
proof
let u,v be Polynomial of L such 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);
now
let x be object;
assume
A6: x in NAT;
per cases;
suppose
A7: x = n;
hence u.x = a by A4
.= v.x by A5,A7;
end;
suppose
A8: x <> n;
hence u.x = 0.L by A4,A6
.= v.x by A5,A6,A8;
end;
end;
hence u = v;
end;
end;
theorem Th18:
for L be right_zeroed add-associative right_complementable
well-unital distributive non empty doubleLoopStr, n be Element of NAT, a be
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 right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, n be Element of NAT, a be Element of L;
A1: now
assume
A2: a = 0.L;
now
let i be Nat;
assume i >= 0;
per cases;
suppose
i = n;
thus monomial(a,n).i = 0.L by A2,Def5;
end;
suppose
i<>n;
hence monomial(a,n).i = 0.L by Def5;
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;
end;
now
now
let i be Nat;
assume i >= n+1;
then i > n by NAT_1:13;
hence monomial(a,n).i = 0.L by Def5;
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;
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;
end;
hence thesis by A1;
end;
theorem Th19:
for L be right_zeroed add-associative right_complementable
well-unital distributive non empty doubleLoopStr, n, x be Element of NAT, a
be Element of L, p be Polynomial of L holds (monomial(a,n)*'p).(x+n) = a * (p.x
)
proof
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, n,x be Element of NAT, a be Element of
L, p be Polynomial of L;
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 be 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
A10: dom b c= dom r by A6,FINSEQ_1:26;
let i be Element of NAT;
A11: i - 1 < i by XREAL_1:146;
assume
A12: i in dom b;
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;
end;
then
A15: Sum b = 0.L by POLYNOM3:1;
now
let i be Element of NAT;
A16: n+(1+i) -' 1 = n+i+1 -' 1 .= n+i by NAT_D:34;
assume
A17: i in dom e;
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;
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;
end;
theorem Th20:
for L be right_zeroed add-associative right_complementable
well-unital distributive non empty doubleLoopStr, n, x be Element of NAT, a
be Element of L, p be Polynomial of L holds (p*'monomial(a,n)).(x+n) = (p.x) *
a
proof
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, n,x be Element of NAT, a be Element of
L, p be Polynomial of L;
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 be 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
let i be Element of NAT;
A11: n > n-1 by XREAL_1:146;
assume
A12: i in dom e;
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;
end;
then
A16: Sum e = 0.L by POLYNOM3:1;
now
let i be Element of NAT;
A17: dom b c= dom r by A6,FINSEQ_1:26;
assume
A18: i in dom b;
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;
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;
end;
theorem Th21:
for L be right_zeroed add-associative right_complementable
well-unital distributive non empty doubleLoopStr, p, q be Polynomial of L
holds len (p*'q) <= (len p)+(len q)-'1
proof
let L be right_zeroed add-associative right_complementable well-unital
distributive non empty doubleLoopStr, p,q be Polynomial of L;
now
let i be Nat;
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 be FinSequence of the carrier of L such that
A2: len r = i+1 and
A3: (p*'q).i = Sum r and
A4: for k be 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;
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
let k be Element of NAT;
assume
A6: k in dom r;
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;
per cases;
suppose
k-'1 < len p;
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;
end;
suppose
k-'1 >= len p;
then p.(k-'1) = 0.L by ALGSEQ_1:8;
hence r.k = 0.L by A7;
end;
end;
hence (p*'q).i = 0.L by A3,POLYNOM3:1;
end;
then len p + len q -' 1 is_at_least_length_of p*'q by ALGSEQ_1:def 2;
hence thesis by ALGSEQ_1:def 3;
end;
begin :: On Ring isomorphism
theorem Th22:
for R,S being non empty doubleLoopStr, I being Ideal of R, P
being Function of R,S st P is RingIsomorphism holds P.:I is Ideal of S
proof
let R,S being non empty doubleLoopStr, I being Ideal of R, P being Function
of R,S;
set Q = P.:I;
assume
A1: P is RingIsomorphism;
A2: now
let p, x be Element of S;
assume x in Q;
then consider x9 being object 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 as Element of R by A3;
A6: P is RingMonomorphism RingEpimorphism by A1;
then P is onto;
then consider p9 being object such that
A7: p9 in dom P and
A8: p = P.p9 by FUNCT_1:def 3;
reconsider p9 as Element of R by A7;
A9: p9*x9 in I by A4,IDEAL_1:def 2;
P is RingHomomorphism by A6;
then P is multiplicative;
then p*x = P.(p9*x9) by A5,A8;
hence p*x in Q by A9,FUNCT_2:35;
end;
A10: now
let p, x be Element of S;
assume x in Q;
then consider x9 being object 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 as Element of R by A11;
A14: P is RingMonomorphism RingEpimorphism by A1;
then P is onto;
then consider p9 being object such that
A15: p9 in dom P and
A16: p = P.p9 by FUNCT_1:def 3;
reconsider p9 as Element of R by A15;
A17: x9*p9 in I by A12,IDEAL_1:def 3;
P is RingHomomorphism by A14;
then P is multiplicative;
then x*p = P.(x9*p9) by A13,A16;
hence x*p in Q by A17,FUNCT_2:35;
end;
now
let x, y be Element of S;
assume that
A18: x in Q and
A19: y in Q;
consider x9 being object 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 object 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,y9 as Element of R by A20,A23;
A26: x9+y9 in I by A21,A24,IDEAL_1:def 1;
P is RingMonomorphism RingEpimorphism by A1;
then P is additive;
then x+y = P.(x9+y9) by A22,A25;
hence x+y in Q by A26,FUNCT_2:35;
end;
hence thesis by A2,A10,IDEAL_1:def 1,def 2,def 3;
end;
theorem Th23:
for R,S being add-associative right_zeroed right_complementable
non empty doubleLoopStr, f being Function of R, S st f is RingHomomorphism
holds f.(0.R) = 0.S
proof
let R,S be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let f be Function of R, S;
assume f is RingHomomorphism;
then
A1: f is additive;
f.(0.R)=f.(0.R+0.R) by RLVECT_1:4
.= f.(0.R)+f.(0.R) by A1;
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 thesis;
end;
theorem Th24:
for R, S being add-associative right_zeroed right_complementable
non empty doubleLoopStr, F being non empty Subset of R, G being non empty
Subset of S, P being Function of R, S, lc being LinearCombination of F, LC
being LinearCombination of G, 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 add-associative right_zeroed right_complementable non empty
doubleLoopStr, F be non empty Subset of R, G be non empty Subset of S, P be
Function of R,S, lc be LinearCombination of F, LC be LinearCombination of G, E
be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] such
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));
defpred P[Nat] means for lc9 being LinearCombination of F, LC9
being LinearCombination of G st lc9 = lc|Seg $1 & LC9 = LC|Seg $1 holds P.(Sum
lc9) = Sum LC9;
A5: P is additive multiplicative by A1;
A6: dom lc = dom LC by A2,FINSEQ_3:29;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A8: P[k];
thus P[k+1]
proof
let lc9 be LinearCombination of F, LC9 be LinearCombination of G;
assume that
A9: lc9 = lc| Seg (k+1) and
A10: LC9 = LC|Seg (k+1);
per cases;
suppose
A11: len lc < k+1;
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 thesis by A8,A13;
end;
suppose
A14: len lc >= k+1;
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
.= (Sum LCk)+P.(lc/.(k+1)) by A8
.= (Sum LCk)+P.(((E/.i)`1_3)*((E/.i)`2_3)*((E/.i)`3_3))
by A3,A15,A16
.= (Sum LCk)+P.(((E/.i)`1_3)*((E/.i)`2_3))*P.((E/.i)`3_3)
by A5
.= (Sum LCk)+P.((E/.i)`1_3)*P.((E/.i)`2_3)*P.((E/.i)`3_3)
by A5
.= (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;
end;
end;
end;
A18: lc = lc|Seg len lc & LC = LC|Seg len LC by FINSEQ_3:49;
A19: P[ 0 ]
proof
let lc9 be LinearCombination of F, LC9 be LinearCombination of G such that
A20: lc9 = lc|(Seg 0 qua set) and
A21: LC9 = LC|(Seg 0 qua set);
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;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A19,A7);
hence thesis by A2,A18;
end;
theorem Th25:
for R, S be non empty doubleLoopStr, P be Function of R, S st P
is RingIsomorphism holds P" is RingIsomorphism
proof
let R, S be non empty doubleLoopStr, P be Function of R, S;
assume
A1: P is RingIsomorphism;
then
A2: P is RingEpimorphism;
then
A3: P is onto;
A4: P is one-to-one by A1;
A5: P is additive multiplicative unity-preserving by A2;
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;
A7: P".(1_S) = P".(P.(1_R)) by A5,GROUP_1:def 13
.= ((P qua Function)").(P.(1_R)) by A4,A6,TOPS_2:def 4
.= 1_R by A4,FUNCT_2:26;
let x,y be Element of S;
consider x9 being object such that
A8: x9 in the carrier of R and
A9: P.(x9) = x by A3,FUNCT_2:11;
reconsider x9 as Element of R by A8;
A10: x9 = ((P qua Function)").(P.(x9)) by A4,FUNCT_2:26
.= P".x by A4,A9,A6,TOPS_2:def 4;
consider y9 being object such that
A11: y9 in the carrier of R and
A12: P.(y9) = y by A3,FUNCT_2:11;
reconsider y9 as Element of R by A11;
A13: y9 = ((P qua Function)").(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
.= ((P qua Function)").(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
.= ((P qua Function)").(P.(x9+y9)) by A4,A6,TOPS_2:def 4
.= P".x + P".y by A4,A10,A13,FUNCT_2:26;
hence thesis by A14,A7;
end;
then P" is additive multiplicative unity-preserving by GROUP_1:def 13;
then
A15: P" is RingHomomorphism;
A16: rng P = [#]S by A3;
then rng(P") = [#]R by A4,TOPS_2:49;
then P" is onto;
then
A17: P" is RingEpimorphism by A15;
P" is one-to-one by A4,A16,TOPS_2:50;
hence thesis by A17;
end;
theorem Th26:
for R,S being Abelian add-associative right_zeroed
right_complementable associative distributive well-unital non empty
doubleLoopStr, F being non empty Subset of R, P being Function of R,S st P is
RingIsomorphism holds P.:(F-Ideal) = (P.:F)-Ideal
proof
let R,S being Abelian add-associative right_zeroed right_complementable
associative distributive well-unital non empty doubleLoopStr, F being non
empty Subset of R, P being Function of R,S;
assume
A1: P is RingIsomorphism;
now
let x be object;
A2: dom P = the carrier of R by FUNCT_2:def 1;
assume
A3: 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 be 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;
then
A6: P is one-to-one;
A7: P is onto by A1;
then
A8: (P qua Function)" = P" by A6,TOPS_2:def 4;
(P qua Function)" .: (P.:F) = (P qua Function)"(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;
then P" is RingHomomorphism;
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;
end;
then
A10: (P.:F)-Ideal c= P.:(F-Ideal);
now
let x be object;
assume x in P.:(F-Ideal);
then consider x9 being object 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;
then P is RingHomomorphism;
then x = Sum lc by A12,A13,A14,A15,Th24;
hence x in (P.:F)-Ideal by IDEAL_1:60;
end;
then P.:(F-Ideal) c= (P.:F)-Ideal;
hence thesis by A10,XBOOLE_0:def 10;
end;
theorem Th27:
for R,S being Abelian add-associative right_zeroed
right_complementable associative distributive well-unital non empty
doubleLoopStr, P being Function of R,S st P is RingIsomorphism & R is
Noetherian holds S is Noetherian
proof
let R,S be Abelian add-associative right_zeroed right_complementable
associative distributive well-unital non empty doubleLoopStr, P be Function
of R,S;
assume that
A1: P is RingIsomorphism and
A2: R is Noetherian;
now
P is RingEpimorphism by A1;
then
A3: P is onto;
let I be Ideal of S;
P is RingMonomorphism by A1;
then
A4: P is one-to-one;
reconsider PI=P".:I as Ideal of R by A1,Th22,Th25;
PI is finitely_generated by A2;
then consider F being non empty finite Subset of R such that
A5: P".:I = F-Ideal;
P is onto by A3;
then P" = (P qua Function)" 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;
end;
hence thesis;
end;
theorem Th28:
for R being add-associative right_zeroed right_complementable
associative Abelian distributive well-unital non trivial
doubleLoopStr holds ex P being Function of R, Polynom-Ring (0,R) st P is
RingIsomorphism
proof
deffunc F(object)=Bags {}--> $1;
let R be add-associative right_zeroed right_complementable associative
Abelian distributive well-unital non trivial doubleLoopStr;
consider P being Function such that
A1: dom P = the carrier of R and
A2: for x being object st x in the carrier of R holds P.x=F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng P;
then consider x being object such that
A3: x in the carrier of R and
A4: y = P.x by A1,FUNCT_1:def 3;
reconsider 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 5;
then y9 in the carrier of Polynom-Ring (0,R) by POLYNOM1:def 11;
hence y in the carrier of Polynom-Ring (0,R) by A2,A4;
end;
assume y in the carrier of Polynom-Ring (0,R);
then reconsider y9=y as Function of (Bags {}), R by POLYNOM1:def 11;
dom y9 = Bags {} by FUNCT_2:def 1;
then
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.{};
then y = P.x by A2;
hence y in rng P by A1,FUNCT_1:def 3;
end;
then
A7: rng P = the carrier of Polynom-Ring (0,R) by TARSKI:2;
then reconsider P as Function of R, Polynom-Ring (0,R) by A1,FUNCT_2:1;
A8: P is onto by A7;
A9: EmptyBag {} = {} --> 0;
now
let x,y be Element of R;
reconsider Px = P.x, Py = P.y, Pxy = P.(x+y) as Polynomial of 0, R by
POLYNOM1:def 11;
now
let z be bag of 0;
A10: z in Bags {} by PRE_POLY:def 12;
A11: Py.z = (Bags {} --> y).z by A2
.= y by A10,FUNCOP_1:7;
A12: Px.z = (Bags {} --> x).z by A2
.= x by A10,FUNCOP_1:7;
Pxy.z = (Bags {} --> x+y).z by A2
.= x+y by A10,FUNCOP_1:7;
hence Pxy.z = Px.z + Py.z by A12,A11;
end;
then Pxy = Px + Py by POLYNOM1:16;
hence P.x+P.y = P.(x+y) by POLYNOM1:def 11;
end;
then
A13: P is additive;
now
let x,y be Element of R;
reconsider Px = P.x, Py = P.y, Pxy = P.(x*y) as Polynomial of 0, R by
POLYNOM1:def 11;
now
reconsider s = <* x*y *> as FinSequence of the carrier of R;
let b be bag of 0;
take s;
A14: b in Bags {} by PRE_POLY:def 12;
thus Pxy.b = (Bags {} --> x*y).b by A2
.= x*y by A14,FUNCOP_1:7
.= Sum s by RLVECT_1:44;
A15: decomp b = <* <* {}, {} *> *> by Th2;
A16: len s = 1 by FINSEQ_1:39;
hence len s = len decomp b by A15,FINSEQ_1:39;
A17: len decomp b = 1 by A15,FINSEQ_1:39;
now
set b1 = {}, b2 = {};
let k be Element of NAT;
A18: b1 in Bags {} by PRE_POLY:51,TARSKI:def 1;
then reconsider b1, b2 as bag of 0;
A19: Px.b1 = (Bags {} --> x).b1 by A2
.= x by A18,FUNCOP_1:7;
A20: Py.b2 = (Bags {} --> y).b2 by A2
.= y by A18,FUNCOP_1:7;
assume
A21: k in dom s;
then
A22: 1 <= k & k <= 1 by A16,FINSEQ_3:25;
then
A23: k = 1 by XXREAL_0:1;
take b1, b2;
k in dom decomp b by A17,A22,FINSEQ_3:25;
hence (decomp b)/.k = (decomp b).1 by A23,PARTFUN1:def 6
.= <*b1, b2*> by A15;
thus s/.k = s.1 by A21,A23,PARTFUN1:def 6
.= Px.b1*Py.b2 by A19,A20;
end;
hence for k being Element of NAT st k in dom s ex b1, b2 being bag of 0
st (decomp b)/.k = <*b1, b2*> & s/.k = Px.b1*Py.b2;
end;
then Pxy = Px *' Py by POLYNOM1:def 10;
hence P.x*P.y = P.(x*y) by POLYNOM1:def 11;
end;
then
A24: P is multiplicative;
take P;
reconsider f0 = {{}} --> 0.R, f1 = {{}} --> 1_R as Function of {{}},the
carrier of R;
A25: dom f1 = {{}};
A26: dom f0 = {{}};
A27: {} 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 A9,POLYNOM1:def 9
.= ({{}} --> 0.R)+*({},1_R) by POLYNOM1:def 8,PRE_POLY:51
.= ({{}} --> 0.R)+*({} .--> 1_R) by A27,FUNCT_7:def 3
.= ({{}} --> 1_R) by A26,A25,FUNCT_4:19
.= P.(1_R)by A2,PRE_POLY:51;
then P is unity-preserving by GROUP_1:def 13;
then
A28: P is RingHomomorphism by A13,A24;
then
A29: P is RingEpimorphism by A8;
now
let x1,x2 be object;
assume that
A30: x1 in dom P and
A31: x2 in dom P;
assume P.x1 = P.x2;
then (Bags {} --> x1) = P.x2 by A2,A30;
then (Bags {} --> x1) = (Bags {} --> x2) by A2,A31;
hence x1 = x2 by FUNCT_4:6;
end;
then P is one-to-one by FUNCT_1:def 4;
then P is RingMonomorphism by A28;
hence thesis by A29;
end;
theorem Th29:
for R being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Nat,
b being bag of n, p1 being Polynomial of n, R, F being FinSequence of
the carrier of Polynom-Ring (n,R) st p1 = Sum F 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 right_zeroed add-associative right_complementable well-unital
distributive non trivial doubleLoopStr, n be Nat, b be
bag of n,p1 be Polynomial of n, R, F be FinSequence of the carrier of
Polynom-Ring (n,R);
assume
A1: p1 = Sum F;
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set CPNR = the carrier of PNR;
defpred P1[Element of CPNR, Element of CR] means for p being Polynomial of n
, R st p = $1 holds $2 = p.b;
A2: now
let x be Element of CPNR;
reconsider x9=x as Polynomial of n, R by POLYNOM1:def 11;
P1[x,x9.b];
hence ex y being Element of CR st P1[x,y];
end;
consider g be Function of CPNR,CR such that
A3: for x being Element of CPNR holds P1[x,g.x] from FUNCT_2:sch 3(A2);
take g;
now
let p be Polynomial of n,R;
reconsider p9=p as Element of CPNR by POLYNOM1:def 11;
P1[p9,g.p9] by A3;
hence g.p = p.b;
end;
hence for p being Polynomial of n, R holds g.p = p.b;
defpred P2[Nat] means for F9 being FinSequence of CPNR, p19 being Polynomial
of n, R st len F9 <= $1 & p19 = Sum F9 holds p19.b = Sum (g * F9);
A4: for k being Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume
A5: P2[k];
now
let F9 be FinSequence of CPNR, p19 be Polynomial of n, R;
assume that
A6: len F9 <= k+1 and
A7: p19 = Sum F9;
per cases;
suppose
len F9 < k+1;
then len F9 <= k by NAT_1:13;
hence p19.b = Sum (g * F9) by A5,A7;
end;
suppose
len F9 >= k+1;
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= CPNR by XBOOLE_1:1;
then reconsider q as FinSequence of CPNR by FINSEQ_1:def 4;
rng p c= rng F9 by A10,FINSEQ_1:29;
then rng p c= CPNR by XBOOLE_1:1;
then reconsider p as FinSequence of CPNR 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 11;
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 CPNR;
reconsider q99=q9 as Polynomial of n, R by POLYNOM1:def 11;
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 11;
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;
end;
end;
hence thesis;
end;
A16: P2[ 0 ]
proof
let F9 being FinSequence of CPNR, p19 be Polynomial of n, R;
assume that
A17: len F9 <= 0 and
A18: p19 = Sum F9;
A19: F9 = <*> (CPNR) by A17;
then g * F9 = <*> (CR);
then
A20: Sum (g * F9) = 0.R by RLVECT_1:43;
p19 = 0.PNR by A18,A19,RLVECT_1:43
.= 0_(n, R) by POLYNOM1:def 11;
hence thesis by A20,POLYNOM1:22;
end;
for k being Nat holds P2[k] from NAT_1:sch 2(A16,A4);
then P2[len F];
hence thesis by A1;
end;
definition
let R be Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr, n be Nat;
func upm (n,R) -> Function of Polynom-Ring (Polynom-Ring(n,R)), Polynom-Ring
(n+1,R) means
:Def6:
for p1 being (Polynomial of Polynom-Ring (n,R)), p2 being
(Polynomial of n, R), p3 being (Polynomial of (n+1), R), b being bag of n+1 st
p3 = it.p1 & p2 = p1.(b.n) holds p3.b = p2.(b|n);
existence
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 PRPNR;
set CPN1R = the carrier of PN1R;
defpred P1[Element of CPRPNR, Element of CPN1R] means for p1 being (
Polynomial of PNR), p2 being (Polynomial of n, R), p3 being (Polynomial of (n+1
), R), b being bag of n+1 st p1 = $1 & p3 = $2 & p2 = p1.(b.n) holds p3.b = p2.
(b|n);
A1: now
let x being Element of CPRPNR;
reconsider p1=x as Polynomial of PNR by POLYNOM3:def 10;
defpred P2[Element of Bags (n+1), Element of CR] means for p2 being (
Polynomial of n, R) st p2 = p1.($1.n) holds $2 = p2.($1|n);
deffunc F(object)=
{ 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
let k be object;
assume k in NAT;
set Ak = F(k);
Ak c= Bags (n+1)
proof
let b be object;
assume b in Ak;
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 thesis;
end;
hence Ak in bool Bags (n+1);
end;
consider A being sequence of bool Bags (n+1) such that
A3: for k being object st k in NAT holds A.k =F(k) from FUNCT_2:sch 2(
A2);
now
let X be set;
assume X in A .: len p1;
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 11;
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;
per cases;
suppose
A6: Support p2 = {};
now
assume A.k <> {};
then consider b being object 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;
end;
hence X is finite by A4;
end;
suppose
A8: Support p2 <> {};
then consider b2 being object such that
A9: b2 in Support p2 by XBOOLE_0:def 1;
reconsider 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 P3[Element of Ak, Element of Supportp2] means for b being
Element of Bags (n+1) st $1 = b holds $2 = b|n;
A11: now
let x be Element of Ak;
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;
P3[x,bn] by A12;
hence ex y being Element of Supportp2 st P3[x,y];
end;
consider f being Function of Ak,Supportp2 such that
A14: for x being Element of Ak holds P3[x,f.x] from FUNCT_2:sch
3(A11);
A15: dom f = Ak by FUNCT_2:def 1;
now
let x1,x2 be object;
assume that
A16: x1 in dom f and
A17: x2 in dom f and
A18: f.x1 = f.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;
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;
end;
end;
then
A25: union (A .: len p1) is finite by FINSET_1:7;
A26: now
let b be Element of Bags (n+1);
reconsider p2 = p1.(b.n) as Polynomial of n, R by POLYNOM1:def 11;
n < n+1 by XREAL_1:29;
then reconsider bn = b|n as bag of n by Th3;
P2[b,p2.bn];
hence ex r being Element of CR st P2[b,r];
end;
consider y being Function of Bags (n+1), CR such that
A27: for b being Element of Bags (n+1) holds P2[b,y.b] from FUNCT_2:
sch 3 (A26);
reconsider y as Function of Bags (n+1), R;
reconsider y as Series of (n+1), R;
Support y c= union (A .: len p1)
proof
let x be object;
A28: dom A = NAT by FUNCT_2:def 1;
assume
A29: x in Support y;
then reconsider x9=x as Element of Bags (n+1);
reconsider p2 = p1.(x9.n) as Polynomial of n, R by POLYNOM1:def 11;
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 4;
then
A30: p2.(xn) <> 0.R by A27;
then p2 <> 0_ (n, R) by POLYNOM1:22;
then p2 <> 0.PNR by POLYNOM1:def 11;
then
A31: x9.n < len p1 by ALGSEQ_1:8;
len p1 = { i where i is 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 4;
then x in A.(x9.n) by A33;
hence thesis by A32,TARSKI:def 4;
end;
then y is finite-Support by A25,POLYNOM1:def 5;
then reconsider y9=y as Element of CPN1R by POLYNOM1:def 11;
now
let p1 be (Polynomial of PNR), p2 be (Polynomial of n, R), p3 be (
Polynomial of (n+1), R), b be bag of n+1;
A34: b is Element of Bags (n+1) by PRE_POLY:def 12;
assume p1 = x & p3 = y9 & p2 = p1.(b.n);
hence p3.b = p2.(b|n) by A27,A34;
end;
hence ex y being Element of CPN1R st P1[x,y];
end;
consider P being Function of CPRPNR,CPN1R such that
A35: for x being Element of CPRPNR holds P1[x,P.x] from FUNCT_2:sch 3
(A1);
reconsider P as Function of PRPNR, PN1R;
take P;
now
let p1 being (Polynomial of Polynom-Ring (n,R)), p2 being (Polynomial of
n, R), p3 being (Polynomial of (n+1), R), b being bag of n+1;
A36: p1 in CPRPNR by POLYNOM3:def 10;
assume p3 = P.p1 & p2 = p1.(b.n);
hence p3.b = p2.(b|n) by A35,A36;
end;
hence thesis;
end;
uniqueness
proof
let A, B be Function of Polynom-Ring (Polynom-Ring(n,R)), Polynom-Ring(n+1
,R);
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)), p2 being (
Polynomial of n, R), p3 being (Polynomial of (n+1), R), b being bag of n+1 st
p3 = A.p1 & p2 = p1.(b.n) holds p3.b = p2.(b|n);
assume
A38: for p1 being (Polynomial of Polynom-Ring (n,R)), p2 being (
Polynomial of n, R), p3 being (Polynomial of (n+1), R), b being bag of n+1 st
p3 = B.p1 & p2 = p1.(b.n) holds p3.b = p2.(b|n);
now
let x be object;
assume
A39: x in CPRPNR;
then reconsider x9=x as Polynomial of PNR by POLYNOM3:def 10;
A.x in CPN1R & B.x in CPN1R by A39,FUNCT_2:5;
then reconsider Ax=A.x, Bx=B.x as (Polynomial of n+1,R) by
POLYNOM1:def 11;
now
let b be object;
assume b in Bags (n+1);
then reconsider b9=b as Element of Bags (n+1);
reconsider p2 = x9.(b9.n) as Polynomial of n, R by POLYNOM1:def 11;
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;
end;
hence A.x = B.x by FUNCT_2:12;
end;
hence A=B;
end;
end;
registration
let R be Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr, n be Nat;
cluster upm (n,R) -> additive;
coherence
proof
set P = upm (n,R);
set PNR = Polynom-Ring(n,R);
thus P is additive
proof
let x,y be Element of Polynom-Ring (Polynom-Ring(n,R));
reconsider x9=x, y9=y, xy9=x+y as Polynomial of PNR by POLYNOM3:def 10;
reconsider Pxy = P.(x+y), Px = P.x, Py = P.y as (Polynomial of n+1, R)
by POLYNOM1:def 11;
A1: xy9 = x9+y9 by POLYNOM3:def 10;
now
let b be object;
assume b in Bags (n+1);
then reconsider b9=b as bag of n+1;
reconsider xybn = (x9+y9).(b9.n) as Polynomial of n,R by
POLYNOM1:def 11;
reconsider xbn=x9.(b9.n), ybn = y9.(b9.n) as Polynomial of n, R by
POLYNOM1:def 11;
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 11;
hence Pxy.b = (xbn + ybn).bn by A1,Def6
.= Px.b9 + Py.b9 by A2,POLYNOM1:15
.= (Px + Py).b by POLYNOM1:15;
end;
hence P.(x+y) = Px+Py by FUNCT_2:12
.= P.x + P.y by POLYNOM1:def 11;
end;
end;
cluster upm (n,R) -> multiplicative;
coherence
proof
set P = upm (n,R);
set CR = the carrier of R;
set PNR = Polynom-Ring(n,R);
set CPNR = the carrier of PNR;
thus P is multiplicative
proof
let x9,y9 be Element of the carrier of Polynom-Ring (Polynom-Ring(n,R));
reconsider x=x9, y=y9, xy = x9*y9 as Polynomial of PNR by POLYNOM3:def 10
;
reconsider Pxy = P.(x9*y9), PxPy = (P.x9)*(P.y9), Px=P.x9, Py=P.y9 as
Polynomial of n+1,R by POLYNOM1:def 11;
A3: xy = x*'y by POLYNOM3:def 10;
A4: PxPy = Px*'Py by POLYNOM1:def 11;
now
let b9 be object;
assume b9 in Bags (n+1);
then reconsider b=b9 as Element of Bags (n+1);
consider r be FinSequence of CPNR such that
A5: len r = (b.n)+1 and
A6: (xy).(b.n) = Sum r and
A7: for k be 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 P3[object,object] means
for p,q being Polynomial of n,R, fcr being
FinSequence of CR, i being Element of NAT st i = $1 & p = x.(i-'1) & q = y.((b.
n)+1-'i) & fcr = $2 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 11;
consider u being FinSequence of CR 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
ex b1, b2 being bag of n+1 st (decomp b)/.k = <*b1, b2*> &
u/.k = Px.b1*Py.b2 by A4,POLYNOM1:def 10;
A11: now
let e9 be object;
assume e9 in dom r;
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 11;
consider fcr being FinSequence of CR 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 10;
A13: fcr in CR* by FINSEQ_1:def 11;
P3[e,fcr] by A12;
hence ex u being object st u in CR* & P3[e9,u] by A13;
end;
consider s being Function of dom r, CR* such that
A14: for e being object st e in dom r holds P3[e,s.e] from FUNCT_2:
sch 1(A11 );
A15: rng s c= CR*;
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 as FinSequence of CR* by A15,FINSEQ_1:def 4;
consider g being Function of CPNR, CR 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
reconsider p9=x.(1-'1), q9=y.((b.n)+1-'1) as Polynomial of n,R by
POLYNOM1:def 11;
s/.1 is FinSequence of CR;
then
A22: s.1 is FinSequence of CR 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;
end;
defpred P1[object,object] means
for i,n1 being Element of NAT, b1 being bag
of n+1 st n1=$1 & 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)) & $2 = (Sum Card (s|(b1
.n+1-'1))) + i;
set t = FlattenSeq s;
A23: now
let n19 be object;
assume
A24: n19 in dom u;
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 11;
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 object such that
A29: i in dom divisors bn and
A30: b1n = (divisors bn).i by FUNCT_1:def 3;
reconsider 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 CR* 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: n2 in dom t by A29,A32,PRE_POLY:30;
for i9,n19 being Element of NAT, 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)) & n2 = (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 object st n29 in dom t & P1[n19,n29] by A34;
end;
consider p being Function of dom u, dom t such that
A35: for x being object st x in dom u holds P1[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 t > 0 by PRE_POLY:27;
then
A36: t <> {};
then
A37: dom p = dom u by FUNCT_2:def 1;
now
let n19,n29 be object;
assume that
A38: n19 in dom p and
A39: n29 in dom p and
A40: p.n19 = p.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 object such that
A45: i2 in dom divisors bn and
A46: b2n = (divisors bn).i2 by FUNCT_1:def 3;
reconsider 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 object such that
A48: i1 in dom divisors bn and
A49: b1n = (divisors bn).i1 by FUNCT_1:def 3;
reconsider 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;
end;
then
A54: p is one-to-one by FUNCT_1:def 4;
dom t c= rng p
proof
let n19 be object;
assume
A55: n19 in dom t;
then reconsider n1=n19 as Element of NAT;
consider i, j being 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 = t.n1 by A55,PRE_POLY:29;
s.i in CR* by A16,A56,FUNCT_2:5;
then
A59: s.i is FinSequence of CR 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 11;
A60: bij.n = i-'1 by Def1;
1 <= i by A56,FINSEQ_3:25;
then
A61: bij.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
let k be object;
per cases;
suppose
A66: k in n+1;
now
per cases;
suppose
A67: k in n;
then
A68: b.k = bn.k by FUNCT_1:49;
bij.k = (bij|n).k by A67,FUNCT_1:49
.= bj.k by Def1;
hence bij.k <= b.k by A65,A68,PRE_POLY:def 11;
end;
suppose
A69: not k in n;
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;
Segm(n+1) = Segm n \/ {n} by AFINSQ_1:2;
then k in {n} by A66,A69,XBOOLE_0:def 3;
then
A72: k = n by TARSKI:def 1;
then bij.k = i -' 1 by Def1;
hence bij.k <= b.k by A72,A70,A71,XREAL_1:233;
end;
end;
hence bij.k <= b.k;
end;
suppose
A73: not k in n+1;
dom bij = n+1 by PARTFUN1:def 2;
hence bij.k <= b.k by A73,FUNCT_1:def 2;
end;
end;
then bij divides b by PRE_POLY:def 11;
then bij in rng divisors b by Th7;
then consider k being object such that
A74: k in dom divisors b and
A75: bij = (divisors b).k by FUNCT_1:def 3;
A76: dom p = dom u by A36,FUNCT_2:def 1;
(divisors bn).j = bij|n by A64,Def1;
then p.k = (Sum Card (s|(bij.n+1-'1))) + j by A35,A57,A63,A74,A75,A62
;
hence thesis by A58,A74,A76,A62,A61,FUNCT_1:def 3;
end;
then
A77: rng p = dom t 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
let k be Nat;
reconsider p = x.(k-'1), q = y.((b.n)+1-'k) as Polynomial of n, R by
POLYNOM1:def 11;
reconsider pq9 = p *' q as Element of CPNR by POLYNOM1:def 11;
assume
A80: k in dom r;
then reconsider sk=s.k as Element of CR* by FUNCT_2:5;
reconsider sk as FinSequence of CR;
A81: r.k = x.(k-'1)*y.((b.n)+1-'k) by A7,A80
.= pq9 by POLYNOM1:def 11;
(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;
end;
A82: now
let n1 be Nat;
reconsider b19 = (divisors b)/.n1 as bag of n+1;
assume
A83: n1 in dom u;
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 11;
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 object such that
A94: i in dom divisors bn and
A95: b1n = (divisors bn).i by FUNCT_1:def 3;
reconsider 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 CR* by A16,FUNCT_2:5;
then reconsider sb1n1=s.(b1.n+1) as FinSequence of CR;
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: t.(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 = t.(p.n1) by A89,A94,A104,A103,A108,A109,PARTFUN1:def 6;
end;
dom r = dom (g * r) by FINSEQ_3:120;
then Sum s = g * r by A78,A79,FINSEQ_1:13;
then
A110: Sum t = Pxy.b by A19,POLYNOM1:14;
A111: len u = card dom u by CARD_1:62
.= card (p qua set) by A37,CARD_1:62
.= card dom t by A54,A77,PRE_POLY:19
.= len t by CARD_1:62;
then
A112: dom u = dom t 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;
end;
hence P.(x9*y9) = (P.x9)*(P.y9) by FUNCT_2:12;
end;
end;
cluster upm (n,R) -> unity-preserving;
coherence
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 PN1R;
reconsider p1 = 1_PRPNR as Polynomial of PNR by POLYNOM3:def 10;
reconsider p19 = 1_PN1R as (Polynomial of n+1, R) by POLYNOM1:def 11;
P.(1_PRPNR) in CPN1R;
then reconsider p3 = P.p1 as (Polynomial of n+1, R) by POLYNOM1:def 11;
now
let x be object;
assume x in Bags (n+1);
then reconsider b = x as Element of Bags (n+1);
reconsider p2 = p1.(b.n) as Polynomial of n, R by POLYNOM1:def 11;
A113: p3.b = p2.(b|n) by Def6;
now
per cases;
suppose
A114: b|n = EmptyBag(n) & b.n = 0;
then
A115: b = (EmptyBag n) bag_extend 0 by Def1
.=EmptyBag (n+1) by Th6;
p2 = (1_. (PNR)).0 by A114,POLYNOM3:def 10
.= 1_(PNR) 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;
end;
suppose
A116: b|n <> EmptyBag(n) or b.n <> 0;
A117: now
n < n+1 by NAT_1:13;
then
A118: b|n is bag of n by Th3;
A119: p2 = (1_. (PNR)).(b.n) by POLYNOM3:def 10;
per cases;
suppose
A120: b.n = 0;
then p2 = 1_(PNR) by A119,POLYNOM3:30
.= 1_ (n,R) by POLYNOM1:31;
hence p3.b = 0.R by A113,A116,A118,A120,POLYNOM1:25;
end;
suppose
b.n <> 0;
then p2 = 0.(PNR) by A119,POLYNOM3:30
.= 0_ (n, R) by POLYNOM1:def 11;
hence p3.b = 0.R by A113,A118,POLYNOM1:22;
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;
end;
end;
hence p3.x = p19.x;
end;
then p19 = p3;
hence thesis by GROUP_1:def 13;
end;
cluster upm (n,R) -> one-to-one;
coherence
proof
set P = upm (n,R);
set PNR = Polynom-Ring(n,R);
set PRPNR = Polynom-Ring (Polynom-Ring(n,R));
now
let x9,y9 being Element of PRPNR;
reconsider x=x9, y=y9 as Polynomial of PNR by POLYNOM3:def 10;
reconsider Py = P.y9 as Polynomial of n+1,R by POLYNOM1:def 11;
assume
A121: P.x9 = P.y9;
now
let bn9 be object;
assume bn9 in NAT;
then reconsider bn = bn9 as Element of NAT;
reconsider xbn=x.bn, ybn = y.bn as Polynomial of n,R by POLYNOM1:def 11
;
now
let b9 be object;
assume b9 in Bags n;
then reconsider b = b9 as bag of n;
set bn1 = b bag_extend bn;
A122: bn1|n = b & bn1.n = bn by Def1;
then (xbn).b = Py.bn1 by A121,Def6
.= (ybn).b by A122,Def6;
hence (xbn).b9 = (ybn).b9;
end;
hence x.bn9 = y.bn9 by FUNCT_2:12;
end;
hence x9=y9 by FUNCT_2:12;
end;
hence thesis by WAYBEL_1:def 1;
end;
end;
definition
let R be Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr, n be Nat;
func mpu (n,R) -> Function of Polynom-Ring (n+1,R), Polynom-Ring
Polynom-Ring(n,R) means
:Def7:
for p1 being (Polynomial of n+1,R), p2 being (
Polynomial of n, R), p3 being (Polynomial of Polynom-Ring (n, R)), i being
Element of NAT, b being bag of n st p3 = it.p1 & p2 = p3.i holds p2.b = p1.(b
bag_extend i);
existence
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 PRPNR;
set CPN1R = the carrier of PN1R;
set CPNR = the carrier of PNR;
defpred P1[Element of CPN1R, Element of CPRPNR] means for p1 being (
Polynomial of n+1,R), p2 being (Polynomial of n, R), p3 being (Polynomial of
Polynom-Ring (n, R)), i being Element of NAT, b being bag of n st p1 = $1 & p3
= $2 & p2 = p3.i holds p2.b = p1.(b bag_extend i);
A1: now
let x being Element of CPN1R;
reconsider p1=x as Polynomial of n+1,R by POLYNOM1:def 11;
defpred P2[Element of NAT, Element of CPNR] means for p2 being (
Polynomial of n, R), b being bag of n st p2 = $2 holds p2.b = p1.(b bag_extend
$1);
A2: now
let i being Element of NAT;
deffunc F(Element of Bags n)=p1.($1 bag_extend i);
consider p2 being Function of Bags n,CR such that
A3: for b being Element of Bags n holds p2.b = F(b) from FUNCT_2:
sch 4;
reconsider p2 as Function of Bags n, R;
reconsider p2 as Series of n, R;
now
per cases;
suppose
A4: Support p1 = {};
now
assume Support p2 <> {};
then consider b being object such that
A5: b in Support p2 by XBOOLE_0:def 1;
reconsider b as Element of Bags n by A5;
p2.b <> 0.R by A5,POLYNOM1:def 4;
then p1.(b bag_extend i) <> 0.R by A3;
hence Support p1 <> {} by POLYNOM1:def 4;
end;
hence Support p2 is finite by A4;
end;
suppose
Support p2 = {};
hence Support p2 is finite;
end;
suppose
A6: Support p1 <> {} & Support p2 <> {};
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 P[Element of Supportp2,set] means $2 = $1 bag_extend i;
A7: now
let x being Element of Supportp2;
x is Element of Bags n & p2.x <> 0.R by POLYNOM1:def 4;
then p1.(x bag_extend i) <> 0.R by A3;
then x bag_extend i in Support p1 by POLYNOM1:def 4;
hence ex y being Element of Supportp1 st P[x,y];
end;
consider f being Function of Supportp2,Supportp1 such that
A8: for x being Element of Supportp2 holds P[x,f.x] from
FUNCT_2:sch 3(A7);
A9: dom f = Supportp2 by FUNCT_2:def 1;
now
let x1,x2 be object;
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f.x1 = f.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;
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;
end;
end;
then p2 is finite-Support by POLYNOM1:def 5;
then reconsider p29=p2 as Element of CPNR by POLYNOM1:def 11;
take p29;
now
let p299 being (Polynomial of n, R), b being bag of n;
A15: b is Element of Bags n by PRE_POLY:def 12;
assume p299 = p29;
hence p299.b = p1.(b bag_extend i) by A3,A15;
end;
hence P2[i,p29];
end;
consider p3 being sequence of CPNR such that
A16: for x being Element of NAT holds P2[x,p3.x] from FUNCT_2:sch 3(
A2);
reconsider p3 as sequence of PNR;
now
per cases;
suppose
A17: Support p1 = {};
now
let i be Nat;
assume i >= 0;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
reconsider p2 = p3.i1 as Polynomial of n, R by POLYNOM1:def 11;
A18: now
let x be object;
assume x in Bags n;
then reconsider x9=x as Element of Bags n;
p1.(x9 bag_extend i) = 0.R by A17,POLYNOM1:def 4;
then p2.x9 = 0.R by A16;
hence p2.x = ((Bags n) --> 0.R).x;
end;
p2 = (Bags n) --> 0.R by A18;
hence p3.i = 0_(n,R) by POLYNOM1:def 8
.= 0.PNR by POLYNOM1:def 11;
end;
hence p3 is finite-Support by ALGSEQ_1:def 1;
end;
suppose
Support p1 <> {};
then reconsider
Supportp1 = Support p1 as finite non empty Subset of Bags
(n+1);
deffunc F(Element of Bags (n+1))=$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 = F(x) from
FUNCT_2:sch 4;
reconsider j = max (f .: Supportp1) as Element of NAT by
ORDINAL1:def 12;
now
let i being Nat;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider p2 = p3.i1 as Polynomial of n, R by POLYNOM1:def 11;
assume
A20: i >= j+1;
A21: now
let x be object;
assume x in Bags n;
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 4;
then p2.x9 = 0.R by A16;
hence p2.x = ((Bags n) --> 0.R).x;
end;
p2 = (Bags n) --> 0.R by A21;
hence p3.i = 0_(n,R) by POLYNOM1:def 8
.= 0.PNR by POLYNOM1:def 11;
end;
hence p3 is finite-Support by ALGSEQ_1:def 1;
end;
end;
then reconsider y=p3 as Element of CPRPNR by POLYNOM3:def 10;
take y;
thus P1[x,y] by A16;
end;
consider P being Function of CPN1R,CPRPNR such that
A23: for x being Element of CPN1R holds P1[x,P.x] from FUNCT_2:sch 3(
A1);
reconsider P as Function of PN1R,PRPNR;
take P;
now
let p1 being (Polynomial of n+1,R), p2 being (Polynomial of n, R ) , p3
being (Polynomial of Polynom-Ring (n, R)), i being Element of NAT, b being bag
of n;
A24: p1 in CPN1R by POLYNOM1:def 11;
assume p3 = P.p1 & p2 = p3.i;
hence p2.b = p1.(b bag_extend i) by A23,A24;
end;
hence thesis;
end;
uniqueness
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 PN1R;
let A,B be Function of PN1R,PRPNR;
assume
A25: for p1 being (Polynomial of n+1,R), p2 being (Polynomial of n, R)
, p3 being (Polynomial of Polynom-Ring (n, R)), i being Element of NAT, b being
bag of n st p3 = A.p1 & p2 = p3.i holds p2.b = p1.(b bag_extend i);
assume
A26: for p1 being (Polynomial of n+1,R), p2 being (Polynomial of n, R)
, p3 being (Polynomial of Polynom-Ring (n, R)), i being Element of NAT, b being
bag of n st p3 = B.p1 & p2 = p3.i holds p2.b = p1.(b bag_extend i);
now
let x be object;
assume
A27: x in CPN1R;
then reconsider x99=x as Element of CPN1R;
reconsider x9=x as Polynomial of n+1, R by A27,POLYNOM1:def 11;
reconsider Ax=A.x99,Bx=B.x99 as Polynomial of PNR by POLYNOM3:def 10;
now
let i be object;
assume i in NAT;
then reconsider i9=i as Element of NAT;
reconsider Axi=Ax.i9, Bxi=Bx.i9 as Polynomial of n, R by
POLYNOM1:def 11;
now
let b be object;
assume b in Bags n;
then reconsider b9=b as bag of n;
thus Axi.b = x9.(b9 bag_extend i9) by A25
.= Bxi.b by A26;
end;
hence Ax.i = Bx.i by FUNCT_2:12;
end;
hence A.x=B.x by FUNCT_2:12;
end;
hence A=B;
end;
end;
theorem Th30:
for R being Abelian add-associative right_zeroed
right_complementable associative distributive well-unital commutative non
trivial non empty doubleLoopStr, n being Nat, p being Element of
Polynom-Ring (n+1,R) holds upm(n,R).(mpu(n,R).p) = p
proof
let R being Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr, n being Nat, p being Element of Polynom-Ring (n+1,R);
set PNR = Polynom-Ring(n,R);
reconsider p9=p as Polynomial of (n+1), R by POLYNOM1:def 11;
reconsider upmmpup = upm(n,R).(mpu(n,R).p) as Polynomial of (n+1), R by
POLYNOM1:def 11;
reconsider mpup = (mpu(n,R).p) as Polynomial of PNR by POLYNOM3:def 10;
now
let b9 be object;
assume b9 in Bags (n+1);
then reconsider b=b9 as Element of Bags (n+1);
reconsider mpupbn = mpup.(b.n) as Polynomial of n, R by POLYNOM1:def 11;
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;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th31:
for R being Abelian add-associative right_zeroed
right_complementable associative distributive well-unital commutative non
trivial non empty doubleLoopStr, n being 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 Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr, n being Nat;
set PN1R = Polynom-Ring(n+1,R);
set CPRPNR = the carrier of Polynom-Ring (Polynom-Ring(n,R));
set CPN1R = the carrier of PN1R;
set P = upm (n,R);
now
let p be object;
assume p in CPN1R;
then reconsider p9 = p as Element of CPN1R;
dom P = CPRPNR & P.(mpu(n,R).p9) = p9 by Th30,FUNCT_2:def 1;
hence p in rng P by FUNCT_1:def 3;
end;
then CPN1R c= rng P;
then rng P = CPN1R by XBOOLE_0:def 10;
then P is onto;
then P is RingEpimorphism;
then P is RingIsomorphism;
hence thesis;
end;
begin :: Hilbert basis theorem
registration
let R be Noetherian Abelian add-associative right_zeroed
right_complementable associative distributive well-unital commutative non
empty doubleLoopStr;
::$N Hilbert Basis Theorem
::$L https://en.wikipedia.org/wiki/Hilbert's_basis_theorem Hilbert Basis Theorem
cluster Polynom-Ring R -> Noetherian;
coherence
proof
set cR = the carrier of R;
set PR = Polynom-Ring R;
set cPR = the carrier of PR;
now
assume PR is non Noetherian;
then consider I being Ideal of PR such that
A1: I is non finitely_generated;
defpred P1[set,set,set] means ($2 is non empty finite Subset of I)
implies (ex A,B being non empty Subset of cPR st A = $2 & B = I\(A-Ideal) & ex
r being Element of cPR st r in minlen(B) & $3 = $2 \/ {r});
A2: now
let n be Nat, x be Subset of cPR;
per cases;
suppose
not x is non empty finite Subset of I;
hence ex y be Subset of cPR st P1[n,x,y];
end;
suppose
A3: x is non empty finite Subset of I;
then reconsider x9=x as non empty Subset of cPR;
set B = I\(x9 -Ideal);
now
assume B = {};
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;
end;
then reconsider B as non empty Subset of cPR;
consider r being object such that
A5: r in minlen (B) by XBOOLE_0:def 1;
minlen(B) c= cPR by XBOOLE_1:1;
then reconsider r as Element of cPR by A5;
P1[n,x,x9 \/ {r}] by A5;
hence ex y be Subset of cPR st P1[n,x,y];
end;
end;
consider F be sequence of bool cPR such that
A6: F.0 = {0.PR} & for n be Nat holds P1[n,F.n,F.(n+1)]
from RECDEF_1:sch 2(A2);
defpred P2[set,set] means ex n being Element of NAT, A,B being non empty
Subset of cPR st A = F.n & B = I\(A-Ideal) & n = $1 & F.(n+1) = F.n \/ {$2} &
$2 in minlen(B);
defpred P[Nat] means F.$1 is non empty finite Subset of I;
A7: now
let n be Nat;
assume P[n];
then reconsider Fn=F.n as non empty finite Subset of I;
consider A,B being non empty Subset of cPR such that
A = Fn and
A8: B = I\(A-Ideal) and
A9: ex r being Element of cPR st r in minlen(B) & F.(n+1)= Fn \/ {r} by A6;
consider r being Element of cPR 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 P[n+1] by A11,XBOOLE_1:8;
end;
F.0 c= I
proof
let x be object;
assume x in F.0;
then x = 0.PR by A6,TARSKI:def 1;
hence thesis by IDEAL_1:2;
end;
then
A12: P[ 0 ] by A6;
A13: for n being Nat holds P[n] from NAT_1:sch 2(A12,A7);
A14: now
let x be Element of NAT;
ex A,B being non empty Subset of cPR st A = F.x & B = I\ (A-Ideal)
& ex r being Element of cPR st r in minlen(B)&F.(x+1)=F.x \/ {r} by A6,A13;
hence ex y being Element of cPR st P2[x,y];
end;
consider f being sequence of cPR such that
A15: for x being Element of NAT holds P2[x,f.x] from FUNCT_2:sch 3(A14);
A16: for x being Nat holds P2[x,f.x]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A15;
end;
A17: for i,j being Element of NAT st i <= j holds F.i c= F.j
proof
let i,j be Element of NAT;
defpred P[Nat] means F.i c= F.(i+$1);
assume i<=j;
then consider m being Nat such that
A18: j = i+m by NAT_1:10;
A19: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
ex A,B being non empty Subset of cPR st A = F.(i+m) & B = I\(A
-Ideal) & ex r being Element of cPR st r in minlen(B) & F.((i+m)+1) = F. (i+m)
\/ {r} by A6,A13;
then
A20: F.(i+m) c= F.((i+m)+1) by XBOOLE_1:7;
assume F.i c= F.(i+m);
hence thesis by A20,XBOOLE_1:1;
end;
A21: P[ 0 ];
A22: for m being Nat holds P[m] from NAT_1:sch 2(A21, A19);
thus thesis by A18,A22;
end;
A23: for i being Element of NAT holds f.i <> 0.PR
proof
let i be Element of NAT;
consider n being Element of NAT, A,B being non empty Subset of cPR
such that
A24: A = F.n and
A25: B = I\(A-Ideal) and
n = i and
F.(n+1) = F.n \/ {f.i} and
A26: f.i in minlen(B) by A16;
F.n c= A-Ideal by A24,IDEAL_1:def 14;
then
A27: not f.i in F.n by A25,A26,XBOOLE_0:def 5;
F.0 c=F.n & 0.PR in F.0 by A6,A17,TARSKI:def 1;
hence thesis by A27;
end;
A28: now
let i be Element of NAT, fi be Polynomial of R;
assume fi = f.i;
then fi <> 0.PR by A23;
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;
end;
defpred P3[set,set] means ex n being Element of NAT, A being Polynomial
of R st n = $1 & A = f.n & $2 = A.(len A -' 1);
A29: now
let x be Element of NAT;
reconsider fx=f.x as Polynomial of R by POLYNOM3:def 10;
fx.(len fx -' 1) is Element of cR;
hence ex y being Element of cR st P3[x,y];
end;
consider a being sequence of cR such that
A30: for x being Element of NAT holds P3[x,a.x] from FUNCT_2:sch 3(
A29);
reconsider a as sequence of R;
for B being non empty Subset of cR ex C being non empty finite
Subset of cR st C c= B & C-Ideal = B-Ideal by IDEAL_1:96;
then consider m being Element of NAT such that
A31: 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 P4[object,object] means
(ex u,v,w being Element of cR st $1 = u*v*w &
v in rng (a|Segm(m+1))) implies ex x,y,z being Element of cPR, p being
Polynomial of R st $2 = p & p = (x*y)*z & $1 = p.(len fm1 -' 1) & len p <= len
fm1 & y in F.(m+1);
A32: ex n being Element of NAT, A,B being non empty Subset of cPR 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 A16;
A33: for i,j being Element of NAT, 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, fi, fj be Polynomial of R;
assume that
A34: i <= j and
A35: fi = f.i and
A36: fj = f.j;
consider k being Nat such that
A37: j = i + k by A34,NAT_1:10;
defpred P[Nat] means for fk being Polynomial of R st fk=f.(
i+$1) holds len fi <= len fk;
A38: now
let k be Nat;
assume
A39: P[k];
now
reconsider fk = f.(i+k) as Polynomial of R by POLYNOM3:def 10;
let fk1 be Polynomial of R;
A40: len fi <= len fk by A39;
consider n being Element of NAT, A,B being non empty Subset of cPR
such that
A41: A = F.n and
A42: B = I\(A-Ideal) and
A43: n = i+k and
F.(n+1) = F.n \/ {f.(i+k)} and
A44: f.(i+k) in minlen(B) by A16;
consider n9 being Element of NAT, A9,B9 being non empty Subset of
cPR such that
A45: A9 = F.n9 and
A46: B9 = I\(A9-Ideal) and
A47: n9 = i+(k+1) and
F.(n9+1) = F.n9 \/ {f.(i+(k+1))} and
A48: f.(i+(k+1)) in minlen(B9) by A16;
A49: f.(i+(k+1)) in I by A46,A48,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 A17,A41,A43,A45,A47,IDEAL_1:57;
then not f.(i+(k+1)) in A-Ideal by A46,A48,XBOOLE_0:def 5;
then
A50: f.(i+(k+1)) in B by A42,A49,XBOOLE_0:def 5;
assume fk1=f.(i+(k+1));
then len fk <= len fk1 by A44,A50,Th17;
hence len fi <= len fk1 by A40,XXREAL_0:2;
end;
hence P[k+1];
end;
A51: P[ 0 ] by A35;
A52: for k being Nat holds P[k] from NAT_1:sch 2(A51, A38);
thus thesis by A36,A37,A52;
end;
A53: for e being object st e in cR
ex d being object st d in cPR & P4[e,d]
proof
let e be object;
assume e in cR;
per cases;
suppose
ex u,v,w being Element of cR st e= u*v*w & v in rng (a|Segm
(m+ 1 ) );
then consider u,b9,w being Element of cR such that
A54: e = u*b9*w and
A55: b9 in rng (a|Segm(m+1));
consider n being object such that
A56: n in dom (a|Segm(m+1)) and
A57: b9 = (a|Segm(m+1)).n by A55,FUNCT_1:def 3;
set c9 = w;
set a9 = u;
set z9 = monomial(c9,0);
A58: len fm1 -' 1 = (len fm1 -' 1) + 0;
reconsider n as Element of NAT by A56;
set y = f.n;
reconsider y9=y as Polynomial of R by POLYNOM3:def 10;
set x9 = monomial(a9,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
A59: n < m+1 by A56,NAT_1:44;
then len y9 <= len fm1 by A33;
then len y9 - len y9 <= len fm1 - len y9 by XREAL_1:9;
then
A60: len fm1 -' len y9 = len fm1 - len y9 by XREAL_0:def 2;
then len x9 <= len fm1 - len y9 +1 by Th18;
then
A61: len x9 + (len y9-1) <= len fm1-(len y9-1)+(len y9-1) by XREAL_1:6;
A62: len (x9*'y9) <= len x9 + len y9 -' 1 by Th21;
A63: len y9 -1 >= 0 by A28;
then 0+0 <= (len y9 - 1)+len x9;
then len (x9*'y9) <= len x9 + len y9 - 1 by A62,XREAL_0:def 2;
then
A64: len (x9*'y9) <= len fm1 by A61,XXREAL_0:2;
len fm1 - 1 >= 0 by A28;
then
A65: len fm1 -' 1 = (len fm1 - len y9) + (len y9 -1) by XREAL_0:def 2
.= (len y9 -' 1) + (len fm1 -' len y9) by A60,A63,XREAL_0:def 2;
reconsider x=x9,z=z9 as Element of cPR by POLYNOM3:def 10;
set p = (x*y)*z;
A66: x*y = x9*'y9 by POLYNOM3:def 10;
then
A67: p = (x9*'y9)*'z9 by POLYNOM3:def 10;
reconsider p as Polynomial of R by POLYNOM3:def 10;
A68: ex n9 being Element of NAT, A being Polynomial of R st n9 = n &
A = f.n9 & a.n = A.(len A -' 1) by A30;
b9 = a.n by A56,A57,FUNCT_1:47;
then (x9*'y9).(len fm1 -'1) = a9 * b9 by A68,A65,Th19;
then
A69: (a9*b9)*c9 = p.(len fm1 -' 1) by A67,A58,Th20;
ex n9 being Element of NAT, A,B being non empty Subset of cPR
st A = F.n9 & B = I\(A-Ideal) & n9 = n & F.(n9+1) = F.n9 \/ {f.n} & f .n in
minlen(B) by A16;
then {y} c= F.(n+1) by XBOOLE_1:7;
then
A70: y in F.(n+1) by ZFMISC_1:31;
len z9 <= 0+1 by Th18;
then len (x9*'y9) + len z9 <= len fm1 + 1 by A64,XREAL_1:7;
then
A71: len(x9*'y9)+len z9-'1 <= len fm1+1-'1 by NAT_D:42;
len ((x9*'y9)*'z9) <= len (x9*'y9) + len z9 -' 1 by Th21;
then len ((x9*'y9)*'z9) <= len fm1 +1 -' 1 by A71,XXREAL_0:2;
then len ((x9*'y9)*'z9) <= len fm1 +1 -1 by XREAL_0:def 2;
then
A72: len p <= len fm1+0 by A66,POLYNOM3:def 10;
n+1 <= m+1 by A59,NAT_1:13;
then F.(n+1) c= F.(m+1) by A17;
hence thesis by A54,A69,A72,A70;
end;
suppose
not ex u,v,w being Element of cR st e= u*v*w & v in rng (a
|Segm(m+1));
hence thesis;
end;
end;
consider LCT being Function of cR, cPR such that
A73: for e being object st e in cR holds P4[e,LCT.e] from FUNCT_2:sch
1 (A53 );
reconsider FM1 = F.(m+1) as non empty Subset of cPR by A13;
set raSm1 = rng(a|Segm(m+1));
consider lc being LinearCombination of rng (a|Segm(m+1)) such that
A74: a.(m+1) = Sum lc by A31,IDEAL_1:60;
A75: for lc being LinearCombination of raSm1 ex LC being
LinearCombination of FM1 st LC = LCT * lc & len lc = len LC
proof
let lc be LinearCombination of raSm1;
set LC = LCT * lc;
dom LCT = cR by FUNCT_2:def 1;
then rng lc c= dom LCT;
then
A76: dom lc = dom (LCT*lc) by RELAT_1:27;
then
A77: len lc = len LC by FINSEQ_3:29;
LC is LinearCombination of FM1
proof
let i be set such that
A78: i in dom LC;
consider u,v being Element of R, a being Element of raSm1 such that
A79: lc/.i = u*a*v by A76,A78,IDEAL_1:def 8;
A80: lc/.i = lc.i by A76,A78,PARTFUN1:def 6;
consider x,y,z being Element of cPR, p being Polynomial of R such
that
A81: LCT.(lc/.i) = p & p = (x*y)*z and
(u*a)*v = p.(len fm1 -' 1) and
len p <= len fm1 and
A82: y in F.(m+1) by A73,A79;
reconsider y as Element of FM1 by A82;
reconsider x, z as Element of PR;
LC/.i = (LCT*lc).i by A78,PARTFUN1:def 6
.= x*y*z by A76,A78,A80,A81,FUNCT_1:13;
hence
ex x,z being Element of PR, y being Element of FM1 st LC/.i = x *y*z;
end;
then reconsider LC as LinearCombination of FM1;
LC = LC;
hence thesis by A77;
end;
for lc being LinearCombination of raSm1 ex LC being
LinearCombination of FM1, 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 (raSm1);
defpred P5[Nat] means for lc being LinearCombination of
raSm1 st len lc <= $1 holds ex LC being LinearCombination of FM1, sLC being
Polynomial of R st LC = LCT*lc & sLC = Sum LC & sLC.(len fm1 -' 1) = Sum lc &
len sLC <= len fm1;
A83: ex n being Element of NAT st n = len lc;
A84: for k being Nat st P5[k] holds P5[k+1]
proof
let k be Nat;
assume
A85: P5[k];
thus P5[k+1]
proof
let lc be LinearCombination of (raSm1);
assume
A86: len lc <= k+1;
per cases;
suppose
len lc <= k;
hence thesis by A85;
end;
suppose
A87: len lc > k;
then len lc >= k+1 by NAT_1:13;
then
A88: len lc = k+1 by A86,XXREAL_0:1;
thus thesis
proof
per cases;
suppose
A89: k = 0;
then dom lc = {1} by A88,FINSEQ_1:2,def 3;
then
A90: 1 in dom lc by TARSKI:def 1;
then consider
u,w being Element of R, v being Element of raSm1
such that
A91: lc/.1 = u*v*w by IDEAL_1:def 8;
A92: lc.1 = lc/.1 by A90,PARTFUN1:def 6;
then consider
x,y,z being Element of cPR, p being Polynomial of R
such that
A93: LCT.(lc.1) = p and
p = (x*y)*z and
A94: (u*v)*w = p.(len fm1 -' 1) and
A95: len p <= len fm1 and
y in F.(m+1) by A73,A91;
A96: lc = <*lc.1*> by A88,A89,FINSEQ_1:40;
then
A97: Sum lc = p.(len fm1 -' 1) by A91,A92,A94,RLVECT_1:44;
consider LC being LinearCombination of FM1 such that
A98: LC = LCT*lc and
len LC = len lc by A75;
LC = <* LCT.(u*v*w) *> by A96,A91,A92,A98,FINSEQ_2:35;
then Sum LC = p by A91,A92,A93,RLVECT_1:44;
hence thesis by A95,A98,A97;
end;
suppose
A99: k > 0;
consider LC being LinearCombination of FM1 such that
A100: LC = LCT*lc and
len LC = len lc by A75;
lc is non empty by A87;
then consider
p being LinearCombination of raSm1, e being Element
of cR such that
A101: lc = p^<*e*> and
A102: <*e*> is LinearCombination of raSm1 by IDEAL_1:32;
len <* e *> = 0+1 by FINSEQ_1:39;
then len <*e*> <= k by A99,NAT_1:13;
then consider LCe being LinearCombination of FM1, sLCe being
Polynomial of R such that
A103: LCe = LCT*<*e*> and
A104: sLCe = Sum LCe and
A105: sLCe.(len fm1 -' 1) = Sum <* e *> and
A106: len sLCe <= len fm1 by A85,A102;
len lc = len p + len <* e *> by A101,FINSEQ_1:22
.= len p + 1 by FINSEQ_1:39;
then consider LCp being LinearCombination of FM1, sLCp being
Polynomial of R such that
A107: LCp = LCT*p and
A108: sLCp = Sum LCp and
A109: sLCp.(len fm1 -' 1) = Sum p and
A110: len sLCp <= len fm1 by A85,A88;
set sLC = sLCp + sLCe;
A111: Sum lc = Sum p + e by A101,FVSUM_1:71
.= sLCp.(len fm1 -' 1) + sLCe.(len fm1 -' 1) by A109,A105,
RLVECT_1:44
.= sLC.(len fm1 -' 1) by NORMSP_1:def 2;
A112: now
per cases;
suppose
len sLCp < len sLCe;
then len sLC <= len sLCe by POLYNOM4:6;
hence len sLC <= len fm1 by A106,XXREAL_0:2;
end;
suppose
len sLCp >= len sLCe;
then len sLC <= len sLCp by POLYNOM4:6;
hence len sLC <= len fm1 by A110,XXREAL_0:2;
end;
end;
dom LCT = cR 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 A101,A107,A103,A100,RLVECT_1:41
.= sLC by A108,A104,POLYNOM3:def 10;
hence thesis by A100,A111,A112;
end;
end;
end;
end;
end;
A113: P5 [ 0]
proof
let lc be LinearCombination of (raSm1);
assume
A114: len lc <= 0;
then
A115: lc = <*>cR;
consider LC being LinearCombination of FM1 such that
A116: LC = LCT * lc and
A117: len lc = len LC by A75;
take LC, p = 0_.(R);
thus LC = LCT * lc by A116;
LC = <*>cPR by A114,A117;
then Sum LC = 0.PR by RLVECT_1:43
.= p by POLYNOM3:def 10;
hence p = Sum LC;
thus p.(len fm1 -' 1) = 0.R
.= Sum lc by A115,RLVECT_1:43;
thus thesis by POLYNOM4:3;
end;
for k being Nat holds P5[k] from NAT_1:sch 2(A113,
A84);
hence thesis by A83;
end;
then consider
LC being LinearCombination of FM1, sLC being Polynomial of R
such that
LC = LCT*lc and
A118: sLC = Sum LC and
A119: sLC.(len fm1 -' 1) = Sum lc and
A120: len sLC <= len fm1;
A121: sLC in FM1-Ideal by A118,IDEAL_1:60;
set f9=fm1-sLC;
A122: now
ex n being Element of NAT, A being Polynomial of R st n = m+1 & A
= f.n & a.(m+1) = A.(len A -' 1) by A30;
then
A123: f9.(len fm1 -' 1)= fm1.(len fm1 -' 1) - fm1.(len fm1 -' 1) by A74,A119,
POLYNOM3:27
.= 0.R by RLVECT_1:15;
len fm1 - 1 >= 0 by A28;
then
A124: (len fm1 -' 1) + 1 = (len fm1 - 1) + 1 by XREAL_0:def 2
.= len fm1;
assume len f9 = len fm1;
hence contradiction by A124,A123,ALGSEQ_1:10;
end;
A125: f9+sLC = fm1+(sLC+(-sLC)) by POLYNOM3:26
.= fm1+(sLC-sLC)
.= fm1+0_.R by POLYNOM3:29
.= fm1 by POLYNOM3:28;
A126: now
reconsider sLC as Element of cPR by POLYNOM3:def 10;
assume
A127: f9 in FM1-Ideal;
reconsider f9 as Element of cPR by POLYNOM3:def 10;
f.(m+1) = f9+sLC by A125,POLYNOM3:def 10;
then fm1 in FM1-Ideal by A121,A127,IDEAL_1:def 1;
hence contradiction by A32,XBOOLE_0:def 5;
end;
len (-sLC) <= len fm1 by A120,POLYNOM4:8;
then len f9 <= len fm1 by POLYNOM4:6;
then
A128: len f9 < len fm1 by A122,XXREAL_0:1;
f9 in I
proof
reconsider f9 as Element of cPR by POLYNOM3:def 10;
reconsider sLC as Element of cPR by POLYNOM3:def 10;
FM1 is Subset of I by A13;
then FM1-Ideal c= I-Ideal by IDEAL_1:57;
then
A129: FM1-Ideal c= I by IDEAL_1:44;
f.(m+1) in I & f9=f.(m+1)-sLC by A32,Th16,XBOOLE_0:def 5;
hence thesis by A121,A129,IDEAL_1:15;
end;
then f9 in I\(FM1-Ideal) by A126,XBOOLE_0:def 5;
hence contradiction by A128,A32,Th17;
end;
hence thesis;
end;
end;
theorem Th32:
for R being Abelian add-associative right_zeroed
right_complementable associative distributive well-unital
commutative non trivial doubleLoopStr st R is Noetherian
for n being Nat holds Polynom-Ring (n,R) is Noetherian
proof
let R be Abelian add-associative right_zeroed right_complementable
associative distributive well-unital commutative non trivial
doubleLoopStr;
assume
A1: R is Noetherian;
defpred P[Nat] means Polynom-Ring($1,R) is Noetherian;
A2: now
let k be Nat such that
A3: P[k];
ex P being Function of Polynom-Ring(Polynom-Ring(k,R)), Polynom-Ring(k+
1,R) st P is RingIsomorphism by Th31;
hence P[k+1] by A3,Th27;
end;
ex P being Function of R, Polynom-Ring (0,R) st P is RingIsomorphism by Th28;
then
A4: P[ 0 ] by A1,Th27;
thus for n being Nat holds P[n] from NAT_1:sch 2(A4, A2);
end;
theorem Th33:
for F being Field holds F is Noetherian
proof
let F be Field;
let I be Ideal of F;
per cases by IDEAL_1:22;
suppose
A1: I = {0.F};
reconsider s0F = {0.F} as finite non empty Subset of F;
{0.F} = s0F-Ideal by IDEAL_1:47;
hence thesis by A1;
end;
suppose
A2: I = the carrier of F;
reconsider s1F = {1_F} as finite non empty Subset of F;
the carrier of F = s1F-Ideal by IDEAL_1:51;
hence thesis by A2;
end;
end;
theorem
for F being Field, n being Element of NAT holds Polynom-Ring (n,F) is
Noetherian
proof
let F be Field, n be Element of NAT;
F is Noetherian by Th33;
hence thesis by Th32;
end;
theorem
for R being Abelian right_zeroed add-associative right_complementable
well-unital distributive associative commutative non trivial
doubleLoopStr, X be infinite Ordinal holds Polynom-Ring (X,R) is non
Noetherian
proof
deffunc F(set)=$1;
let R be Abelian right_zeroed add-associative right_complementable
well-unital distributive associative commutative non trivial
doubleLoopStr, X be infinite Ordinal such that
A1: Polynom-Ring (X,R) is Noetherian;
reconsider f0 = X --> 0.R as Function of X,the carrier of R;
deffunc G(Element of X)=1_1($1,R);
set tcR = the carrier of R;
A2: for d1,d2 being Element of X st G(d1)=G(d2) holds d1=d2 by Th14;
tcR c= tcR;
then reconsider cR = the carrier of R as non empty Subset of tcR;
set S = {1_1(n, R) where n is Element of X : n in NAT};
set tcPR = the carrier of Polynom-Ring(X,R);
A3: NAT c= X by CARD_3:85;
reconsider 0X = 0 as Element of X by A3;
A4: S c= tcPR
proof
let x be object;
assume x in S;
then ex n being Element of X st x = 1_1(n,R) & n in NAT;
hence thesis by POLYNOM1:def 11;
end;
1_1(0X,R) in S;
then reconsider S as non empty Subset of tcPR by A4;
consider C being non empty finite Subset of tcPR such that
A5: C c= S and
A6: C-Ideal = S-Ideal by A1,IDEAL_1:96;
set CN = { F(n) where n is Element of X : G(n) in C };
A7: C is finite;
A8: CN is finite from FUNCT_7:sch 2(A7,A2);
A9: CN c= NAT
proof
let x be object;
assume x in CN;
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 thesis by A10,Th14;
end;
set c = the Element of C;
c in S by A5;
then consider cn being Element of X such that
A12: c = 1_1(cn,R) and
A13: cn in NAT;
reconsider cn as Element of NAT by A13;
cn in CN by A12;
then reconsider CN as non empty finite Subset of NAT by A8,A9;
reconsider mm = max CN as Element of NAT by ORDINAL1:def 12;
reconsider m1 = mm+1 as Element of NAT;
reconsider m2 = m1 as Element of X by A3;
1_1(m2,R) in S & S c= S-Ideal by IDEAL_1:def 14;
then consider lc being LinearCombination of C such that
A14: 1_1(m2,R) = Sum lc by A6,IDEAL_1:60;
reconsider ev = f0+*(m2,1_R) as Function of X, R;
consider E be FinSequence of [:tcPR, tcPR, tcPR:] such that
A15: E represents lc by IDEAL_1:35;
set P = Polynom-Evaluation(X, R, ev);
deffunc F(Nat)=(P.((E/.$1)`1_3))*(P.((E/.$1)`2_3))*(P.((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 = F(k) from FINSEQ_2:sch
1;
now
let i being set;
assume
A18: i in dom LC;
then reconsider k = i as Element of NAT;
reconsider a = (P.((E/.k)`2_3)) as Element of cR;
reconsider u=(P.((E/.k)`1_3)), v=(P.((E/.k)`3_3)) as Element of R;
take u, v, a;
thus LC/.i = LC.k by A18,PARTFUN1:def 6
.= u*a*v by A17,A18;
end;
then reconsider LC as LinearCombination of cR by IDEAL_1:def 8;
A19: now
let i be Element of NAT;
A20: now
assume m2 in CN;
then (max CN)+1 <= max CN by XXREAL_2:def 8;
hence contradiction by XREAL_1:29;
end;
assume
A21: i in dom LC;
then i in dom lc by A16,FINSEQ_3:29;
then reconsider y = (E/.i)`2_3 as Element of C by A15;
y in S by A5;
then consider n being Element of X such that
A22: y = 1_1(n, R) and
n in NAT;
n in CN by A22;
then
A23: ev.n = (X --> 0.R).n by A20,FUNCT_7:32
.= 0.R;
A24: Support(1_1(n,R)) = {UnitBag n} by Th13;
A25: P.1_1(n,R) = eval(1_1(n,R), ev) by POLYNOM2:def 5
.= (1_1(n,R).UnitBag n)*eval(UnitBag n,ev) by A24,POLYNOM2:19
.= 1_R *eval(UnitBag n,ev) by Th12
.= 1_R * ev.n by Th11
.= 0.R by A23;
thus LC.i = (P.((E/.i)`1_3))*(P.((E/.i)`2_3))*(P.((E/.i)`3_3))
by A17,A21
.= 0.R*(P.((E/.i)`3_3)) by A22,A25
.= 0.R;
end;
dom (X --> 0.R) = X;
then
A26: ev.m2 = 1_R by FUNCT_7:31;
A27: Support(1_1(m2,R)) = {UnitBag m2} by Th13;
A28: Polynom-Evaluation(X, R, ev).1_1(m2,R) = eval(1_1(m2,R), ev) by
POLYNOM2:def 5
.= (1_1(m2,R).UnitBag m2)*eval(UnitBag m2,ev) by A27,POLYNOM2:19
.= 1_R *eval(UnitBag m2,ev) by Th12
.= 1_R * ev.m2 by Th11
.= 1_R by A26;
for k being set st k in dom LC
holds LC.k = (P.((E/.k)`1_3))*(P.((E/.k)`2_3))*(P.((E/.k)`3_3)) by A17;
then P.(Sum lc) = Sum LC by A15,A16,Th24
.=0.R by A19,POLYNOM3:1;
hence contradiction by A14,A28;
end;