Copyright (c) 2003 Association of Mizar Users
environ
vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, RELAT_1, VECTSP_1, RLVECT_1,
ORDINAL1, LATTICES, ANPROJ_1, VECTSP_2, ALGSTR_1, ARYTM_1, REALSET1,
GROUP_1, BINOP_1, ARYTM_3, TERMORD, IDEAL_1, RELAT_2, DICKSON, MCART_1,
FINSEQ_1, FINSEQ_4, REWRITE1, BINOM, TARSKI, FINSET_1, PBOOLE, POLYRED,
CAT_3, SQUARE_1, ALGSEQ_1, BAGORDER, ORDERS_1, RFINSEQ, WAYBEL_4,
FINSEQ_7, GROEB_1, GROEB_2;
notation TARSKI, SUBSET_1, RELAT_1, XBOOLE_0, RELAT_2, RELSET_1, FUNCT_1,
ORDINAL1, ALGSTR_1, RLVECT_1, FINSEQ_4, FINSET_1, MCART_1, REALSET1,
FINSEQ_1, VECTSP_2, VECTSP_1, POLYNOM7, REAL_1, BINOM, PBOOLE, ORDERS_1,
POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, STRUCT_0, TERMORD, POLYRED,
GROUP_1, SQUARE_1, BINARITH, TOPREAL1, NUMBERS, XREAL_0, NAT_1, GROEB_1,
RFINSEQ, FINSEQ_7, WAYBEL_4;
constructors REWRITE1, REAL_1, IDEAL_1, TERMORD, POLYRED, CQC_LANG, TOPREAL1,
GROEB_1, FINSEQ_7, WELLFND1, WAYBEL_4, MONOID_0, MEMBERED, BINARITH,
BAGORDER;
clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, FINSEQ_1, VECTSP_2,
GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, NAT_1, INT_1, BINOM, POLYNOM7,
TERMORD, IDEAL_1, SUBSET_1, POLYRED, RFINSEQ, XBOOLE_0, MEMBERED,
NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems TARSKI, RELSET_1, FINSEQ_1, ZFMISC_1, VECTSP_1, POLYNOM1, REAL_1,
FINSEQ_4, RLVECT_1, NAT_1, MCART_1, POLYNOM7, REWRITE1, AXIOMS, XBOOLE_0,
IDEAL_1, TERMORD, INT_1, FUNCT_1, FINSET_1, XBOOLE_1, PBOOLE, BINARITH,
SEQM_3, VECTSP_2, POLYRED, SQUARE_1, FUNCT_2, BINOM, FINSEQ_3, RELAT_1,
RELAT_2, WAYBEL_4, BAGORDER, RFINSEQ, FINSEQ_5, XCMPLX_0, TOPREAL1,
ALGSTR_1, FINSEQ_7, GROEB_1, XCMPLX_1;
schemes NAT_1, FUNCT_1, BINOM;
begin :: Preliminaries
theorem
for X being set,
p being FinSequence of X
st p <> {} holds p|1 = <*p/.1*> by FINSEQ_5:23;
theorem Th2:
for L being non empty LoopStr,
p being FinSequence of L,
n,m being Nat
st m <= n holds (p|n)|m = p|m
proof
let L be non empty LoopStr,
p be FinSequence of L,
n,m be Nat;
assume A1: m <= n;
set q = p|n;
A2: dom q = dom(p|(Seg n)) by TOPREAL1:def 1
.= dom p /\ (Seg n) by FUNCT_1:68;
A3: Seg m c= Seg n by A1,FINSEQ_1:7;
A4: dom(q|m) = dom(q|(Seg m)) by TOPREAL1:def 1
.= (dom p /\ (Seg n)) /\ (Seg m) by A2,FUNCT_1:68
.= dom p /\ ((Seg n) /\ (Seg m)) by XBOOLE_1:16
.= dom p /\ (Seg m) by A3,XBOOLE_1:28
.= dom(p|(Seg m)) by FUNCT_1:68
.= dom(p|m) by TOPREAL1:def 1;
now let x be set;
assume A5: x in dom(p|m);
then reconsider x' = x as Nat;
A6: x' in dom(p|(Seg m)) by A5,TOPREAL1:def 1;
A7: x' in dom(q|(Seg m)) by A4,A5,TOPREAL1:def 1;
A8: (q|m).x' = (q|(Seg m)).x' by TOPREAL1:def 1
.= q.x' by A7,FUNCT_1:68;
x' in dom(p) /\ (Seg m) by A6,FUNCT_1:68;
then x' in dom p & x' in Seg m by XBOOLE_0:def 3;
then x' in dom(p) /\ (Seg n) by A3,XBOOLE_0:def 3;
then A9: x' in dom(p|(Seg n)) by FUNCT_1:68;
A10: q.x' = (p|(Seg n)).x' by TOPREAL1:def 1
.= p.x' by A9,FUNCT_1:68;
(p|m).x' = (p|(Seg m)).x' by TOPREAL1:def 1
.= p.x' by A6,FUNCT_1:68;
hence (p|m).x = (q|m).x by A8,A10;
end;
hence thesis by A4,FUNCT_1:9;
end;
theorem
for L being add-associative right_zeroed
right_complementable (non empty LoopStr),
p being FinSequence of L,
n being Nat
st for k being Nat st k in dom p & k > n holds p.k = 0.L
holds Sum p = Sum(p|n)
proof
let L be add-associative right_zeroed right_complementable
(non empty LoopStr),
p be FinSequence of L,
n be Nat;
assume A1: for k being Nat st k in dom p & k > n holds p.k = 0.L;
defpred P[Nat] means
for p being FinSequence of L,
n being Nat
st len p = $1 &
for k being Nat st k in dom p & k > n holds p.k = 0.L
holds Sum p = Sum(p|n);
A2: P[0]
proof let p be FinSequence of L,
n be Nat;
assume len p = 0 &
for k being Nat st k in dom p & k > n holds p.k = 0.L;
then len p <= n by NAT_1:18;
hence Sum p = Sum(p|n) by TOPREAL1:2;
end;
A3: now let k be Nat;
assume A4: P[k];
now let p be FinSequence of L,
n be Nat;
assume A5: len p = k+1 &
for l being Nat st l in dom p & l > n holds p.l = 0.L;
set q = p|(Seg k);
reconsider q as FinSequence of L by FINSEQ_1:23;
A6: dom p = Seg(k+1) by A5,FINSEQ_1:def 3;
A7: k <= len p by A5,NAT_1:29;
then A8: len q = k by FINSEQ_1:21;
A9: k <= k + 1 by NAT_1:29;
dom q = Seg(k) by A7,FINSEQ_1:21;
then A10: dom q c= dom p by A6,A9,FINSEQ_1:7;
A11: k + 1 in dom p by A6,FINSEQ_1:6;
then A12: q^<*p/.(k+1)*> = q^<*p.(k+1)*> by FINSEQ_4:def 4
.= p by A5,FINSEQ_3:61;
A13: q = p|k by TOPREAL1:def 1;
now per cases;
case k < n;
then A14: k + 1 <= n by NAT_1:38;
A15: dom(p|n) = dom(p|(Seg n)) by TOPREAL1:def 1;
A16: now let u be set;
assume u in dom(p|n);
then A17: u in dom(p|(Seg n)) by TOPREAL1:def 1;
dom(p|(Seg n)) c= dom p by FUNCT_1:76;
hence u in dom p by A17;
end;
now let u be set;
assume A18: u in dom p;
then A19: u in Seg(k+1) by A5,FINSEQ_1:def 3;
reconsider u' = u as Nat by A18;
1 <= u' & u' <= k + 1 by A19,FINSEQ_1:3;
then 1 <= u' & u' <= n by A14,AXIOMS:22;
then u' in Seg n by FINSEQ_1:3;
then u' in dom(p) /\ (Seg n) by A18,XBOOLE_0:def 3;
hence u in dom(p|n) by A15,FUNCT_1:68;
end;
then A20: dom(p|n) = dom p by A16,TARSKI:2;
for x being set st x in dom(p|(Seg n)) holds (p|(Seg n)).x = p.x
by FUNCT_1:68;
then p|(Seg n) = p by A15,A20,FUNCT_1:9;
hence Sum(p|n) = Sum p by TOPREAL1:def 1;
case A21: n <= k;
A22: now let l be Nat;
assume A23: l in dom q & l > n;
then A24: p.l = 0.L by A5,A10;
thus q.l = q/.l by A23,FINSEQ_4:def 4
.= p/.l by A13,A23,TOPREAL1:1
.= 0.L by A10,A23,A24,FINSEQ_4:def 4;
end;
k + 1 > n by A21,NAT_1:38;
then A25: 0.L = p.(k+1) by A5,A11
.= p/.(k+1) by A11,FINSEQ_4:def 4;
thus Sum p = Sum q + Sum(<*p/.(k+1)*>) by A12,RLVECT_1:58
.= Sum q + p/.(k+1) by RLVECT_1:61
.= Sum q by A25,RLVECT_1:def 7
.= Sum(q|n) by A4,A8,A22
.= Sum(p|n) by A13,A21,Th2;
end;
hence Sum p = Sum(p|n);
end;
hence P[k+1];
end;
A26: for k being Nat holds P[k] from Ind(A2,A3);
consider k being Nat such that A27: len p = k;
thus thesis by A1,A26,A27;
end;
theorem
for L being add-associative right_zeroed Abelian (non empty LoopStr),
f being FinSequence of L,
i,j being Nat
holds Sum Swap(f,i,j) = Sum f
proof
let L be add-associative right_zeroed Abelian (non empty LoopStr),
f be FinSequence of L,
i,j be Nat;
per cases;
suppose not(1 <= i & i <= len f & 1 <= j & j <= len f);
hence thesis by FINSEQ_7:def 2;
suppose A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
then i in Seg(len f) & j in Seg(len f) by FINSEQ_1:3;
then A2: i in dom f & j in dom f by FINSEQ_1:def 3;
now per cases by REAL_1:def 5;
case i = j;
hence thesis by FINSEQ_7:21;
case A3: i < j;
then Swap(f, i, j) =
(f|(i-'1))^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j) by A1,FINSEQ_7:29;
then A4: Sum(Swap(f, i, j))
= Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>)
+ Sum(f/^j) by RLVECT_1:58
.= (Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1)) + Sum(<*f/.i*>))
+ Sum(f/^j) by RLVECT_1:58
.= ((Sum(f|(i-'1)^<*f/.j*>) + Sum((f/^i)|(j-'i-'1))) + Sum(<*f/.i*>))
+ Sum(f/^j) by RLVECT_1:58
.= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum((f/^i)|(j-'i-'1)))
+ Sum(<*f/.i*>)) + Sum(f/^j) by RLVECT_1:58
.= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>))
+ Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 6
.= (((Sum(f|(i-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>))
+ Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 6
.= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum(<*f/.j*>))
+ Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:58
.= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum((f/^i)|(j-'i-'1)))
+ Sum(<*f/.j*>)) + Sum(f/^j) by RLVECT_1:def 6
.= (Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1)))
+ Sum(<*f/.j*>)) + Sum(f/^j) by RLVECT_1:58
.= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>))
+ Sum(f/^j) by RLVECT_1:58
.= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j))
by RLVECT_1:58;
(f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j)
= (f|(i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j)
by A2,FINSEQ_4:def 4
.= (f|(i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f.j*>)^(f/^j)
by A2,FINSEQ_4:def 4
.= f by A1,A3,FINSEQ_7:1;
hence thesis by A4;
case A5: i > j;
then Swap(f, j, i) =
(f|(j-'1))^<*f/.i*>^(f/^j)|(i-'j-'1)^<*f/.j*>^(f/^i) by A1,FINSEQ_7:29;
then A6: Sum(Swap(f, j, i))
= Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1)^<*f/.j*>)
+ Sum(f/^i) by RLVECT_1:58
.= (Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1)) + Sum(<*f/.j*>))
+ Sum(f/^i) by RLVECT_1:58
.= ((Sum(f|(j-'1)^<*f/.i*>) + Sum((f/^j)|(i-'j-'1))) + Sum(<*f/.j*>))
+ Sum(f/^i) by RLVECT_1:58
.= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum((f/^j)|(i-'j-'1)))
+ Sum(<*f/.j*>)) + Sum(f/^i) by RLVECT_1:58
.= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>))
+ Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 6
.= (((Sum(f|(j-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>))
+ Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 6
.= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum(<*f/.i*>))
+ Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:58
.= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum((f/^j)|(i-'j-'1)))
+ Sum(<*f/.i*>)) + Sum(f/^i) by RLVECT_1:def 6
.= (Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1)))
+ Sum(<*f/.i*>)) + Sum(f/^i) by RLVECT_1:58
.= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>))
+ Sum(f/^i) by RLVECT_1:58
.= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i))
by RLVECT_1:58;
(f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i)
= (f|(j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i)
by A2,FINSEQ_4:def 4
.= (f|(j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f.i*>)^(f/^i)
by A2,FINSEQ_4:def 4
.= f by A1,A5,FINSEQ_7:1;
hence thesis by A6,FINSEQ_7:23;
end;
hence thesis;
end;
theorem
for n being Ordinal,
T being TermOrder of n,
b1,b2,b3 being bag of n
st b1 <= b3,T & b2 <= b3,T holds max(b1,b2,T) <= b3,T by TERMORD:12;
theorem
for n being Ordinal,
T being TermOrder of n,
b1,b2,b3 being bag of n
st b3 <= b1,T & b3 <= b2,T holds b3 <= min(b1,b2,T),T by TERMORD:11;
definition
let X be set,
b1,b2 be bag of X;
assume A1:b2 divides b1;
func b1 / b2 -> bag of X means :Def1:
b2 + it = b1;
existence by A1,TERMORD:1;
uniqueness
proof
let b3,b4 be bag of X;
assume A2: b2 + b3 = b1;
assume A3: b2 + b4 = b1;
A4: dom b3 = X by PBOOLE:def 3 .= dom b4 by PBOOLE:def 3;
now let x be set;
assume x in dom b3;
thus b3.x = (b2.x + b3.x) -' b2.x by BINARITH:39
.= b1.x -' b2.x by A2,POLYNOM1:def 5
.= (b2.x + b4.x) -' b2.x by A3,POLYNOM1:def 5
.= b4.x by BINARITH:39;
end;
hence thesis by A4,FUNCT_1:9;
end;
end;
definition
::: exercise 5.45, p. 211
let X be set,
b1,b2 be bag of X;
func lcm(b1,b2) -> bag of X means :Def2:
for k being set holds it.k = max(b1.k,b2.k);
existence
proof
defpred Q[set,set] means $2 = max(b1.$1,b2.$1);
A1: for x,y1,y2 being set st x in X & Q[x,y1] & Q[x,y2]
holds y1 = y2;
A2: for x being set st x in X ex y being set st Q[x,y];
consider b being Function such that
A3: dom b = X & for x being set st x in X holds Q[x,b.x]
from FuncEx(A1,A2);
reconsider b as ManySortedSet of X by A3,PBOOLE:def 3;
now let u be set;
assume u in rng b;
then consider x being set such that
A4: x in dom b & u = b.x by FUNCT_1:def 5;
A5: u = max(b1.x,b2.x) by A3,A4;
b1.x in NAT & b2.x in NAT;
hence u in NAT by A5,SQUARE_1:49;
end;
then A6: rng b c= NAT by TARSKI:def 3;
now let u be set;
assume A7: u in support b;
then A8: b.u <> 0 by POLYNOM1:def 7;
A9: support b c= dom b by POLYNOM1:41;
now assume not(u in support(b1) \/ support(b2));
then not(u in support(b1)) & not(u in support(b2)) by XBOOLE_0:def 2;
then b1.u = 0 & b2.u = 0 by POLYNOM1:def 7;
then max(b1.u,b2.u) = 0;
hence contradiction by A3,A7,A8,A9;
end;
hence u in support(b1) \/ support(b2);
end;
then support b c= (support(b1) \/ support(b2)) by TARSKI:def 3;
then support b is finite by FINSET_1:13;
then reconsider b as bag of X by A6,POLYNOM1:def 8,SEQM_3:def 8;
A10: dom b = X by PBOOLE:def 3 .= dom b1 by PBOOLE:def 3;
A11: dom b = X by PBOOLE:def 3 .= dom b2 by PBOOLE:def 3;
take b;
now let k be set;
now per cases;
case k in dom b;
hence b.k = max(b1.k,b2.k) by A3;
case A12: not(k in dom b);
then b1.k = 0 & b2.k = 0 by A10,A11,FUNCT_1:def 4;
hence b.k = max(b1.k,b2.k) by A12,FUNCT_1:def 4;
end;
hence b.k = max(b1.k,b2.k);
end;
hence thesis;
end;
uniqueness
proof
let b3,b4 be bag of X;
assume A13: for k being set holds b3.k = max(b1.k,b2.k);
assume A14: for k being set holds b4.k = max(b1.k,b2.k);
A15: dom b3 = X by PBOOLE:def 3 .= dom b4 by PBOOLE:def 3;
now let u be set;
assume u in dom b3;
thus b3.u = max(b1.u,b2.u) by A13 .= b4.u by A14;
end;
hence thesis by A15,FUNCT_1:9;
end;
commutativity;
idempotence;
synonym b1 lcm b2;
end;
definition
let X be set,
b1,b2 be bag of X;
pred b1,b2 are_disjoint means :Def3:
for i being set holds b1.i = 0 or b2.i = 0;
antonym b1,b2 are_non_disjoint;
end;
theorem Th7:
::: exercise 5.45, p. 211
for X being set,
b1,b2 being bag of X
holds b1 divides lcm(b1,b2) & b2 divides lcm(b1,b2)
proof
let X be set,
b1,b2 be bag of X;
set bb = lcm(b1,b2);
now let k be set;
b1.k <= max(b1.k,b2.k) by SQUARE_1:46;
hence b1.k <= bb.k by Def2;
end;
hence b1 divides lcm(b1,b2) by POLYNOM1:def 13;
now let k be set;
b2.k <= max(b1.k,b2.k) by SQUARE_1:46;
hence b2.k <= bb.k by Def2;
end;
hence b2 divides lcm(b1,b2) by POLYNOM1:def 13;
end;
theorem Th8:
::: exercise 5.45, p. 211
for X being set,
b1,b2,b3 be bag of X
holds (b1 divides b3 & b2 divides b3) implies lcm(b1,b2) divides b3
proof
let X being set,
b1,b2,b3 be bag of X;
assume A1: b1 divides b3 & b2 divides b3;
now let k be set;
assume k in X;
now per cases by SQUARE_1:49;
case max(b1.k,b2.k) = b1.k;
hence max(b1.k,b2.k) <= b3.k by A1,POLYNOM1:def 13;
case max(b1.k,b2.k) = b2.k;
hence max(b1.k,b2.k) <= b3.k by A1,POLYNOM1:def 13;
end;
hence lcm(b1,b2).k <= b3.k by Def2;
end;
hence thesis by POLYNOM1:50;
end;
theorem
for X being set,
T being TermOrder of X,
b1,b2 being bag of X
holds b1,b2 are_disjoint iff lcm(b1,b2) = b1 + b2
proof
let X be set,
T be TermOrder of X,
b1,b2 be bag of X;
A1: now assume A2: b1,b2 are_disjoint;
now let k be set;
A3: 0 <= b1.k & 0 <= b2.k by NAT_1:18;
now per cases by A2,Def3;
case A4: b1.k = 0;
hence (b1+b2).k = 0 + b2.k by POLYNOM1:def 5
.= max(b1.k,b2.k) by A3,A4,SQUARE_1:def 2;
case A5: b2.k = 0;
hence (b1+b2).k = b1.k + 0 by POLYNOM1:def 5
.= max(b1.k,b2.k) by A3,A5,SQUARE_1:def 2;
end;
hence (b1+b2).k = max(b1.k,b2.k);
end;
hence lcm(b1,b2) = b1 + b2 by Def2;
end;
now assume A6: lcm(b1,b2) = b1 + b2;
now let k be set;
A7: lcm(b1,b2).k = max(b1.k,b2.k) by Def2;
now per cases by A6,A7,SQUARE_1:49;
case (b1 + b2).k = b1.k;
then b1.k + b2.k = b1.k + 0 by POLYNOM1:def 5;
hence b2.k = 0 by XCMPLX_1:2;
case (b1 + b2).k = b2.k;
then b1.k + b2.k = 0 + b2.k by POLYNOM1:def 5;
hence b1.k = 0 by XCMPLX_1:2;
end;
hence b1.k = 0 or b2.k = 0;
end;
hence b1,b2 are_disjoint by Def3;
end;
hence thesis by A1;
end;
theorem Th10:
for X being set,
b being bag of X
holds b/b = EmptyBag X
proof
let X be set,
b be bag of X;
b + EmptyBag X = b by POLYNOM1:57;
hence thesis by Def1;
end;
theorem Th11:
for X being set,
b1,b2 be bag of X
holds b2 divides b1 iff lcm(b1,b2) = b1
proof
let X being set,
b1,b2 be bag of X;
now assume A1: b2 divides b1;
now let k be set;
b2.k <= b1.k by A1,POLYNOM1:def 13;
hence b1.k = max(b1.k,b2.k) by SQUARE_1:def 2;
end;
hence lcm(b1,b2) = b1 by Def2;
end;
hence thesis by Th7;
end;
theorem
::: exercise 5.69 (i) ==> (ii), p. 223
for X being set,
b1,b2,b3 being bag of X
holds b1 divides lcm(b2,b3) implies lcm(b2,b1) divides lcm(b2,b3)
proof
let X being set,
b1,b2,b3 be bag of X;
assume A1: b1 divides lcm(b2,b3);
for k being set st k in X holds lcm(b2,b1).k <= lcm(b2,b3).k
proof
let k be set;
assume k in X;
b1.k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
then A2: b1.k <= max(b2.k,b3.k) by Def2;
b2.k <= max(b2.k,b3.k) by SQUARE_1:46;
then max(b2.k,b1.k) <= max(b2.k,b3.k) by A2,SQUARE_1:50;
then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
hence lcm(b2,b1).k <= lcm(b2,b3).k by Def2;
end;
hence thesis by POLYNOM1:50;
end;
theorem
::: exercise 5.69 (ii) ==> (iii), p. 223
for X being set,
b1,b2,b3 being bag of X
holds lcm(b2,b1) divides lcm(b2,b3) implies lcm(b1,b3) divides lcm(b2,b3)
proof
let X be set,
b1,b2,b3 be bag of X;
assume A1: lcm(b2,b1) divides lcm(b2,b3);
for k being set st k in X holds lcm(b1,b3).k <= lcm(b2,b3).k
proof
let k be set;
assume k in X;
lcm(b2,b1).k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
then A2: max(b2.k,b1.k) <= max(b2.k,b3.k) by Def2;
b1.k <= max(b2.k,b1.k) by SQUARE_1:46;
then A3: b1.k <= max(b2.k,b3.k) by A2,AXIOMS:22;
b3.k <= max(b2.k,b3.k) by SQUARE_1:46;
then max(b1.k,b3.k) <= max(b2.k,b3.k) by A3,SQUARE_1:50;
then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
hence lcm(b1,b3).k <= lcm(b2,b3).k by Def2;
end;
hence thesis by POLYNOM1:50;
end;
theorem
::: exercise 5.69 (iii) ==> (i), p. 223
for n being set,
b1,b2,b3 being bag of n
holds lcm(b1,b3) divides lcm(b2,b3) implies b1 divides lcm(b2,b3)
proof
let X be set,
b1,b2,b3 be bag of X;
assume A1: lcm(b1,b3) divides lcm(b2,b3);
for k being set st k in X holds b1.k <= lcm(b2,b3).k
proof
let k be set;
assume k in X;
lcm(b1,b3).k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
then A2: max(b1.k,b3.k) <= max(b2.k,b3.k) by Def2;
b1.k <= max(b1.k,b3.k) by SQUARE_1:46;
then b1.k <= max(b2.k,b3.k) by A2,AXIOMS:22;
hence b1.k <= lcm(b2,b3).k by Def2;
end;
hence thesis by POLYNOM1:50;
end;
theorem
for n being Nat,
T being connected admissible TermOrder of n,
P being non empty Subset of Bags n
ex b being bag of n
st b in P &
for b' being bag of n st b' in P holds b <= b',T
proof
let n be Nat,
T be connected admissible TermOrder of n,
P be non empty Subset of Bags n;
set R = RelStr(#Bags n, T#), m = MinElement(P,R);
A1: m in P & m is_minimal_wrt P,the InternalRel of R by BAGORDER:def 19;
m is Element of Bags n;
then reconsider b = m as bag of n;
A2: T is_connected_in field T by RELAT_2:def 14;
now let b' be bag of n;
assume A3: b' in P;
b <= b,T & b' <= b',T by TERMORD:6;
then [b,b] in T & [b',b'] in T by TERMORD:def 2;
then A4: b in field T & b' in field T by RELAT_1:30;
now per cases;
case b' = b;
hence b <= b',T by TERMORD:6;
case A5: b' <> b;
then not([b',b] in T) by A1,A3,WAYBEL_4:def 26;
then [b,b'] in T by A2,A4,A5,RELAT_2:def 6;
hence b <= b',T by TERMORD:def 2;
end;
hence b <= b',T;
end;
hence thesis by A1;
end;
definition
let L be add-associative right_zeroed right_complementable
(non trivial LoopStr),
a be non-zero Element of L;
cluster -a -> non-zero;
coherence
proof
A1: a <> 0.L by RLVECT_1:def 13;
now assume -a = 0.L;
then --a = 0.L by RLVECT_1:25;
hence contradiction by A1,RLVECT_1:30;
end;
hence thesis by RLVECT_1:def 13;
end;
end;
definition
let X be set,
L be left_zeroed right_zeroed add-cancelable
distributive (non empty doubleLoopStr),
m be Monomial of X,L,
a be Element of L;
cluster a * m -> monomial-like;
coherence
proof
set p = a * m;
now per cases by POLYNOM7:6;
case A1: Support m = {};
now assume A2: Support p <> {};
consider b being Element of Support p;
b in Support p by A2;
then reconsider b as Element of Bags X;
p.b = a * m.b by POLYNOM7:def 10
.= a * 0.L by A1,POLYNOM1:def 9
.= 0.L by BINOM:2;
hence contradiction by A2,POLYNOM1:def 9;
end;
hence thesis by POLYNOM7:6;
case ex b being bag of X st Support m = {b};
then consider b being bag of X such that
A3: Support m = {b};
reconsider b as Element of Bags X by POLYNOM1:def 14;
now per cases;
case A4: a = 0.L;
now assume A5: Support p <> {};
consider b being Element of Support p;
b in Support p by A5;
then reconsider b as Element of Bags X;
p.b = a * m.b by POLYNOM7:def 10
.= 0.L by A4,BINOM:1;
hence contradiction by A5,POLYNOM1:def 9;
end;
hence Support p = {};
case a <> 0.L;
A6: now let b' be Element of Bags X;
assume b' <> b;
then not(b' in Support m) by A3,TARSKI:def 1;
then A7: m.b' = 0.L by POLYNOM1:def 9;
p.b' = a * m.b' by POLYNOM7:def 10;
hence p.b' = 0.L by A7,BINOM:2;
end;
now per cases;
case A8: a * m.b = 0.L;
now assume A9: Support p <> {};
consider b' being Element of Support p;
b' in Support p by A9;
then reconsider b' as Element of Bags X;
A10: p.b' <> 0.L by A9,POLYNOM1:def 9;
then b' = b by A6;
hence contradiction by A8,A10,POLYNOM7:def 10;
end;
hence Support p = {};
case A11: a * m.b <> 0.L;
A12: now let u be set;
assume u in {b};
then A13: u = b by TARSKI:def 1;
p.b <> 0.L by A11,POLYNOM7:def 10;
hence u in Support p by A13,POLYNOM1:def 9;
end;
now let u be set;
assume A14: u in Support p;
then reconsider u' = u as Element of Bags X;
p.u' <> 0.L by A14,POLYNOM1:def 9;
then u' = b by A6;
hence u in {b} by TARSKI:def 1;
end;
hence Support p = {b} by A12,TARSKI:2;
end;
hence thesis by POLYNOM7:6;
end;
hence thesis by POLYNOM7:6;
end;
hence thesis;
end;
end;
definition
let n be Ordinal,
L be left_zeroed right_zeroed add-cancelable
distributive domRing-like (non trivial doubleLoopStr),
p be non-zero Polynomial of n,L,
a be non-zero Element of L;
cluster a * p -> non-zero;
coherence
proof
set ap = a * p;
p <> 0_(n,L) by POLYNOM7:def 2;
then A1: Support p <> {} by POLYNOM7:1;
consider b being Element of Support p;
b in Support p by A1;
then reconsider b as Element of Bags n;
A2: p.b <> 0.L by A1,POLYNOM1:def 9;
a <> 0.L by RLVECT_1:def 13;
then a * p.b <> 0.L by A2,VECTSP_2:def 5;
then ap.b <> 0.L by POLYNOM7:def 10;
then b in Support ap by POLYNOM1:def 9;
then ap <> 0_(n,L) by POLYNOM7:1;
hence thesis by POLYNOM7:def 2;
end;
end;
theorem Th16:
for n being Ordinal,
T being TermOrder of n,
L being right_zeroed right-distributive (non empty doubleLoopStr),
p,q being Series of n,L,
b being bag of n
holds b *' (p + q) = b *' p + b *' q
proof
let n be Ordinal,
T be TermOrder of n,
L be right_zeroed right-distributive (non empty doubleLoopStr),
p1,p2 be Series of n,L,
b be bag of n;
set q1 = b *' (p1 + p2), q2 = b *' p1 + b *' p2;
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
now let x be set;
assume x in dom q1;
then reconsider u = x as bag of n by POLYNOM1:def 14;
now per cases;
case A2: b divides u;
hence q1.u = (p1+p2).(u -' b) by POLYRED:def 1
.= p1.(u -' b) + p2.(u -' b) by POLYNOM1:def 21
.= (b*'p1).u + p2.(u -' b) by A2,POLYRED:def 1
.= (b*'p1).u + (b*'p2).u by A2,POLYRED:def 1
.= q2.u by POLYNOM1:def 21;
case A3: not(b divides u);
hence q1.u = 0.L by POLYRED:def 1
.= 0.L + 0.L by RLVECT_1:def 7
.= (b*'p1).u + 0.L by A3,POLYRED:def 1
.= (b*'p1).u + (b*'p2).u by A3,POLYRED:def 1
.= q2.u by POLYNOM1:def 21;
end;
hence q1.x = q2.x;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem Th17:
for n being Ordinal,
T being TermOrder of n,
L being add-associative right_zeroed right_complementable
(non empty LoopStr),
p being Series of n,L,
b being bag of n
holds b *' (-p) = -(b *' p)
proof
let n be Ordinal,
T be TermOrder of n,
L be add-associative right_zeroed right_complementable
(non empty LoopStr),
p be Series of n,L,
b be bag of n;
set q1 = b *' (-p), q2 = -(b *' p);
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
now let x be set;
assume x in dom q1;
then reconsider u = x as bag of n by POLYNOM1:def 14;
now per cases;
case A2: b divides u;
then A3: (b*'p).u = p.(u-'b) by POLYRED:def 1;
thus q1.u = (-p).(u-'b) by A2,POLYRED:def 1
.= -(p.(u-'b)) by POLYNOM1:def 22
.= (-(b*'p)).u by A3,POLYNOM1:def 22;
case A4: not(b divides u);
then A5: (b*'p).u = 0.L by POLYRED:def 1;
thus q1.u = 0.L by A4,POLYRED:def 1
.= -0.L by RLVECT_1:25
.= q2.u by A5,POLYNOM1:def 22;
end;
hence q1.x = q2.x;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem Th18:
for n being Ordinal,
T being TermOrder of n,
L being left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
p being Series of n,L,
b being bag of n,
a being Element of L
holds b *' (a * p) = a * (b *' p)
proof
let n be Ordinal,
T be TermOrder of n,
L be left_zeroed add-right-cancelable
right-distributive (non empty doubleLoopStr),
p be Series of n,L,
b be bag of n,
a be Element of L;
set q1 = b *' (a * p), q2 = a * (b *' p);
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
now let x be set;
assume x in dom q1;
then reconsider u = x as bag of n by POLYNOM1:def 14;
now per cases;
case A2: b divides u;
hence q1.u = (a*p).(u-'b) by POLYRED:def 1
.= a * p.(u-'b) by POLYNOM7:def 10
.= a * (b*'p).u by A2,POLYRED:def 1
.= q2.u by POLYNOM7:def 10;
case A3: not(b divides u);
hence q1.u = 0.L by POLYRED:def 1
.= a * 0.L by BINOM:2
.= a * (b*'p).u by A3,POLYRED:def 1
.= q2.u by POLYNOM7:def 10;
end;
hence q1.x = q2.x;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem Th19:
for n being Ordinal,
T being TermOrder of n,
L being right-distributive (non empty doubleLoopStr),
p,q being Series of n,L,
a being Element of L
holds a * (p + q) = a * p + a * q
proof
let n be Ordinal,
T be TermOrder of n,
L be right-distributive (non empty doubleLoopStr),
p1,p2 be Series of n,L,
b be Element of L;
set q1 = b * (p1 + p2), q2 = b * p1 + b * p2;
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
now let x be set;
assume x in dom q1;
then reconsider u = x as bag of n by POLYNOM1:def 14;
q1.u = b * (p1+p2).u by POLYNOM7:def 10
.= b * (p1.u + p2.u) by POLYNOM1:def 21
.= b * p1.u + b * p2.u by VECTSP_1:def 11
.= (b*p1).u + b * p2.u by POLYNOM7:def 10
.= (b*p1).u + (b*p2).u by POLYNOM7:def 10
.= (b*p1 + b*p2).u by POLYNOM1:def 21;
hence q1.x = q2.x;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem Th20:
for X being set,
L being add-associative right_zeroed right_complementable
(non empty doubleLoopStr),
a being Element of L
holds -(a _(X,L)) = (-a) _(X,L)
proof
let n be set,
L be add-associative right_zeroed right_complementable
(non empty doubleLoopStr),
a be Element of L;
A1: dom(- (a _(n,L))) = Bags n by FUNCT_2:def 1
.= dom((-a) _(n,L)) by FUNCT_2:def 1;
now let u be set;
assume u in dom((-a) _(n,L));
then reconsider u' = u as Element of Bags n;
now per cases;
case A2: u' = EmptyBag n;
hence -((a _(n,L)).u') = - a by POLYNOM7:18
.= ((-a) _(n,L)).u' by A2,POLYNOM7:18;
case A3: u' <> EmptyBag n;
-0.L = 0.L by RLVECT_1:25;
hence -((a _(n,L)).u') = 0.L by A3,POLYNOM7:18
.= ((-a) _(n,L)).u' by A3,POLYNOM7:18;
end;
hence ((-a) _(n,L)).u = (- (a _(n,L))).u by POLYNOM1:def 22;
end;
hence thesis by A1,FUNCT_1:9;
end;
Lm1:
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
f being Polynomial of n,L,
g being set,
P being Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,g implies g is Polynomial of n,L
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
f be Polynomial of n,L,
g be set,
P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume R reduces f,g;
then consider p being RedSequence of R such that
A1: p.1 = f & p.len p = g by REWRITE1:def 3;
len p > 0 by REWRITE1:def 2;
then A2: 1 <= len(p) by RLVECT_1:99;
then reconsider l = len p - 1 as Nat by INT_1:18;
A3: l + 1 = (len p + -1) + 1 by XCMPLX_0:def 8
.= len p + (-1 + 1) by XCMPLX_1:1
.= len p + 0;
then 1 <= l + 1 & l + 1 <= len p by NAT_1:37;
then l + 1 in Seg(len p) by FINSEQ_1:3;
then A4: l + 1 in dom p by FINSEQ_1:def 3;
set h = p.l;
per cases;
suppose len p = 1;
hence thesis by A1;
suppose len p <> 1;
then 1 < len p by A2,REAL_1:def 5;
then 1 + -1 < len p + -1 by REAL_1:67;
then 1 - 1 < len p - 1 by XCMPLX_0:def 8;
then 0 + 1 < l + 1 by REAL_1:67;
then 1 <= l & l <= l + 1 by NAT_1:38;
then l in Seg(len p) by A3,FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then [h,g] in R by A1,A3,A4,REWRITE1:def 2;
then consider h',g' being set such that
A5: [h,g] = [h',g'] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
g' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
g = [h',g']`2 by A5,MCART_1:def 2 .= g' by MCART_1:def 2;
hence g is Polynomial of n,L by A5,POLYNOM1:def 27;
end;
begin :: S-Polynomials
theorem Th21:
::: theorem 5.44, p. 210
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
P being Subset of Polynom-Ring(n,L) st not(0_(n,L) in P)
holds (for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P
for m1,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T)
holds PolyRedRel(P,T) reduces m1 *' p1 - m2 *' p2, 0_(n,L))
implies P is_Groebner_basis_wrt T
proof
let n be Nat,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
assume not(0_(n,L) in P);
assume A1: for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P
for m1,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T)
holds PolyRedRel(P,T) reduces m1 *' p1 - m2 *' p2, 0_(n,L);
set R = PolyRedRel(P,T);
now let a,b,c being set;
assume A2: [a,b] in R & [a,c] in R;
then consider f,f1 being set such that
A3: f in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
f1 in the carrier of Polynom-Ring(n,L) &
[a,b] = [f,f1] by ZFMISC_1:def 2;
reconsider f1 as Polynomial of n,L by A3,POLYNOM1:def 27;
A4: f in (the carrier of Polynom-Ring(n,L)) &
not(f in {0_(n,L)}) by A3,XBOOLE_0:def 4;
then reconsider f as Polynomial of n,L by POLYNOM1:def 27;
f <> 0_(n,L) by A4,TARSKI:def 1;
then reconsider f as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider f',f2 being set such that
A5: f' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
f2 in the carrier of Polynom-Ring(n,L) &
[a,c] = [f',f2] by A2,ZFMISC_1:def 2;
reconsider f2 as Polynomial of n,L by A5,POLYNOM1:def 27;
A6: f' = [a,c]`1 by A5,MCART_1:def 1
.= a by MCART_1:def 1
.= [f,f1]`1 by A3,MCART_1:def 1
.= f by MCART_1:def 1;
A7: f1 = [a,b]`2 by A3,MCART_1:def 2 .= b by MCART_1:def 2;
A8: f2 = [a,c]`2 by A5,MCART_1:def 2 .= c by MCART_1:def 2;
A9: f' = [a,c]`1 by A5,MCART_1:def 1 .= a by MCART_1:def 1;
A10: f reduces_to f1,P,T & f reduces_to f2,P,T
by A2,A3,A5,A6,POLYRED:def 13;
then consider g1 being Polynomial of n,L such that
A11: g1 in P & f reduces_to f1,g1,T by POLYRED:def 7;
consider b1 being bag of n such that
A12: f reduces_to f1,g1,b1,T by A11,POLYRED:def 6;
A13: g1 <> 0_(n,L) by A12,POLYRED:def 5;
then reconsider g1 as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider g2 being Polynomial of n,L such that
A14: g2 in P & f reduces_to f2,g2,T by A10,POLYRED:def 7;
consider b2 being bag of n such that
A15: f reduces_to f2,g2,b2,T by A14,POLYRED:def 6;
A16: g2 <> 0_(n,L) by A15,POLYRED:def 5;
then reconsider g2 as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider m1 being Monomial of n,L such that
A17: f1 = f - m1 *' g1 & not(HT(m1*'g1,T) in Support f1) &
HT(m1*'g1,T) <= HT(f,T),T by A11,GROEB_1:2;
consider m2 being Monomial of n,L such that
A18: f2 = f - m2 *' g2 & not(HT(m2*'g2,T) in Support f2) &
HT(m2*'g2,T) <= HT(f,T),T by A14,GROEB_1:2;
set mg1 = m1 *' g1, mg2 = m2 *' g2;
now per cases;
case m1 = 0_(n,L);
then f1 = f - 0_(n,L) by A17,POLYRED:5 .= f by POLYRED:4;
then R reduces b,c & R reduces c,c by A2,A6,A7,A9,REWRITE1:13,16;
hence b,c are_convergent_wrt R by REWRITE1:def 7;
case m2 = 0_(n,L);
then f2 = f - 0_(n,L) by A18,POLYRED:5 .= f by POLYRED:4;
then R reduces c,b & R reduces b,b by A2,A6,A8,A9,REWRITE1:13,16;
hence b,c are_convergent_wrt R by REWRITE1:def 7;
case m1 <> 0_(n,L) & m2 <> 0_(n,L);
then reconsider m1,m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
HT(m1,T) + HT(g1,T) in Support mg1 &
HT(m2,T) + HT(g2,T) in Support mg2 by TERMORD:29;
then A19: mg1 <> 0_(n,L) & mg2 <> 0_(n,L) by POLYNOM7:1;
A20: HC(g1,T) <> 0.L & HC(g2,T) <> 0.L by A13,A16,TERMORD:17;
A21: f2 - f1
= (f + -(m2 *' g2)) - (f - m1 *' g1) by A17,A18,POLYNOM1:def 23
.= (f + -(m2 *' g2)) - (f + -(m1 *' g1)) by POLYNOM1:def 23
.= (f + -(m2 *' g2)) + -(f + -(m1 *' g1)) by POLYNOM1:def 23
.= (f + -(m2 *' g2)) + (-f + --(m1 *' g1)) by POLYRED:1
.= f + (-(m2 *' g2) + (-f + (m1 *' g1))) by POLYNOM1:80
.= f + (-f + (-(m2 *' g2) + (m1 *' g1))) by POLYNOM1:80
.= (f + -f) + (-(m2 *' g2) + (m1 *' g1)) by POLYNOM1:80
.= 0_(n,L) + (-(m2 *' g2) + (m1 *' g1)) by POLYRED:3
.= (m1 *' g1) + -(m2 *' g2) by POLYRED:2
.= mg1 - mg2 by POLYNOM1:def 23;
PolyRedRel(P,T) reduces f2-f1,0_(n,L)
proof
now per cases;
case mg1 - mg2 = 0_(n,L);
hence thesis by A21,REWRITE1:13;
case A22: mg1 - mg2 <> 0_(n,L);
now per cases;
case g1 = g2;
then f2 - f1 = m1 *' g1 + -(m2 *' g1) by A21,POLYNOM1:def 23
.= g1 *' m1 + (-m2) *' g1 by POLYRED:6
.= (m1 + -m2) *' g1 by POLYNOM1:85;
hence thesis by A11,POLYRED:45;
case A23: g1 <> g2;
now per cases;
case A24: HT(mg1,T) <> HT(mg2,T);
now per cases;
case HT(mg2,T) < HT(mg1,T),T;
then not(HT(mg1,T) <= HT(mg2,T),T) by TERMORD:5;
then not(HT(mg1,T)) in Support(mg2) by TERMORD:def 6;
then A25: mg2.(HT(mg1,T)) = 0.L by POLYNOM1:def 9;
A26: (mg1-mg2).(HT(mg1,T))
= (mg1+-mg2).(HT(mg1,T)) by POLYNOM1:def 23
.= mg1.(HT(mg1,T))+(-mg2).(HT(mg1,T)) by POLYNOM1:def 21
.= mg1.(HT(mg1,T))+-(mg2).(HT(mg1,T)) by POLYNOM1:def 22
.= mg1.(HT(mg1,T))+0.L by A25,RLVECT_1:25
.= mg1.(HT(mg1,T)) by RLVECT_1:def 7
.= HC(mg1,T) by TERMORD:def 7;
then (mg1-mg2).(HT(mg1,T)) <> 0.L by A19,TERMORD:17;
then A27: HT(mg1,T) in Support(mg1 - mg2) by POLYNOM1:def 9;
A28: HT(m1,T) + HT(g1,T) = HT(mg1,T) by TERMORD:31;
(mg1 - mg2) -
((mg1-mg2).HT(mg1,T)/HC(g1,T)) * (HT(m1,T) *' g1)
= (mg1 - mg2) -
((HC(m1,T)*HC(g1,T))/HC(g1,T)) * (HT(m1,T) *' g1)
by A26,TERMORD:32
.= (mg1 - mg2) -
((HC(m1,T)*HC(g1,T))*(HC(g1,T)")) * (HT(m1,T) *' g1)
by VECTSP_1:def 23
.= (mg1 - mg2) -
(HC(m1,T)*(HC(g1,T)*(HC(g1,T)"))) * (HT(m1,T) *' g1)
by VECTSP_1:def 16
.= (mg1 - mg2) -
(HC(m1,T)*1_ L) * (HT(m1,T) *' g1) by A20,VECTSP_1:def 22
.= (mg1 - mg2) -
HC(m1,T) * (HT(m1,T) *' g1) by VECTSP_1:def 19
.= (mg1 - mg2) - Monom(HC(m1,T),HT(m1,T)) *' g1 by POLYRED:22
.= (mg1 - mg2) - Monom(coefficient(m1),HT(m1,T)) *'g1
by TERMORD:23
.= (mg1 - mg2) - Monom(coefficient(m1),term(m1)) *'g1
by TERMORD:23
.= (mg1 - mg2) - mg1 by POLYNOM7:11
.= (mg1+-mg2)-mg1 by POLYNOM1:def 23
.= (mg1+-mg2)+-mg1 by POLYNOM1:def 23
.= (mg1+-mg1)+-mg2 by POLYNOM1:80
.= 0_(n,L)+-mg2 by POLYRED:3
.= -mg2 by POLYRED:2;
then mg1-mg2 reduces_to -mg2,g1,HT(mg1,T),T
by A13,A22,A27,A28,POLYRED:def 5;
then mg1-mg2 reduces_to -mg2,g1,T by POLYRED:def 6;
then mg1-mg2 reduces_to -mg2,P,T by A11,POLYRED:def 7;
then [mg1-mg2,-mg2] in R by POLYRED:def 13;
then A29: R reduces mg1-mg2,-mg2 by REWRITE1:16;
R reduces (-m2)*'g2,0_(n,L) by A14,POLYRED:45;
then R reduces -mg2,0_(n,L) by POLYRED:6;
hence thesis by A21,A29,REWRITE1:17;
case not(HT(mg2,T) < HT(mg1,T),T);
then HT(mg1,T) <= HT(mg2,T),T by TERMORD:5;
then HT(mg1,T) < HT(mg2,T),T by A24,TERMORD:def 3;
then not(HT(mg2,T) <= HT(mg1,T),T) by TERMORD:5;
then not(HT(mg2,T)) in Support(mg1) by TERMORD:def 6;
then A30: mg1.(HT(mg2,T)) = 0.L by POLYNOM1:def 9;
A31: (mg2-mg1).(HT(mg2,T))
= (mg2+-mg1).(HT(mg2,T)) by POLYNOM1:def 23
.= mg2.(HT(mg2,T))+(-mg1).(HT(mg2,T)) by POLYNOM1:def 21
.= mg2.(HT(mg2,T))+-(mg1).(HT(mg2,T)) by POLYNOM1:def 22
.= mg2.(HT(mg2,T))+0.L by A30,RLVECT_1:25
.= mg2.(HT(mg2,T)) by RLVECT_1:def 7
.= HC(mg2,T) by TERMORD:def 7;
then (mg2-mg1).(HT(mg2,T)) <> 0.L by A19,TERMORD:17;
then A32: HT(mg2,T) in Support(mg2 - mg1) by POLYNOM1:def 9;
A33: HT(m2,T) + HT(g2,T) = HT(mg2,T) by TERMORD:31;
reconsider x = -0_(n,L)
as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider x as Element of Polynom-Ring(n,L);
0.Polynom-Ring(n,L) = 0_(n,L) by POLYNOM1:def 27;
then A34: x + (0.Polynom-Ring(n,L)) = -0_(n,L) + 0_(n,L)
by POLYNOM1:def 27
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
A35: now assume mg2 - mg1 = 0_(n,L);
then -(mg2 + -mg1) = - 0_(n,L) by POLYNOM1:def 23;
then -mg2 + -(-mg1) = -0_(n,L) by POLYRED:1;
then mg1 + -mg2
= -(0.(Polynom-Ring(n,L))) by A34,RLVECT_1:19
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:25
.= 0_(n,L) by POLYNOM1:def 27;
hence contradiction by A22,POLYNOM1:def 23;
end;
(mg2 - mg1) -
((mg2-mg1).HT(mg2,T)/HC(g2,T)) * (HT(m2,T) *' g2)
= (mg2 - mg1) -
((HC(m2,T)*HC(g2,T))/HC(g2,T)) * (HT(m2,T) *' g2)
by A31,TERMORD:32
.= (mg2 - mg1) -
((HC(m2,T)*HC(g2,T))*(HC(g2,T)")) * (HT(m2,T) *' g2)
by VECTSP_1:def 23
.= (mg2 - mg1) -
(HC(m2,T)*(HC(g2,T)*(HC(g2,T)"))) * (HT(m2,T) *' g2)
by VECTSP_1:def 16
.= (mg2 - mg1) -
(HC(m2,T)*1_ L) * (HT(m2,T) *' g2) by A20,VECTSP_1:def 22
.= (mg2 - mg1) -
HC(m2,T) * (HT(m2,T) *' g2) by VECTSP_1:def 19
.= (mg2 - mg1) - Monom(HC(m2,T),HT(m2,T)) *' g2 by POLYRED:22
.= (mg2 - mg1) - Monom(coefficient(m2),HT(m2,T)) *'g2
by TERMORD:23
.= (mg2 - mg1) - Monom(coefficient(m2),term(m2)) *'g2
by TERMORD:23
.= (mg2 - mg1) - mg2 by POLYNOM7:11
.= (mg2+-mg1)-mg2 by POLYNOM1:def 23
.= (mg2+-mg1)+-mg2 by POLYNOM1:def 23
.= (mg2+-mg2)+-mg1 by POLYNOM1:80
.= 0_(n,L)+-mg1 by POLYRED:3
.= -mg1 by POLYRED:2;
then mg2-mg1 reduces_to -mg1,g2,HT(mg2,T),T
by A16,A32,A33,A35,POLYRED:def 5;
then mg2-mg1 reduces_to -mg1,g2,T by POLYRED:def 6;
then mg2-mg1 reduces_to -mg1,P,T by A14,POLYRED:def 7;
then [mg2-mg1,-mg1] in R by POLYRED:def 13;
then A36: R reduces mg2-mg1,-mg1 by REWRITE1:16;
R reduces (-m1)*'g1,0_(n,L) by A11,POLYRED:45;
then R reduces -mg1,0_(n,L) by POLYRED:6;
then A37: R reduces mg2-mg1,0_(n,L) by A36,REWRITE1:17;
-(1_(n,L)) = -(1.L _(n,L)) by POLYNOM7:20
.= (-1.L) _(n,L) by Th20;
then A38: R reduces (-1_(n,L))*'(mg2-mg1),(-1_(n,L))*'0_(n,L)
by A37,POLYRED:47;
(-1_(n,L))*'(mg2-mg1)
= (-1_(n,L))*'(mg2+-mg1) by POLYNOM1:def 23
.= (-1_(n,L))*'mg2+(-1_(n,L))*'(-mg1) by POLYNOM1:85
.= -(1_(n,L)*'mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
.= 1_(n,L)*'(-mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
.= 1_(n,L)*'(-mg2)+(-(1_(n,L)*'(-mg1))) by POLYRED:6
.= 1_(n,L)*'(-mg2)+1_(n,L)*'(--mg1) by POLYRED:6
.= (-mg2)+1_(n,L)*'mg1 by POLYNOM1:89
.= mg1 + -mg2 by POLYNOM1:89
.= mg1 - mg2 by POLYNOM1:def 23;
hence thesis by A21,A38,POLYNOM1:87;
end;
hence thesis;
case A39: HT(mg1,T) = HT(mg2,T);
(f-mg1).HT(mg1,T) = 0.L by A17,POLYNOM1:def 9;
then (f+-mg1).HT(mg1,T) = 0.L by POLYNOM1:def 23;
then f.HT(mg1,T) + (-mg1).HT(mg1,T) = 0.L by POLYNOM1:def 21;
then f.HT(mg1,T) + -(mg1.HT(mg1,T)) = 0.L by POLYNOM1:def 22;
then A40: f.HT(mg1,T) = --(mg1.HT(mg1,T)) by RLVECT_1:19;
(f-mg2).HT(mg2,T) = 0.L by A18,POLYNOM1:def 9;
then (f+-mg2).HT(mg2,T) = 0.L by POLYNOM1:def 23;
then f.HT(mg2,T) + (-mg2).HT(mg2,T) = 0.L by POLYNOM1:def 21;
then f.HT(mg2,T) + -(mg2.HT(mg2,T)) = 0.L by POLYNOM1:def 22;
then A41: f.HT(mg2,T) = --(mg2.HT(mg2,T)) by RLVECT_1:19;
HC(mg1,T) = mg1.HT(mg1,T) by TERMORD:def 7
.= f.(HT(mg1,T)) by A40,RLVECT_1:30
.= mg2.HT(mg2,T) by A39,A41,RLVECT_1:30
.= HC(mg2,T) by TERMORD:def 7;
then HM(mg1,T) = Monom(HC(mg2,T),HT(mg2,T)) by A39,TERMORD:def 8
.= HM(mg2,T) by TERMORD:def 8;
hence thesis by A1,A11,A14,A21,A23;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
then f2,f1 are_convergent_wrt R by POLYRED:50;
hence b,c are_convergent_wrt R by A7,A8,REWRITE1:41;
end;
hence b,c are_convergent_wrt R;
end;
then PolyRedRel(P,T) is locally-confluent by REWRITE1:def 24;
hence thesis by GROEB_1:def 3;
end;
definition
::: definition 5.46, p. 211
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 be Polynomial of n,L;
func S-Poly(p1,p2,T) -> Polynomial of n,L equals :Def4:
HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1 -
HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
coherence;
end;
Lm2:
for L being add-associative left_zeroed right_zeroed add-cancelable
right_complementable associative distributive well-unital
(non empty doubleLoopStr),
P being Subset of L,
p being Element of L st p in P
holds p in P-Ideal
proof
let L be add-associative left_zeroed right_zeroed add-cancelable
associative distributive well-unital right_complementable
(non empty doubleLoopStr),
P be Subset of L,
p be Element of L;
assume A1: p in P;
then reconsider P' = P as non empty Subset of L;
set f = <*p*>;
now let i be set;
assume A2: i in dom f;
dom f = {1} by FINSEQ_1:4,55;
then i = 1 by A2,TARSKI:def 1;
then f/.i = f.1 by A2,FINSEQ_4:def 4
.= p by FINSEQ_1:57
.= 1_ L * p by VECTSP_1:def 19
.= 1_ L * p * 1_ L by VECTSP_1:def 13;
hence ex u,v being Element of L, a being Element of P' st f/.i = u*a*v by A1
;
end;
then reconsider f as LinearCombination of P' by IDEAL_1:def 9;
Sum f = p by RLVECT_1:61;
hence thesis by IDEAL_1:60;
end;
Lm3:
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
unital distributive (non trivial doubleLoopStr),
p,q being Polynomial of n,L,
f,g being Element of Polynom-Ring(n,L)
holds (f = p & g = q) implies f - g = p - q
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
unital distributive (non trivial doubleLoopStr),
p,q be Polynomial of n,L,
f,g be Element of Polynom-Ring(n,L);
assume A1: f = p & g = q;
reconsider x = -q as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider x as Element of Polynom-Ring(n,L);
x + g = -q + q by A1,POLYNOM1:def 27
.= 0_(n,L) by POLYRED:3
.= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then A2: -q = -g by RLVECT_1:19;
thus p - q = p + (-q) by POLYNOM1:def 23
.= f + (-g) by A1,A2,POLYNOM1:def 27
.= f - g by RLVECT_1:def 11;
end;
theorem Th22:
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like Abelian (non trivial doubleLoopStr),
P being Subset of Polynom-Ring(n,L),
p1,p2 being Polynomial of n,L st p1 in P & p2 in P
holds S-Poly(p1,p2,T) in P-Ideal
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like Abelian (non trivial doubleLoopStr),
P be Subset of Polynom-Ring(n,L),
p1,p2 be Polynomial of n,L;
assume A1: p1 in P & p2 in P;
set q = S-Poly(p1,p2,T);
reconsider p1' = p1, p2' = p2 as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider p1', p2' as Element of Polynom-Ring(n,L);
set q1 = Monom(HC(p2,T),lcm(HT(p1,T),HT(p2,T))/HT(p1,T)),
q2 = Monom(HC(p1,T),lcm(HT(p1,T),HT(p2,T))/HT(p2,T));
reconsider q1' = q1, q2' = q2 as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider q1', q2' as Element of Polynom-Ring(n,L);
A2: q = HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1 -
HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2 by Def4
.= q1 *' p1 - HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2
by POLYRED:22
.= q1 *' p1 - q2 *' p2 by POLYRED:22;
p1' in P-Ideal & p2' in P-Ideal by A1,Lm2;
then q1' * p1' in P-Ideal & q2' * p2' in P-Ideal by IDEAL_1:def 2;
then A3: q1' * p1' - q2' * p2' in P-Ideal by IDEAL_1:16;
q1 *' p1 = q1' * p1' & q2 *' p2 = q2' * p2' by POLYNOM1:def 27;
hence thesis by A2,A3,Lm3;
end;
theorem
::: exercise 5.47 (i), p. 211
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 being Polynomial of n,L
holds p1 = p2 implies S-Poly(p1,p2,T) = 0_(n,L)
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 be Polynomial of n,L;
assume p1 = p2;
then S-Poly(p1,p2,T) =
HC(p1,T) * (lcm(HT(p1,T),HT(p1,T))/HT(p1,T)) *' p1 -
HC(p1,T) * (lcm(HT(p1,T),HT(p1,T))/HT(p1,T)) *' p1 by Def4;
hence thesis by POLYNOM1:83;
end;
theorem Th24:
::: exercise 5.47 (i), p. 211
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
m1,m2 being Monomial of n,L
holds S-Poly(m1,m2,T) = 0_(n,L)
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
m1,m2 be Monomial of n,L;
per cases;
suppose A1: m1 = 0_(n,L);
A2: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))),T)
= coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))))
by TERMORD:23
.= HC(0_(n,L),T) by POLYNOM7:9
.= 0.L by TERMORD:17;
thus S-Poly(m1,m2,T)
= HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' 0_(n,L) -
HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by A1,Def4
.= Monom(HC(m2,T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' 0_(n,L) -
HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by POLYRED:22
.= 0_(n,L) -
HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by POLYNOM1:87
.= 0_(n,L) -
Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' m2
by POLYRED:22
.= 0_(n,L) - 0_(n,L) *' m2 by A2,TERMORD:17
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYNOM1:83;
suppose A3: m2 = 0_(n,L);
A4: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))),T)
= coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))))
by TERMORD:23
.= HC(0_(n,L),T) by POLYNOM7:9
.= 0.L by TERMORD:17;
thus S-Poly(m1,m2,T)
= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' 0_(n,L) by A3,Def4
.= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
Monom(HC(m1,T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' 0_(n,L)
by POLYRED:22
.= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
0_(n,L) by POLYNOM1:87
.= Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1 -
0_(n,L) by POLYRED:22
.= 0_(n,L) *' m1 - 0_(n,L) by A4,TERMORD:17
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYNOM1:83;
suppose m1 <> 0_(n,L) & m2 <> 0_(n,L);
then HC(m1,T) <> 0.L & HC(m2,T) <> 0.L by TERMORD:17;
then A5: HC(m1,T) is non-zero & HC(m2,T) is non-zero by RLVECT_1:def 13;
A6: m1 = Monom(coefficient(m1),term(m1)) by POLYNOM7:11
.= Monom(HC(m1,T),term(m1)) by TERMORD:23
.= Monom(HC(m1,T),HT(m1,T)) by TERMORD:23;
A7: m2 = Monom(coefficient(m2),term(m2)) by POLYNOM7:11
.= Monom(HC(m2,T),term(m2)) by TERMORD:23
.= Monom(HC(m2,T),HT(m2,T)) by TERMORD:23;
A8: HT(m1,T) divides lcm(HT(m1,T),HT(m2,T)) by Th7;
A9: HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1
= Monom(HC(m2,T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1
by POLYRED:22
.= Monom(HC(m2,T)*HC(m1,T),
(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))+HT(m1,T)) by A5,A6,TERMORD:3
.= Monom(HC(m2,T)*HC(m1,T),
lcm(HT(m1,T),HT(m2,T))) by A8,Def1;
A10: HT(m2,T) divides lcm(HT(m1,T),HT(m2,T)) by Th7;
A11: HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2
= Monom(HC(m1,T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' m2
by POLYRED:22
.= Monom(HC(m2,T)*HC(m1,T),
(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))+HT(m2,T)) by A5,A7,TERMORD:3
.= Monom(HC(m2,T)*HC(m1,T),
lcm(HT(m1,T),HT(m2,T))) by A10,Def1;
thus S-Poly(m1,m2,T)
= HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by Def4
.= 0_(n,L) by A9,A11,POLYNOM1:83;
end;
theorem Th25:
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p being Polynomial of n,L
holds S-Poly(p,0_(n,L),T) = 0_(n,L) & S-Poly(0_(n,L),p,T) = 0_(n,L)
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p be Polynomial of n,L;
set p2 = 0_(n,L);
thus S-Poly(p,0_(n,L),T)
= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p -
HC(p,T) * (lcm(HT(p,T),HT(p2,T))/HT(p2,T)) *' 0_(n,L) by Def4
.= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p -
Monom(HC(p,T),lcm(HT(p,T),HT(p2,T))/HT(p2,T)) *' 0_(n,L) by POLYRED:22
.= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p - 0_(n,L)
by POLYNOM1:87
.= 0.L * ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p) - 0_(n,L) by TERMORD:17
.= ((0.L _(n,L)) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L)
by POLYNOM7:27
.= (0_(n,L) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L)
by POLYNOM7:19
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYRED:4;
thus S-Poly(0_(n,L),p,T)
= HC(p,T) * (lcm(HT(p2,T),HT(p,T))/HT(p2,T)) *' 0_(n,L) -
HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by Def4
.= Monom(HC(p,T),(lcm(HT(p2,T),HT(p,T))/HT(p2,T))) *' 0_(n,L) -
HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by POLYRED:22
.= 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p
by POLYNOM1:87
.= 0_(n,L) - 0.L * ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p) by TERMORD:17
.= 0_(n,L) - ((0.L _(n,L)) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p))
by POLYNOM7:27
.= 0_(n,L) - (0_(n,L) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p))
by POLYNOM7:19
.= 0_(n,L) - 0_(n,L) by POLYRED:5
.= 0_(n,L) by POLYRED:4;
end;
theorem
::: exercise 5.47 (ii), p. 211
for n being Ordinal,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 being Polynomial of n,L
holds S-Poly(p1,p2,T) = 0_(n,L) or
HT(S-Poly(p1,p2,T),T) < lcm(HT(p1,T),HT(p2,T)),T
proof
let n be Ordinal,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 be Polynomial of n,L;
assume A1: S-Poly(p1,p2,T) <> 0_(n,L);
set sp = S-Poly(p1,p2,T),
g1 = HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1,
g2 = HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
per cases;
suppose p1 = 0_(n,L) or p2 = 0_(n,L);
hence thesis by A1,Th25;
suppose A2: p1 <> 0_(n,L) & p2 <> 0_(n,L);
then A3: HC(p1,T) <> 0.L & HC(p2,T) <> 0.L by TERMORD:17;
then A4: HC(p1,T) is non-zero & HC(p2,T) is non-zero by RLVECT_1:def 13;
A5: HT(p1,T) divides lcm(HT(p1,T),HT(p2,T)) by Th7;
A6: HT(p2,T) divides lcm(HT(p1,T),HT(p2,T)) by Th7;
A7: p1 is non-zero & p2 is non-zero by A2,POLYNOM7:def 2;
A8: HT(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T)
= term(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))))
by TERMORD:23
.= lcm(HT(p1,T),HT(p2,T))/HT(p1,T) by A4,POLYNOM7:10;
HC(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T)
= coefficient(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))))
by TERMORD:23
.= HC(p2,T) by POLYNOM7:9;
then Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) <> 0_(n,L)
by A3,TERMORD:17;
then A9: Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) is non-zero
by POLYNOM7:def 2;
A10: HT(g1,T)
= HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *' p1,T)
by POLYRED:22
.= HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) + HT(p1,T)
by A7,A9,TERMORD:31
.= lcm(HT(p1,T),HT(p2,T)) by A5,A8,Def1;
A11: HT(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T)
= term(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))))
by TERMORD:23
.= lcm(HT(p1,T),HT(p2,T))/HT(p2,T) by A4,POLYNOM7:10;
HC(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T)
= coefficient(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))))
by TERMORD:23
.= HC(p1,T) by POLYNOM7:9;
then Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) <> 0_(n,L)
by A3,TERMORD:17;
then A12: Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) is non-zero
by POLYNOM7:def 2;
A13: HT(g2,T)
= HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *' p2,T)
by POLYRED:22
.= HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) + HT(p2,T)
by A7,A12,TERMORD:31
.= lcm(HT(p1,T),HT(p2,T)) by A6,A11,Def1;
sp = g1 - g2 by Def4;
then HT(sp,T) <= max(HT(g1,T),HT(g2,T),T), T by GROEB_1:7;
then A14: HT(sp,T) <= lcm(HT(p1,T),HT(p2,T)),T by A10,A13,TERMORD:12;
A15: HC(g1,T)
= HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *' p1,T)
by POLYRED:22
.= HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) * HC(p1,T)
by A7,A9,TERMORD:32
.= coefficient(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) * HC(p1,T)
by TERMORD:23
.= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
A16: HC(g2,T)
= HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *' p2,T)
by POLYRED:22
.= HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) * HC(p2,T)
by A7,A12,TERMORD:32
.= coefficient(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) * HC(p2,T)
by TERMORD:23
.= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
Support sp <> {} by A1,POLYNOM7:1;
then A17: HT(sp,T) in Support sp by TERMORD:def 6;
sp.(lcm(HT(p1,T),HT(p2,T)))
= (g1-g2).HT(g2,T) by A13,Def4
.= (g1+-g2).HT(g2,T) by POLYNOM1:def 23
.= g1.HT(g2,T) + (-g2).HT(g2,T) by POLYNOM1:def 21
.= g1.HT(g2,T) + -(g2.HT(g2,T)) by POLYNOM1:def 22
.= HC(g1,T) + -(g2.HT(g2,T)) by A10,A13,TERMORD:def 7
.= HC(g1,T) + -HC(g2,T) by TERMORD:def 7
.= 0.L by A15,A16,RLVECT_1:16;
then not(lcm(HT(p1,T),HT(p2,T)) in Support sp) by POLYNOM1:def 9;
hence HT(S-Poly(p1,p2,T),T) < lcm(HT(p1,T),HT(p2,T)),T by A14,A17,TERMORD:def 3
;
end;
theorem
::: exercise 5.47 (iii), p. 211
for n being Ordinal,
T being connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 being non-zero Polynomial of n,L
holds HT(p2,T) divides HT(p1,T) implies
HC(p2,T) * p1 top_reduces_to S-Poly(p1,p2,T),p2,T
proof
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
p1,p2 be non-zero Polynomial of n,L;
assume A1: HT(p2,T) divides HT(p1,T);
A2: p1 <> 0_(n,L) & p2 <> 0_(n,L) by POLYNOM7:def 2;
then Support p1 <> {} by POLYNOM7:1;
then A3: HT(p1,T) in Support p1 by TERMORD:def 6;
set hcp2 = HC(p2,T);
A4: hcp2 <> 0.L by A2,TERMORD:17;
A5: HT(hcp2*p1,T) = HT(p1,T) by POLYRED:21;
consider b being bag of n such that
A6: HT(p1,T) = HT(p2,T) + b by A1,TERMORD:1;
set g = (hcp2*p1) - ((hcp2*p1).HT(p1,T)/HC(p2,T)) * (b *' p2);
A7: Support(p1) c= Support(hcp2*p1) by POLYRED:20;
then hcp2*p1 <> 0_(n,L) by A3,POLYNOM7:1;
then A8: hcp2*p1 reduces_to g,p2,HT(p1,T),T by A2,A3,A6,A7,POLYRED:def 5;
A9: lcm(HT(p1,T),HT(p2,T)) = HT(p1,T) by A1,Th11;
g = (hcp2*p1) - (hcp2*(p1.HT(p1,T))/HC(p2,T)) * (b *' p2) by POLYNOM7:def 10
.= (hcp2*p1) - ((hcp2*HC(p1,T))/HC(p2,T)) * (b *' p2) by TERMORD:def 7
.= (hcp2*p1) - ((hcp2*HC(p1,T))*(HC(p2,T)")) * (b *' p2) by VECTSP_1:def 23
.= (hcp2*p1) - (HC(p1,T)*(hcp2*(HC(p2,T)"))) * (b *' p2) by VECTSP_1:def 16
.= (hcp2*p1) - (HC(p1,T)*1_ L) * (b *' p2) by A4,VECTSP_1:def 22
.= (hcp2*p1) - HC(p1,T) * (b *' p2) by VECTSP_1:def 13
.= HC(p2,T) * (EmptyBag n) *' p1 - HC(p1,T) * (b *' p2) by POLYRED:17
.= HC(p2,T) * (HT(p1,T)/HT(p1,T)) *' p1 - HC(p1,T) * (b *' p2) by Th10
.= HC(p2,T) * (HT(p1,T)/HT(p1,T)) *' p1 -
HC(p1,T) * (HT(p1,T)/HT(p2,T)) *' p2 by A1,A6,Def1
.= S-Poly(p1,p2,T) by A9,Def4;
hence thesis by A5,A8,POLYRED:def 10;
end;
theorem
::: theorem 5.48 (i) ==> (ii), p. 211
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
G being Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T
implies (for g1,g2,h being Polynomial of n,L
st g1 in G & g2 in G &
h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
holds h = 0_(n,L))
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
G be Subset of Polynom-Ring(n,L);
assume A1: G is_Groebner_basis_wrt T;
set R = PolyRedRel(G,T);
per cases;
suppose G = {};
hence thesis;
suppose G <> {};
then reconsider G as non empty Subset of Polynom-Ring(n,L);
R is locally-confluent by A1,GROEB_1:def 3;
then R is confluent by GROEB_1:12;
then A2: R is with_UN_property by GROEB_1:13;
then A3: R is with_Church-Rosser_property by GROEB_1:14;
now let g1,g2,h being Polynomial of n,L;
assume A4: g1 in G & g2 in G &
h is_a_normal_form_of S-Poly(g1,g2,T),R;
then S-Poly(g1,g2,T) in G-Ideal by Th22;
then A5: R reduces S-Poly(g1,g2,T),0_(n,L) by A3,GROEB_1:15;
A6: now assume not(0_(n,L) is_a_normal_form_wrt R);
then consider b being set such that
A7: [0_(n,L),b] in R by REWRITE1:def 5;
consider f1,f2 being set such that
A8: f1 in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
f2 in the carrier of Polynom-Ring(n,L) &
[0_(n,L),b] = [f1,f2] by A7,ZFMISC_1:def 2;
A9: f1 in (the carrier of Polynom-Ring(n,L)) &
not(f1 in {0_(n,L)}) by A8,XBOOLE_0:def 4;
f1 = [0_(n,L),b]`1 by A8,MCART_1:def 1 .= 0_(n,L) by MCART_1:def 1;
hence contradiction by A9,TARSKI:def 1;
end;
A10: h is_a_normal_form_wrt R & R reduces S-Poly(g1,g2,T),h
by A4,REWRITE1:def 6;
then S-Poly(g1,g2,T),0_(n,L) are_convertible_wrt R &
h,S-Poly(g1,g2,T) are_convertible_wrt R by A5,REWRITE1:26;
then h,0_(n,L) are_convertible_wrt R by REWRITE1:31;
hence h = 0_(n,L) by A2,A6,A10,REWRITE1:def 19;
end;
hence thesis;
end;
theorem
::: theorem 5.48 (ii) ==> (iii), p. 211
for n being Nat,
T being connected admissible TermOrder of n,
L being Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
G being Subset of Polynom-Ring(n,L)
holds (for g1,g2,h being Polynomial of n,L
st g1 in G & g2 in G &
h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
holds h = 0_(n,L))
implies (for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L))
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be Abelian add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like non degenerated (non empty doubleLoopStr),
G be Subset of Polynom-Ring(n,L);
assume A1: for g1,g2,h being Polynomial of n,L
st g1 in G & g2 in G &
h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
holds h = 0_(n,L);
set R = PolyRedRel(G,T);
now let g1,g2 be Polynomial of n,L;
assume A2: g1 in G & g2 in G;
now per cases;
case S-Poly(g1,g2,T) in field R;
hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:def 14;
case not(S-Poly(g1,g2,T) in field R);
hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:47;
end;
then consider q being set such that
A3: q is_a_normal_form_of S-Poly(g1,g2,T),R by REWRITE1:def 11;
q is_a_normal_form_wrt R & R reduces S-Poly(g1,g2,T),q
by A3,REWRITE1:def 6;
then reconsider q as Polynomial of n,L by Lm1;
q = 0_(n,L) by A1,A2,A3;
hence R reduces S-Poly(g1,g2,T),0_(n,L) by A3,REWRITE1:def 6;
end;
hence thesis;
end;
theorem Th30:
::: theorem 5.48 (iii) ==> (i), p. 211
for n being Nat,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
G being Subset of Polynom-Ring(n,L) st not(0_(n,L) in G)
holds (for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L))
implies G is_Groebner_basis_wrt T
proof
let n be Nat,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
G be Subset of Polynom-Ring(n,L);
assume A1: not(0_(n,L) in G);
assume A2: for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L);
now let g1,g2 be Polynomial of n,L;
assume A3: g1 <> g2 & g1 in G & g2 in G;
thus for m1,m2 being Monomial of n,L st HM(m1 *'g1,T) = HM(m2 *'g2,T)
holds PolyRedRel(G,T) reduces m1 *' g1 - m2 *' g2, 0_(n,L)
proof
let m1,m2 be Monomial of n,L;
assume A4: HM(m1 *'g1,T) = HM(m2 *'g2,T);
set t1 = HT(g1,T), t2 = HT(g2,T);
set a1 = HC(g1,T), a2 = HC(g2,T);
set b1 = coefficient(m1), b2 = coefficient(m2);
set u1 = term(m1), u2 = term(m2);
A5: a1 <> 0.L & a2 <> 0.L by A1,A3,TERMORD:17;
then reconsider a1,a2 as non-zero Element of L by RLVECT_1:def 13;
reconsider g1,g2 as non-zero Polynomial of n,L by A1,A3,POLYNOM7:def 2;
A6: HC(m1*'g1,T) = coefficient(HM(m1*'g1,T)) by TERMORD:22
.= HC(m2*'g2,T) by A4,TERMORD:22;
now per cases;
case A7: b1 = 0.L or b2 = 0.L;
now per cases by A7;
case b1 = 0.L;
then HC(m1,T) = 0.L by TERMORD:23;
then m1 = 0_(n,L) by TERMORD:17;
then A8: m1 *' g1 = 0_(n,L) by POLYRED:5;
then HC(m2*'g2,T) = 0.L by A6,TERMORD:17;
then m2 *' g2 = 0_(n,L) by TERMORD:17;
then m1 *' g1 - m2 *' g2 = 0_(n,L) by A8,POLYRED:4;
hence thesis by REWRITE1:13;
case b2 = 0.L;
then HC(m2,T) = 0.L by TERMORD:23;
then m2 = 0_(n,L) by TERMORD:17;
then A9: m2 *' g2 = 0_(n,L) by POLYRED:5;
then HC(m1*'g1,T) = 0.L by A6,TERMORD:17;
then m1 *' g1 = 0_(n,L) by TERMORD:17;
then m1 *' g1 - m2 *' g2 = 0_(n,L) by A9,POLYRED:4;
hence thesis by REWRITE1:13;
end;
hence thesis;
case A10: b1 <> 0.L & b2 <> 0.L;
then reconsider b1,b2 as non-zero Element of L by RLVECT_1:def 13;
HC(m1,T) <> 0.L & HC(m2,T) <> 0.L by A10,TERMORD:23;
then m1 <> 0_(n,L) & m2 <> 0_(n,L) by TERMORD:17;
then reconsider m1,m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
A11: Monom(b1*a1,u1+t1)
= Monom(b1,u1) *' Monom(a1,t1) by TERMORD:3
.= m1 *' Monom(a1,t1) by POLYNOM7:11
.= HM(m1,T) *' Monom(a1,t1) by TERMORD:23
.= HM(m1,T) *' HM(g1,T) by TERMORD:def 8
.= HM(m2*'g2,T) by A4,TERMORD:33
.= HM(m2,T) *' HM(g2,T) by TERMORD:33
.= HM(m2,T) *' Monom(a2,t2) by TERMORD:def 8
.= m2 *' Monom(a2,t2) by TERMORD:23
.= Monom(b2,u2) *' Monom(a2,t2) by POLYNOM7:11
.= Monom(b2*a2,u2+t2) by TERMORD:3;
b1 * a1 <> 0.L & b2 * a2 <> 0.L by A5,A10,VECTSP_2:def 5;
then A12: b1 * a1 is non-zero & b2 * a2 is non-zero by RLVECT_1:def 13;
then A13: u1 + t1 = term(Monom(b2*a2,u2+t2)) by A11,POLYNOM7:10
.= u2 + t2 by A12,POLYNOM7:10;
t1 divides lcm(t1,t2) by Th7;
then consider s1 being bag of n such that
A14: t1 + s1 = lcm(t1,t2) by TERMORD:1;
t2 divides lcm(t1,t2) by Th7;
then consider s2 being bag of n such that
A15: t2 + s2 = lcm(t1,t2) by TERMORD:1;
t1 divides u1 + t1 & t2 divides u1 + t1 by A13,TERMORD:1;
then lcm(t1,t2) divides u1 + t1 by Th8;
then consider v being bag of n such that
A16: u1 + t1 = lcm(t1,t2) + v by TERMORD:1;
u1 + t1 = (v + s1) + t1 by A14,A16,POLYNOM1:39;
then A17: u1 = ((v + s1) + t1) -' t1 by POLYNOM1:52
.= v + s1 by POLYNOM1:52;
u2 + t2 = (v + s2) + t2 by A13,A15,A16,POLYNOM1:39;
then A18: u2 = ((v + s2) + t2) -' t2 by POLYNOM1:52
.= v + s2 by POLYNOM1:52;
b1*a1 = coefficient(Monom(b2*a2,u2+t2)) by A11,POLYNOM7:9
.= b2 * a2 by POLYNOM7:9;
then (b1 * a1) / a2 = (b2 * a2) * a2" by VECTSP_1:def 23
.= b2 * (a2 * a2") by VECTSP_1:def 16
.= b2 * 1_ L by A5,VECTSP_1:def 22;
then A19: b2 / a1 = ((b1 * a1) / a2) / a1 by VECTSP_2:def 2
.= ((b1 * a1) * a2") / a1 by VECTSP_1:def 23
.= ((b1 * a1) * a2") * a1" by VECTSP_1:def 23
.= ((b1 * a2") * a1) * a1" by VECTSP_1:def 16
.= (b1 * a2") * (a1 * a1") by VECTSP_1:def 16
.= (b1 * a2") * 1_ L by A5,VECTSP_1:def 22
.= b1 * a2" by VECTSP_2:def 2
.= b1 / a2 by VECTSP_1:def 23;
HT(g1,T) divides lcm(HT(g1,T),HT(g2,T)) by Th7;
then A20: s1 = lcm(HT(g1,T),HT(g2,T))/HT(g1,T) by A14,Def1;
HT(g2,T) divides lcm(HT(g1,T),HT(g2,T)) by Th7;
then A21: s2 = lcm(HT(g1,T),HT(g2,T))/HT(g2,T) by A15,Def1;
A22: (b1/a2)*a2 = (b1*a2")*a2 by VECTSP_1:def 23
.= b1*(a2"*a2) by VECTSP_1:def 16
.= b1*1_ L by A5,VECTSP_1:def 22;
A23: (b2/a1)*a1 = (b2*a1")*a1 by VECTSP_1:def 23
.= b2*(a1"*a1) by VECTSP_1:def 16
.= b2*1_ L by A5,VECTSP_1:def 22
.= b2 by VECTSP_2:def 2;
A24: m1 *' g1 - m2 *' g2
= Monom(b1,u1) *' g1 - m2 *' g2 by POLYNOM7:11
.= Monom(b1,u1) *' g1 - Monom(b2,u2) *' g2 by POLYNOM7:11
.= b1 * ((v+s1) *' g1) - Monom(b2,v+s2) *' g2 by A17,A18,POLYRED:22
.= b1 * (v *' (s1 *' g1)) - Monom(b2,v+s2) *' g2 by POLYRED:18
.= b1 * (v *' (s1 *' g1)) - b2 * ((v+s2) *' g2) by POLYRED:22
.= b1 * (v *' (s1 *' g1)) - b2 * (v *' (s2 *' g2)) by POLYRED:18
.= b1 * (v *' (s1 *' g1)) + -(b2 * (v *' (s2 *' g2))) by POLYNOM1:def 23
.= b1 * (v *' (s1 *' g1)) + b2 * (-(v *' (s2 *' g2))) by POLYRED:9
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (-(v*'(s2*'g2)))
by A22,A23,VECTSP_2:def 2
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (v*'(-(s2*'g2)))
by Th17
.= ((b1/a2) * a2) * (v*'(s1*'g1)) + (b1/a2) * (a1 * (v*'-(s2*'g2)))
by A19,POLYRED:11
.= (b1/a2) * (a2 * (v*'(s1*'g1))) + (b1/a2) * (a1 * (v*'-(s2*'g2)))
by POLYRED:11
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + a1 * (v*'-(s2*'g2))) by Th19
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (a1*(-(s2*'g2)))) by Th18
.= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by POLYRED:9
.= (b1/a2) * (v *' (a2*(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by Th18
.= (b1/a2) * (v *' (a2*(s1*'g1) + (-(a1*(s2*'g2))))) by Th16
.= (b1/a2) * (v *' (a2*(s1*'g1) - a1*(s2*'g2))) by POLYNOM1:def 23
.= (b1/a2) * v *' S-Poly(g1,g2,T) by A20,A21,Def4
.= Monom(b1/a2,v) *' S-Poly(g1,g2,T) by POLYRED:22;
PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L) by A2,A3;
hence thesis by A24,POLYRED:48;
end;
hence thesis;
end;
end;
hence thesis by A1,Th21;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
P be Subset of Polynom-Ring(n,L);
func S-Poly(P,T) -> Subset of Polynom-Ring(n,L) equals :Def5:
{ S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
p1 in P & p2 in P };
coherence
proof
set M = {S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
p1 in P & p2 in P};
now let u be set;
assume u in M;
then consider p1,p2 being Polynomial of n,L such that
A1: u = S-Poly(p1,p2,T) & p1 in P & p2 in P;
thus u in the carrier of Polynom-Ring(n,L) by A1,POLYNOM1:def 27;
end;
then M c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
hence thesis;
end;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
P be finite Subset of Polynom-Ring(n,L);
cluster S-Poly(P,T) -> finite;
coherence
proof
defpred P[set,set] means
ex p1,p2 being Polynomial of n,L
st p1 = $1`1 & $1`2 = p2 &
p1 in P & p2 in P & $2 = S-Poly(p1,p2,T);
A1: for x,y1,y2 being set st x in [:P,P:] & P[x,y1] & P[x,y2]
holds y1 = y2;
A2: for x being set st x in [:P,P:] ex y being set st P[x,y]
proof
let x be set;
assume x in [:P,P:];
then consider p1,p2 being set such that
A3: p1 in P & p2 in P & [p1,p2] = x by ZFMISC_1:def 2;
reconsider p1,p2 as Polynomial of n,L by A3,POLYNOM1:def 27;
take S-Poly(p1,p2,T);
take p1,p2;
thus x`1 = p1 by A3,MCART_1:def 1;
thus x`2 = p2 by A3,MCART_1:def 2;
thus thesis by A3;
end;
consider f being Function such that
A4: dom f = [:P,P:] & for x being set st x in [:P,P:] holds P[x,f.x]
from FuncEx(A1,A2);
A5: now let v be set;
assume v in rng f;
then consider u being set such that
A6: u in dom f & v = f.u by FUNCT_1:def 5;
consider p1,p2 being Polynomial of n,L such that
A7: p1 = u`1 & u`2 = p2 &
p1 in P & p2 in P & f.u = S-Poly(p1,p2,T) by A4,A6;
f.u in {S-Poly(p,q,T) where p,q is Polynomial of n,L :
p in P & q in P} by A7;
hence v in S-Poly(P,T) by A6,Def5;
end;
now let v be set;
assume v in S-Poly(P,T);
then v in {S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
p1 in P & p2 in P} by Def5;
then consider p1,p2 being Polynomial of n,L such that
A8: v = S-Poly(p1,p2,T) & p1 in P & p2 in P;
A9: [p1,p2] in dom f by A4,A8,ZFMISC_1:def 2;
then consider p1',p2' being Polynomial of n,L such that
A10: [p1,p2]`1 = p1' & [p1,p2]`2 = p2' & p1' in P & p2' in P &
f.[p1,p2] = S-Poly(p1',p2',T) by A4;
p1 = p1' & p2 = p2' by A10,MCART_1:def 1,def 2;
hence v in rng f by A8,A9,A10,FUNCT_1:def 5;
end;
then rng f = S-Poly(P,T) by A5,TARSKI:2;
hence thesis by A4,FINSET_1:26;
end;
end;
theorem
::: corollary 5.49, p. 212
for n being Nat,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
G being Subset of Polynom-Ring(n,L)
st not(0_(n,L) in G) &
for g being Polynomial of n,L st g in G holds g is Monomial of n,L
holds G is_Groebner_basis_wrt T
proof
let n being Nat,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
G being Subset of Polynom-Ring(n,L);
assume A1: not(0_(n,L) in G) & for g being Polynomial of n,L
st g in G holds g is Monomial of n,L;
now let g1,g2 be Polynomial of n,L;
assume g1 in G & g2 in G;
then g1 is Monomial of n,L & g2 is Monomial of n,L by A1;
then S-Poly(g1,g2,T) = 0_(n,L) by Th24;
hence PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L) by REWRITE1:13;
end;
hence thesis by A1,Th30;
end;
begin :: Standard Representations
theorem
for L being non empty multLoopStr,
P being non empty Subset of L,
A being LeftLinearCombination of P,
i being Nat
holds A|i is LeftLinearCombination of P
proof
let L be non empty multLoopStr,
P be non empty Subset of L,
A be LeftLinearCombination of P,
j be Nat;
set C = A|(Seg j);
reconsider C as FinSequence of the carrier of L by FINSEQ_1:23;
now let i be set;
assume A1: i in dom C;
then A2: dom C c= dom A & C.i = A.i by FUNCT_1:70,76;
then A3: C/.i = A.i by A1,FINSEQ_4:def 4 .= A/.i by A1,A2,FINSEQ_4:def 4;
consider u being Element of L, a being Element of P such that
A4: A/.i = u * a by A1,A2,IDEAL_1:def 10;
thus ex u being Element of L, a being Element of P
st C/.i = u * a by A3,A4;
end;
then C is LeftLinearCombination of P by IDEAL_1:def 10;
hence thesis by TOPREAL1:def 1;
end;
theorem
for L being non empty multLoopStr,
P being non empty Subset of L,
A being LeftLinearCombination of P,
i being Nat
holds A/^i is LeftLinearCombination of P
proof
let L be non empty multLoopStr,
P be non empty Subset of L,
A be LeftLinearCombination of P,
j be Nat;
set C = A/^j;
reconsider C as FinSequence of the carrier of L;
now per cases;
case A1: j <= len A;
then reconsider m = len A - j as Nat by INT_1:18;
now let i be set;
assume A2: i in dom C;
then reconsider k = i as Nat;
A3: C/.k = A/.(j+k) by A2,FINSEQ_5:30;
dom C = Seg(len C) by FINSEQ_1:def 3
.= Seg(m) by A1,RFINSEQ:def 2;
then A4: 1 <= k & k <= len A - j by A2,FINSEQ_1:3;
then k + j <= (len A - j) + j by AXIOMS:24;
then k + j <= (len A + -j) + j by XCMPLX_0:def 8;
then k + j <= len A + (-j + j) by XCMPLX_1:1;
then k + j <= len A + (j - j) by XCMPLX_0:def 8;
then A5: k + j <= len A + 0 by XCMPLX_1:14;
k <= k + j by NAT_1:29;
then 1 <= k + j by A4,AXIOMS:22;
then j + k in Seg(len A) by A5,FINSEQ_1:3;
then j + k in dom A by FINSEQ_1:def 3;
then consider u being Element of L, a being Element of P such that
A6: A/.(j+k) = u * a by IDEAL_1:def 10;
thus ex u being Element of L, a being Element of P
st C/.i = u * a by A3,A6;
end;
hence thesis by IDEAL_1:def 10;
case not(j <= len A);
then C = <*>(the carrier of L) by RFINSEQ:def 2;
then for i being set st i in dom C
ex u being Element of L, a being Element of P
st C/.i = u * a by FINSEQ_1:26;
hence thesis by IDEAL_1:def 10;
end;
hence thesis;
end;
theorem
for L being non empty multLoopStr,
P,Q being non empty Subset of L,
A being LeftLinearCombination of P
holds P c= Q implies A is LeftLinearCombination of Q
proof
let L be non empty multLoopStr,
P,Q be non empty Subset of L,
A be LeftLinearCombination of P;
assume A1: P c= Q;
now let i be set;
assume i in dom A;
then consider u being Element of L,
a being Element of P such that
A2: A/.i = u*a by IDEAL_1:def 10;
a in P;
hence ex u being Element of L,
a being Element of Q st A/.i = u*a by A1,A2;
end;
hence thesis by IDEAL_1:def 10;
end;
definition
let n be Ordinal,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
P be non empty Subset of Polynom-Ring(n,L),
A,B be LeftLinearCombination of P;
redefine func A^B -> LeftLinearCombination of P;
coherence
proof
A^B is LeftLinearCombination of P \/ P;
hence thesis;
end;
end;
definition
let n be Ordinal,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
pred A is_MonomialRepresentation_of f means :Def6:
Sum A = f &
for i being Nat st i in dom A
ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & A/.i = m *' p;
end;
theorem
for n being Ordinal,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A being LeftLinearCombination of P st A is_MonomialRepresentation_of f
holds Support f c= union { Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p }
proof
let n be Ordinal,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
defpred P[Nat] means
for f being Polynomial of n,L,
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f & len A = $1
holds Support f c= union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p};
A2: P[0]
proof let f be Polynomial of n,L,
A be LeftLinearCombination of P;
assume A3: A is_MonomialRepresentation_of f & len A = 0;
then A = <*>(the carrier of Polynom-Ring(n,L)) by FINSEQ_1:32;
then Sum A = 0.(Polynom-Ring(n,L)) by RLVECT_1:60;
then f = 0.(Polynom-Ring(n,L)) by A3,Def6;
then f = 0_(n,L) by POLYNOM1:def 27;
then Support f = {} by POLYNOM7:1;
hence Support f c= union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p} by XBOOLE_1:2;
end;
A4: now let k be Nat;
assume A5: P[k];
for f being Polynomial of n,L,
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f & len A = k+1
holds Support f c= union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p}
proof
let f be Polynomial of n,L,
A be LeftLinearCombination of P;
assume A6: A is_MonomialRepresentation_of f & len A = k+1;
then A7: Sum A = f &
for i being Nat st i in dom A
ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & A/.i = m*'p by Def6;
A <> <*>(the carrier of Polynom-Ring(n,L)) by A6,FINSEQ_1:32;
then reconsider A as non empty LeftLinearCombination of P;
consider A' being LeftLinearCombination of P,
e being Element of Polynom-Ring(n,L) such that
A8: A = A'^<* e *> & <*e*> is LeftLinearCombination of P by IDEAL_1:33;
A9: len A = len A' + len<*e*> by A8,FINSEQ_1:35
.= len A' + 1 by FINSEQ_1:56;
then A10: len A' = k by A6,XCMPLX_1:2;
reconsider g = Sum A' as Polynomial of n,L by POLYNOM1:def 27;
A11: dom A = Seg(k+1) by A6,FINSEQ_1:def 3;
A12: dom A' = Seg k by A10,FINSEQ_1:def 3;
k <= k + 1 by NAT_1:29;
then A13: dom A' c= dom A by A11,A12,FINSEQ_1:7;
now let i being Nat;
assume A14: i in dom A';
then A/.i = A.i by A13,FINSEQ_4:def 4
.= A'.i by A8,A14,FINSEQ_1:def 7 .= A'/.i by A14,FINSEQ_4:def
4;
hence ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & A'/.i = m*'p
by A6,A13,A14,Def6;
end;
then A' is_MonomialRepresentation_of g by Def6;
then A15: Support g c= union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A' & A'/.i = m*'p} by A5,A10;
reconsider ep = Sum(<*e*>) as Polynomial of n,L by POLYNOM1:def 27;
f = Sum A' + Sum(<*e*>) by A7,A8,RLVECT_1:58
.= g + ep by POLYNOM1:def 27;
then A16: Support f c= Support g \/ Support ep by POLYNOM1:79;
now let x be set;
assume A17: x in Support f;
then reconsider u = x as Element of Bags n;
now per cases by A16,A17,XBOOLE_0:def 2;
case u in Support g;
then consider Y being set such that
A18: u in Y & Y in {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A' & A'/.i = m*'p} by A15,TARSKI:def 4
;
consider m' being Monomial of n,L,
p' being Polynomial of n,L such that
A19: Y = Support(m'*'p') &
ex i being Nat st i in dom A' & A'/.i = m'*'p' by A18;
consider i being Nat such that
A20: i in dom A' & A'/.i = m'*'p' by A19;
A/.i = A.i by A13,A20,FINSEQ_4:def 4
.= A'.i by A8,A20,FINSEQ_1:def 7
.= A'/.i by A20,FINSEQ_4:def 4;
then Y in {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p} by A13,A19,A20;
hence u in union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p} by A18,TARSKI:def 4;
case A21: u in Support ep;
A22: A.(len A) = e by A8,A9,FINSEQ_1:59;
A23: dom A = Seg(len A) by FINSEQ_1:def 3;
1 <= len A by A6,NAT_1:29;
then A24: len A in Seg(len A) by FINSEQ_1:3;
then A25: len A in dom A by FINSEQ_1:def 3;
A26: ex m' being Monomial of n,L, p' being Polynomial of n,L
st p' in P & A/.(len A) = m' *' p' by A6,A23,A24,Def6;
A27: A/.(len A) = A.(len A) by A25,FINSEQ_4:def 4;
e = Sum(<*e*>) by RLVECT_1:61;
then Support ep in {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p} by A22,A25,A26,A27
;
hence u in union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p}
by A21,TARSKI:def 4;
end;
hence x in union {Support(m*'p) where m is Monomial of n,L,
p is Polynomial of n,L :
ex i being Nat st i in dom A & A/.i = m*'p};
end;
hence thesis by TARSKI:def 3;
end;
hence P[k+1];
end;
A28: for k being Nat holds P[k] from Ind(A2,A4);
consider n being Nat such that A29: len A = n;
thus thesis by A1,A28,A29;
end;
theorem
for n being Ordinal,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A,B being LeftLinearCombination of P
st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g
holds (A^B) is_MonomialRepresentation_of f+g
proof
let n be Ordinal,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A,B be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f &
B is_MonomialRepresentation_of g;
reconsider f' = f, g' = g as Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
reconsider f',g' as Element of Polynom-Ring(n,L);
A2: Sum(A^B) = Sum A + Sum B by RLVECT_1:58
.= f' + Sum B by A1,Def6
.= f' + g' by A1,Def6
.= f + g by POLYNOM1:def 27;
now let i be Nat;
assume A3: i in dom(A^B);
now per cases by A3,FINSEQ_1:38;
case A4: i in dom A;
dom A c= dom(A^B) by FINSEQ_1:39;
then (A^B)/.i = (A^B).i by A4,FINSEQ_4:def 4
.= A.i by A4,FINSEQ_1:def 7
.= A/.i by A4,FINSEQ_4:def 4;
hence ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & (A^B)/.i = m *' p
by A1,A4,Def6;
case ex k being Nat st k in dom B & i = len A + k;
then consider k being Nat such that
A5: k in dom B & i = len A + k;
i in dom(A^B) by A5,FINSEQ_1:41;
then (A^B)/.i = (A^B).i by FINSEQ_4:def 4
.= B.k by A5,FINSEQ_1:def 7
.= B/.k by A5,FINSEQ_4:def 4;
hence ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & (A^B)/.i = m *' p
by A1,A5,Def6;
end;
hence ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & (A^B)/.i = m *' p;
end;
hence thesis by A2,Def6;
end;
Lm4:
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f
for b being bag of n
holds (for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m *' p & p in P holds (m*'p).b = 0.L)
implies f.b = 0.L
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
let b be bag of n;
assume A2: for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m *' p & p in P holds (m*'p).b = 0.L;
A3: Sum A = f by A1,Def6;
defpred P[Nat] means
for f being Polynomial of n,L,
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f & f = Sum(A) & len A = $1
holds (for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m*'p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L;
A4: P[0]
proof
let f be Polynomial of n,L,
A be LeftLinearCombination of P;
assume A5: A is_MonomialRepresentation_of f &
f = Sum(A) & len A = 0;
assume for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m*'p & p in P holds (m*'p).b = 0.L;
f = Sum(<*>(the carrier of Polynom-Ring(n,L))) by A5,FINSEQ_1:32
.= 0.(Polynom-Ring(n,L)) by RLVECT_1:60
.= 0_(n,L) by POLYNOM1:def 27;
hence thesis by POLYNOM1:81;
end;
A6: now let k be Nat;
assume A7: P[k];
for f being Polynomial of n,L,
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f & f = Sum(A) & len A = k+1
holds (for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m*'p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L
proof
let f be Polynomial of n,L,
A be LeftLinearCombination of P;
assume A8: A is_MonomialRepresentation_of f &
f = Sum(A) & len A = k+1;
assume A9: for i being Nat st i in dom A
for m being Monomial of n,L, p being Polynomial of n,L
st A.i = m*'p & p in P holds (m*'p).b = 0.L;
set B = A|(Seg k);
reconsider B as FinSequence of Polynom-Ring(n,L) by FINSEQ_1:23;
reconsider B as LeftLinearCombination of P by IDEAL_1:42;
set g = Sum B;
reconsider g as Polynomial of n,L by POLYNOM1:def 27;
A10: dom A = Seg(k+1) by A8,FINSEQ_1:def 3;
A11: k <= len A by A8,NAT_1:29;
then A12: len B = k by FINSEQ_1:21;
A13: k <= k + 1 by NAT_1:29;
dom B = Seg(k) by A11,FINSEQ_1:21;
then A14: dom B c= dom A by A10,A13,FINSEQ_1:7;
now let i be Nat;
assume A15: i in dom B;
then consider m being Monomial of n,L,
p being Polynomial of n,L such that
A16: p in P & A/.i = m*'p by A8,A14,Def6;
B/.i = B.i by A15,FINSEQ_4:def 4 .= A.i by A15,FUNCT_1:68
.= A/.i by A14,A15,FINSEQ_4:def 4;
hence ex m being Monomial of n,L,
p being Polynomial of n,L
st p in P & B/.i = m *' p by A16;
end;
then A17: B is_MonomialRepresentation_of g by Def6;
reconsider h = A/.(k+1) as Polynomial of n,L by POLYNOM1:def 27;
A18: k + 1 in dom A by A10,FINSEQ_1:6;
then B^<*A/.(k+1)*> = B^<*A.(k+1)*> by FINSEQ_4:def 4
.= A by A8,FINSEQ_3:61;
then f = Sum(B) + Sum(<*A/.(k+1)*>) by A8,RLVECT_1:58
.= Sum B + A/.(k+1) by RLVECT_1:61
.= g + h by POLYNOM1:def 27;
then A19: f.b = g.b + h.b by POLYNOM1:def 21;
now let i be Nat;
assume A20: i in dom B;
now let m be Monomial of n,L, p be Polynomial of n,L;
assume A21: B.i = m*'p & p in P;
then A.i = m*'p by A20,FUNCT_1:68;
hence (m*'p).b = 0.L by A9,A14,A20,A21;
end;
hence for m being Monomial of n,L, p being Polynomial of n,L
st B.i = m*'p & p in P holds (m*'p).b = 0.L;
end;
then A22: g.b = 0.L by A7,A12,A17;
consider m being Monomial of n,L,
p being Polynomial of n,L such that
A23: p in P & A/.(k+1) = m *' p by A8,A18,Def6;
A/.(k+1) = A.(k+1) by A18,FINSEQ_4:def 4;
then 0.L = h.b by A9,A18,A23;
hence thesis by A19,A22,RLVECT_1:def 7;
end;
hence P[k+1];
end;
A24: for k being Nat holds P[k] from Ind(A4,A6);
consider n being Nat such that A25: n = len A;
thus thesis by A1,A2,A3,A24,A25;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P,
b be bag of n;
pred A is_Standard_Representation_of f,P,b,T means :Def7:
Sum A = f &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
pred A is_Standard_Representation_of f,P,T means :Def8:
A is_Standard_Representation_of f,P,HT(f,T),T;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
b be bag of n;
pred f has_a_Standard_Representation_of P,b,T means
ex A being LeftLinearCombination of P
st A is_Standard_Representation_of f,P,b,T;
end;
definition
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L);
pred f has_a_Standard_Representation_of P,T means :Def10:
ex A being LeftLinearCombination of P
st A is_Standard_Representation_of f,P,T;
end;
theorem Th37:
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A being LeftLinearCombination of P,
b being bag of n
holds A is_Standard_Representation_of f,P,b,T
implies A is_MonomialRepresentation_of f
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P,
b be bag of n;
assume A1: A is_Standard_Representation_of f,P,b,T;
then A2: Sum A = f &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
now let i be Nat;
assume i in dom A;
then consider m' being non-zero Monomial of n,L,
p' being non-zero Polynomial of n,L such that
A3: p' in P & A/.i = m'*'p' & HT(m'*'p',T) <= b,T by A1,Def7;
thus ex m being Monomial of n,L,
p being Polynomial of n,L st p in P & A/.i = m*'p by A3;
end;
hence thesis by A2,Def6;
end;
Lm5:
for n being Ordinal,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
f,g being Polynomial of n,L,
f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
for P being non empty Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,g implies
ex A being LeftLinearCombination of P
st f' = g' + Sum A &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T
proof
let n be Ordinal,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
f,g be Polynomial of n,L,
f',g' be Element of Polynom-Ring(n,L);
assume A1: f = f' & g = g';
let P be non empty Subset of Polynom-Ring(n,L);
assume A2: PolyRedRel(P,T) reduces f,g;
defpred P[Nat] means
for f,g being Polynomial of n,L,
f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
for P being non empty Subset of Polynom-Ring(n,L),
R being RedSequence of PolyRedRel(P,T)
st R.1 = f & R.len R = g & len R = $1
ex A being LeftLinearCombination of P
st f' = g' + Sum A &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T;
A3: P[1]
proof
let f,g be Polynomial of n,L,
f',g' be Element of Polynom-Ring(n,L);
assume A4: f = f' & g = g';
let P be non empty Subset of Polynom-Ring(n,L),
R be RedSequence of PolyRedRel(P,T);
assume A5: R.1 = f & R.len R = g & len R = 1;
set A = <*>(the carrier of Polynom-Ring(n,L));
A6: dom A = {};
for i being set st i in dom A
ex u being Element of Polynom-Ring(n,L),
a being Element of P st A/.i = u*a;
then reconsider A as LeftLinearCombination of P by IDEAL_1:def 10;
take A;
f' = g' + 0.(Polynom-Ring(n,L)) by A4,A5,RLVECT_1:def 7
.= g' + Sum A by RLVECT_1:60;
hence thesis by A6;
end;
A7: now let k be Nat;
assume A8: 1 <= k;
thus P[k] implies P[k+1]
proof
assume A9: P[k];
for f,g being Polynomial of n,L,
f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
for P being non empty Subset of Polynom-Ring(n,L),
R being RedSequence of PolyRedRel(P,T)
st R.1 = f & R.len R = g & len R = k + 1
ex A being LeftLinearCombination of P
st f' = g' + Sum A &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T
proof
let f,g be Polynomial of n,L,
f',g' be Element of Polynom-Ring(n,L);
assume A10: f = f' & g = g';
let P be non empty Subset of Polynom-Ring(n,L),
R be RedSequence of PolyRedRel(P,T);
assume A11: R.1 = f & R.len R = g & len R = k + 1;
then A12: dom R = Seg(k+1) by FINSEQ_1:def 3;
A13: k <= k + 1 by NAT_1:29;
then A14: k in dom R by A8,A12,FINSEQ_1:3;
A15: 1 <= k + 1 by NAT_1:29;
set Q = R|(Seg k);
reconsider Q as FinSequence by FINSEQ_1:19;
A16: len Q = k by A11,A13,FINSEQ_1:21;
A17: dom Q = Seg k by A11,A13,FINSEQ_1:21;
k <> 0 by A8;
then A18: len Q > 0 by A16,NAT_1:19;
now let i be Nat;
assume A19: i in dom Q & i+1 in dom Q;
then A20: 1 <= i & i <= k & 1 <= i+1 & i+1 <= k by A17,FINSEQ_1:3;
then A21: i <= k+1 & i+1 <= k+1 by A13,AXIOMS:22;
then A22: i in dom R by A12,A20,FINSEQ_1:3;
i+1 in dom R by A12,A20,A21,FINSEQ_1:3;
then A23: [R.i, R.(i+1)] in PolyRedRel(P,T) by A22,REWRITE1:def 2;
R.i = Q.i by A19,FUNCT_1:68;
hence [Q.i, Q.(i+1)] in PolyRedRel(P,T) by A19,A23,FUNCT_1:68;
end;
then reconsider Q as RedSequence of PolyRedRel(P,T)
by A18,REWRITE1:def 2;
k + 1 in dom R by A12,A15,FINSEQ_1:3;
then A24: [R.k,R.(k+1)] in PolyRedRel(P,T) by A14,REWRITE1:def 2;
then consider h',g2 being set such that
A25: [R.k,R.(k+1)] = [h',g2] &
h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
g2 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
A26: R.k = [h',g2]`1 by A25,MCART_1:def 1 .= h' by MCART_1:def 1;
A27: h' in (the carrier of Polynom-Ring(n,L)) by A25,XBOOLE_0:def 4;
not(h' in {0_(n,L)}) by A25,XBOOLE_0:def 4;
then h' <> 0_(n,L) by TARSKI:def 1;
then reconsider h' as non-zero Polynomial of n,L
by A27,POLYNOM1:def 27,POLYNOM7:def 2;
reconsider g2 as Polynomial of n,L by A25,POLYNOM1:def 27;
k <> 0 by A8;
then A28: k in dom Q by A17,FINSEQ_1:5;
then A29: Q.k = h' by A26,FUNCT_1:68;
then Q.k is Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
then reconsider u' = Q.k as Element of Polynom-Ring(n,L)
;
reconsider u = u' as Polynomial of n,L by POLYNOM1:def 27;
A30: 1 in dom Q by A8,A17,FINSEQ_1:3;
then A31: Q.1 = f by A11,FUNCT_1:68;
Q.len Q = u by A11,A13,FINSEQ_1:21;
then consider A' being LeftLinearCombination of P such that
A32: f' = u' + Sum A' &
for i being Nat st i in dom A'
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A'.i = m*'p & HT(m*'p,T)<=HT(f,T),T by A9,A10,A16,A31;
now per cases;
case u' = g';
hence thesis by A32;
case A33: u' <> g';
h' reduces_to g2,P,T by A24,A25,POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A34: p' in P & h' reduces_to g2,p',T by POLYRED:def 7;
consider m' being Monomial of n,L such that
A35: g2 = h' - m' *' p' &
not(HT(m'*'p',T) in Support g2) & HT(m'*'p',T) <= HT(h',T),T
by A34,GROEB_1:2;
h' is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
then reconsider hh = h' as Element of Polynom-Ring(n,L)
;
A36: R.(k+1) = [h',g2]`2 by A25,MCART_1:def 2 .= g2 by MCART_1:def 2;
then reconsider gg = g2 as Element of Polynom-Ring(n,L) by A10,A11;
m' is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
then reconsider mm = m' as Element of Polynom-Ring(n,L)
;
reconsider pp = p' as Element of P by A34;
m'*'p' is Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
then reconsider mp = m'*'p' as Element of Polynom-Ring(n,L)
;
A37: mp = mm * pp by POLYNOM1:def 27;
now assume p' = 0_(n,L);
then g2 = h' - 0_(n,L) by A35,POLYRED:5
.= Q.k by A29,POLYRED:4;
hence contradiction by A10,A11,A33,A36;
end;
then reconsider p' as non-zero Polynomial of n,L by POLYNOM7:def 2;
now assume m' = 0_(n,L);
then g2 = h' - 0_(n,L) by A35,POLYRED:5
.= Q.k by A29,POLYRED:4;
hence contradiction by A10,A11,A33,A36;
end;
then reconsider m' as non-zero Monomial of n,L by POLYNOM7:def 2;
A38: gg = hh - mp by A35,Lm3;
A39: PolyRedRel(P,T) reduces f,h' by A8,A28,A29,A30,A31,REWRITE1:18;
h' is_reducible_wrt p',T by A34,POLYRED:def 8;
then h' <> 0_(n,L) by POLYRED:37;
then HT(h',T) <= HT(f,T),T by A39,POLYRED:44;
then A40: HT(m'*'p',T) <= HT(f,T),T by A35,TERMORD:8;
set B = (A')^(<*mp*>);
len B = len A' + len<*m'*'p'*> by FINSEQ_1:35
.= len A' + 1 by FINSEQ_1:57;
then A41: dom B = Seg(len A' + 1) by FINSEQ_1:def 3;
now let i be set;
assume A42: i in dom B;
then reconsider j = i as Nat;
A43: 1 <= j & j <= len A' + 1 by A41,A42,FINSEQ_1:3;
now per cases;
case j = len A' + 1;
then mp = B.j by FINSEQ_1:59 .= B/.j by A42,FINSEQ_4:def 4;
hence ex u being Element of Polynom-Ring(n,L),
a being Element of P st B/.i = u*a by A37;
case j <> len A' + 1;
then j < len A' + 1 by A43,REAL_1:def 5;
then j <= len A' by NAT_1:38;
then j in Seg(len A') by A43,FINSEQ_1:3;
then A44: j in dom A' by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A45: p in P & A'.j = m*'p & HT(m*'p,T) <= HT(f,T),T by A32;
A46: B.j = B/.j by A42,FINSEQ_4:def 4;
m is Element of Polynom-Ring(n,L)
by POLYNOM1:def 27;
then reconsider u' = m as Element of Polynom-Ring(n,L)
;
reconsider a' = p as Element of P by A45;
u' * a' = m *' p by POLYNOM1:def 27
.= B/.j by A44,A45,A46,FINSEQ_1:def 7;
hence ex u being Element of Polynom-Ring(n,L),
a being Element of P st B/.i = u*a;
end;
hence ex u being Element of Polynom-Ring(n,L),
a being Element of P st B/.i = u*a;
end;
then reconsider B as LeftLinearCombination of P by IDEAL_1:def 10;
take B;
A47: gg + Sum B = gg + (Sum(A') + Sum(<*mp*>)) by RLVECT_1:58
.= gg + (Sum(A') + mp) by RLVECT_1:61
.= (hh + -mp) + (Sum(A') + mp) by A38,RLVECT_1:def 11
.= hh + (-mp + (Sum(A') + mp)) by RLVECT_1:def 6
.= hh + (Sum(A') + (-mp + mp)) by RLVECT_1:def 6
.= hh + (Sum(A') + 0.(Polynom-Ring(n,L))) by RLVECT_1:16
.= hh + Sum(A') by RLVECT_1:10
.= f' by A26,A28,A32,FUNCT_1:68;
now let i be Nat;
assume i in dom B;
then A48: 1 <= i & i <= len A' + 1 by A41,FINSEQ_1:3;
now per cases;
case i = len A' + 1;
then mp = B.i by FINSEQ_1:59;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A34,A40;
case i <> len A' + 1;
then i < len A' + 1 by A48,REAL_1:def 5;
then i <= len A' by NAT_1:38;
then i in Seg(len A') by A48,FINSEQ_1:3;
then A49: i in dom A' by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A50: p in P & A'.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A32;
B.i = m *' p by A49,A50,FINSEQ_1:def 7;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A50;
end;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T;
end;
hence thesis by A10,A11,A36,A47;
end;
hence thesis;
end;
hence thesis;
end;
end;
A51: for k being Nat st 1 <= k holds P[k] from Ind2(A3,A7);
consider R being RedSequence of PolyRedRel(P,T) such that
A52: R.1 = f & R.len R = g by A2,REWRITE1:def 3;
len R > 0 by REWRITE1:def 2;
then 1 <= len R by RLVECT_1:99;
hence thesis by A1,A51,A52;
end;
theorem
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A,B being LeftLinearCombination of P,
b being bag of n
st A is_Standard_Representation_of f,P,b,T &
B is_Standard_Representation_of g,P,b,T
holds A^B is_Standard_Representation_of f+g,P,b,T
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A,B be LeftLinearCombination of P,
b be bag of n;
assume A1: A is_Standard_Representation_of f,P,b,T &
B is_Standard_Representation_of g,P,b,T;
then f = Sum A & g = Sum B by Def7;
then A2: f + g = Sum A + Sum B by POLYNOM1:def 27
.= Sum(A^B) by RLVECT_1:58;
now let i be Nat;
assume A3: i in dom(A^B);
now per cases by A3,FINSEQ_1:38;
case A4: i in dom A;
then consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A5: p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by A1,Def7;
(A^B)/.i = (A^B).i by A3,FINSEQ_4:def 4
.= A.i by A4,FINSEQ_1:def 7
.= A/.i by A4,FINSEQ_4:def 4;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A5;
case ex k being Nat st k in dom B & i = len A + k;
then consider k being Nat such that
A6: k in dom B & i = len A + k;
consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A7: p in P & B/.k = m *' p & HT(m*'p,T) <= b,T by A1,A6,Def7;
(A^B)/.i = (A^B).i by A3,FINSEQ_4:def 4
.= B.k by A6,FINSEQ_1:def 7
.= B/.k by A6,FINSEQ_4:def 4;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A7;
end;
hence ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T;
end;
hence thesis by A2,Def7;
end;
theorem
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A,B being LeftLinearCombination of P,
b being bag of n,
i being Nat
st A is_Standard_Representation_of f,P,b,T &
B = A|i & g = Sum(A/^i)
holds B is_Standard_Representation_of f-g,P,b,T
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A,B be LeftLinearCombination of P,
b be bag of n,
i be Nat;
assume A1: A is_Standard_Representation_of f,P,b,T &
B = A|i & g = Sum(A/^i);
then A2: Sum A = f &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
A = B ^ (A/^i) by A1,RFINSEQ:21;
then Sum A = Sum B + Sum(A/^i) by RLVECT_1:58;
then Sum A + -(Sum(A/^i))
= Sum B + (Sum(A/^i) + -Sum(A/^i)) by RLVECT_1:def 6
.= Sum B + 0.(Polynom-Ring(n,L)) by RLVECT_1:16
.= Sum B by RLVECT_1:def 7;
then A3: Sum B = Sum A - (Sum(A/^i)) by RLVECT_1:def 11
.= f - g by A1,A2,Lm3;
dom(A|(Seg i)) c= dom A by FUNCT_1:76;
then A4: dom B c= dom A by A1,TOPREAL1:def 1;
now let j being Nat;
assume A5: j in dom B;
then A6: j in dom(A|(Seg i)) by A1,TOPREAL1:def 1;
A7: A/.j = A.j by A4,A5,FINSEQ_4:def 4
.= (A|(Seg i)).j by A6,FUNCT_1:70
.= B.j by A1,TOPREAL1:def 1
.= B/.j by A5,FINSEQ_4:def 4;
consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A8: p in P & A/.j = m *' p & HT(m*'p,T) <= b,T
by A1,A4,A5,Def7;
thus ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A7,A8;
end;
hence thesis by A3,Def7;
end;
theorem
for n being Ordinal,
T being connected TermOrder of n,
L being Abelian right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A,B being LeftLinearCombination of P,
b being bag of n,
i being Nat
st A is_Standard_Representation_of f,P,b,T &
B = A/^i & g = Sum(A|i) & i <= len A
holds B is_Standard_Representation_of f-g,P,b,T
proof
let n be Ordinal,
T be connected TermOrder of n,
L be Abelian right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f,g be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A,B be LeftLinearCombination of P,
b be bag of n,
i be Nat;
assume A1: A is_Standard_Representation_of f,P,b,T &
B = A/^i & g = Sum(A|i) & i <= len A;
then A2: Sum A = f &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
A = (A|i) ^ B by A1,RFINSEQ:21;
then Sum A = Sum(A|i) + Sum B by RLVECT_1:58;
then Sum A + -(Sum(A|i))
= (Sum(A|i) + -Sum(A|i)) + Sum B by RLVECT_1:def 6
.= 0.(Polynom-Ring(n,L)) + Sum B by RLVECT_1:16
.= Sum B by ALGSTR_1:def 5;
then A3: Sum B = Sum A - (Sum(A|i)) by RLVECT_1:def 11
.= f - g by A1,A2,Lm3;
now let j being Nat;
assume A4: j in dom B;
then A5: j + i in dom A by A1,FINSEQ_5:29;
A6: B/.j = B.j by A4,FINSEQ_4:def 4
.= A.(j+i) by A1,A4,RFINSEQ:def 2
.= A/.(j+i) by A5,FINSEQ_4:def 4;
consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A7: p in P & A/.(j+i) = m *' p & HT(m*'p,T) <= b,T
by A1,A5,Def7;
thus ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A6,A7;
end;
hence thesis by A3,Def7;
end;
theorem Th41:
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f being non-zero Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f
ex i being Nat,
m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st i in dom A & p in P & A.i = m *' p & HT(f,T) <= HT(m*'p,T),T
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be non-zero Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
f <> 0_(n,L) by POLYNOM7:def 2;
then HC(f,T) <> 0.L by TERMORD:17;
then f.(HT(f,T)) <> 0.L by TERMORD:def 7;
then consider i being Nat such that
A2: i in dom A &
ex m being Monomial of n,L, p being Polynomial of n,L
st A.i = m *' p & p in P & (m*'p).HT(f,T) <> 0.L by A1,Lm4;
consider m being Monomial of n,L, p being Polynomial of n,L such that
A3: A.i = m *' p & (m*'p).HT(f,T) <> 0.L & p in P by A2;
A4: m*'p <> 0_(n,L) by A3,POLYNOM1:81;
then m <> 0_(n,L) by POLYRED:5;
then reconsider m as non-zero Monomial of n,L by POLYNOM7:def 2;
p <> 0_(n,L) by A4,POLYNOM1:87;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 2;
HT(f,T) in Support(m*'p) by A3,POLYNOM1:def 9;
then HT(f,T) <= HT(m*'p,T),T by TERMORD:def 6;
hence thesis by A2,A3;
end;
theorem Th42:
for n being Ordinal,
T being connected TermOrder of n,
L being right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f being non-zero Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L),
A being LeftLinearCombination of P
st A is_Standard_Representation_of f,P,T
ex i being Nat,
m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st p in P & i in dom A & A/.i = m *' p & HT(f,T) = HT(m*'p,T)
proof
let n be Ordinal,
T be connected TermOrder of n,
L be right_zeroed add-associative right_complementable
unital distributive non trivial (non empty doubleLoopStr),
f be non-zero Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L),
A be LeftLinearCombination of P;
assume A is_Standard_Representation_of f,P,T;
then A1: A is_Standard_Representation_of f,P,HT(f,T),T by Def8;
then A is_MonomialRepresentation_of f by Th37;
then consider i being Nat, m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A2: i in dom A & p in P & A.i = m *' p &
HT(f,T) <= HT(m*'p,T),T by Th41;
consider m' being non-zero Monomial of n,L,
p' being non-zero Polynomial of n,L such that
A3: p' in P & A/.i = m' *' p' & HT(m'*'p',T) <= HT(f,T),T by A1,A2,Def7;
take i,m',p';
m *' p = m' *' p' by A2,A3,FINSEQ_4:def 4;
hence thesis by A2,A3,TERMORD:7;
end;
theorem Th43:
::: lemma 5.60, p. 218
for n being Ordinal,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
f being Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,0_(n,L) implies
f has_a_Standard_Representation_of P,T
proof
let n be Ordinal,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Abelian Field-like non degenerated (non empty doubleLoopStr),
f be Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L);
assume A1: PolyRedRel(P,T) reduces f,0_(n,L);
f is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
then reconsider f' = f as Element of Polynom-Ring(n,L);
0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then consider A being LeftLinearCombination of P such that
A2: f' = 0.(Polynom-Ring(n,L)) + Sum A &
for i being Nat st i in dom A
ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A1,Lm5;
A3: f = Sum A by A2,RLVECT_1:def 7;
now let i be Nat;
assume A4: i in dom A;
then A5: A.i = A/.i by FINSEQ_4:def 4;
consider m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A6: p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A2,A4;
thus ex m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L
st p in P & A/.i = m *' p & HT(m*'p,T) <= HT(f,T),T by A5,A6;
end;
then A is_Standard_Representation_of f,P,HT(f,T),T by A3,Def7;
then A is_Standard_Representation_of f,P,T by Def8;
hence thesis by Def10;
end;
theorem Th44:
::: lemma 5.61, p. 218
for n being Ordinal,
T being admissible connected TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
f being non-zero Polynomial of n,L,
P being non empty Subset of Polynom-Ring(n,L)
holds f has_a_Standard_Representation_of P,T implies
f is_top_reducible_wrt P,T
proof
let n be Ordinal,
T be admissible connected TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive
Field-like (non trivial doubleLoopStr),
f be non-zero Polynomial of n,L,
P be non empty Subset of Polynom-Ring(n,L);
assume f has_a_Standard_Representation_of P,T;
then consider A being LeftLinearCombination of P
such that A1: A is_Standard_Representation_of f,P,T by Def10;
consider i being Nat,
m being non-zero Monomial of n,L,
p being non-zero Polynomial of n,L such that
A2: p in P & i in dom A & A/.i = m*'p & HT(f,T) = HT(m*'p,T) by A1,Th42;
A3: i in dom A & p <> 0_(n,L) & p in P &
A/.i = m *' p by A2,POLYNOM7:def 2;
A4: f <> 0_(n,L) by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then A5: HT(f,T) in Support f by TERMORD:def 6;
set s = HT(m,T);
set g = f - (f.HT(f,T)/HC(p,T)) * (s *' p);
HT(f,T) = s + HT(p,T) by A2,TERMORD:31;
then f reduces_to g,p,HT(f,T),T by A3,A4,A5,POLYRED:def 5;
then f top_reduces_to g,p,T by POLYRED:def 10;
then f is_top_reducible_wrt p,T by POLYRED:def 11;
hence thesis by A2,POLYRED:def 12;
end;
theorem
::: theorem 5.62, p. 219
for n being Nat,
T being connected admissible TermOrder of n,
L being add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
G being non empty Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T
iff for f being non-zero Polynomial of n,L st f in G-Ideal
holds f has_a_Standard_Representation_of G,T
proof
let n be Nat,
T be connected admissible TermOrder of n,
L be add-associative right_complementable right_zeroed
commutative associative well-unital distributive Abelian
Field-like non degenerated (non empty doubleLoopStr),
P be non empty Subset of Polynom-Ring(n,L);
A1: now assume P is_Groebner_basis_wrt T;
then PolyRedRel(P,T) is locally-confluent by GROEB_1:def 3;
then PolyRedRel(P,T) is confluent by GROEB_1:12;
then PolyRedRel(P,T) is with_UN_property by GROEB_1:13;
then A2: PolyRedRel(P,T) is with_Church-Rosser_property by GROEB_1:14;
now let f be non-zero Polynomial of n,L;
assume f in P-Ideal;
then PolyRedRel(P,T) reduces f,0_(n,L) by A2,GROEB_1:15;
hence f has_a_Standard_Representation_of P,T by Th43;
end;
hence for f being non-zero Polynomial of n,L st f in P-Ideal
holds f has_a_Standard_Representation_of P,T;
end;
now assume A3: for f being non-zero Polynomial of n,L st f in P-Ideal
holds f has_a_Standard_Representation_of P,T;
now let f be non-zero Polynomial of n,L;
assume f in P-Ideal;
then f has_a_Standard_Representation_of P,T by A3;
hence f is_top_reducible_wrt P,T by Th44;
end;
then for b being bag of n st b in HT(P-Ideal,T)
ex b' being bag of n st b' in HT(P,T) & b' divides b by GROEB_1:18;
then HT(P-Ideal,T) c= multiples(HT(P,T)) by GROEB_1:19;
then PolyRedRel(P,T) is locally-confluent by GROEB_1:20;
hence P is_Groebner_basis_wrt T by GROEB_1:def 3;
end;
hence thesis by A1;
end;