let n be Element of NAT ; for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let T be connected admissible TermOrder of n; for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); ( I <> {(0_ (n,L))} implies ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T ) )
set R = RelStr(# (Bags n),(DivOrder n) #);
assume A1:
I <> {(0_ (n,L))}
; ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
ex q being Element of I st q <> 0_ (n,L)
then consider q being Element of I such that
A5:
q <> 0_ (n,L)
;
reconsider q = q as Polynomial of n,L by POLYNOM1:def 11;
HT (q,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) }
by A5;
then reconsider hti = HT (I,T) as non empty Subset of RelStr(# (Bags n),(DivOrder n) #) ;
set hq = HT (q,T);
consider S being set such that
A6:
S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #)
and
A7:
for C being set st C is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) holds
S c= C
by DICKSON:34;
reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;
A10:
S c= hti
by A6, DICKSON:def 9;
then reconsider S = S as finite Subset of (Bags n) by A8, TARSKI:def 3;
set M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } ;
set s = the Element of S;
hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) }
by A5;
then A11:
ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in S & b <= hq )
by A6, DICKSON:def 9;
then
the Element of S in S
;
then reconsider s = the Element of S as Element of Bags n ;
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for r being Polynomial of n,L holds
( not r in I or not r < p,T or not r <> 0_ (n,L) or not HM (r,T) = Monom ((1. L),s) ) ) ) } in { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S }
by A11;
then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } as non empty set ;
set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ;
A12:
for x being set st x in M holds
ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ (n,L) )
proof
let x be
set ;
( x in M implies ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ (n,L) ) )
assume
x in M
;
ex q being Polynomial of n,L st
( q in I & x = {q} & q <> 0_ (n,L) )
then consider s being
Element of
Bags n such that A13:
x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
and A14:
s in S
;
s in hti
by A10, A14;
then consider q being
Polynomial of
n,
L such that A15:
s = HT (
q,
T)
and A16:
(
q in I &
q <> 0_ (
n,
L) )
;
consider qq being
Polynomial of
n,
L such that A17:
(
qq in I &
HM (
qq,
T)
= Monom (
(1. L),
(HT (q,T))) &
qq <> 0_ (
n,
L) )
by A16, Lm10;
set M9 =
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } ;
A18:
now for u being object st u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } holds
u in the carrier of (Polynom-Ring (n,L))let u be
object ;
( u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } implies u in the carrier of (Polynom-Ring (n,L)) )assume
u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) }
;
u in the carrier of (Polynom-Ring (n,L))then
ex
pp being
Polynomial of
n,
L st
(
u = pp &
pp in I &
HM (
pp,
T)
= Monom (
(1. L),
s) &
pp <> 0_ (
n,
L) )
;
hence
u in the
carrier of
(Polynom-Ring (n,L))
;
verum end;
qq in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) }
by A15, A17;
then reconsider M9 =
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } as non
empty Subset of
(Polynom-Ring (n,L)) by A18, TARSKI:def 3;
reconsider M9 =
M9 as non
empty Subset of
(Polynom-Ring (n,L)) ;
consider p being
Polynomial of
n,
L such that A19:
p in M9
and A20:
for
r being
Polynomial of
n,
L st
r in M9 holds
p <= r,
T
by POLYRED:31;
consider p9 being
Polynomial of
n,
L such that A21:
p9 = p
and A22:
p9 in I
and A23:
HM (
p9,
T)
= Monom (
(1. L),
s)
and A24:
p9 <> 0_ (
n,
L)
by A19;
A25:
now for q being Polynomial of n,L holds
( not q in I or not q < p9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) )assume
ex
q being
Polynomial of
n,
L st
(
q in I &
q < p9,
T &
q <> 0_ (
n,
L) &
HM (
q,
T)
= Monom (
(1. L),
s) )
;
contradictionthen consider q being
Polynomial of
n,
L such that A26:
q in I
and A27:
q < p9,
T
and A28:
(
q <> 0_ (
n,
L) &
HM (
q,
T)
= Monom (
(1. L),
s) )
;
q in M9
by A26, A28;
then
p <= q,
T
by A20;
hence
contradiction
by A21, A27, POLYRED:29;
verum end;
A29:
now for q being Polynomial of n,L holds
( not q in I or not q < p9,T or not HM (q,T) = Monom ((1. L),s) )A30:
1. L <> 0. L
;
assume
ex
q being
Polynomial of
n,
L st
(
q in I &
q < p9,
T &
HM (
q,
T)
= Monom (
(1. L),
s) )
;
contradictionthen consider q being
Polynomial of
n,
L such that A31:
(
q in I &
q < p9,
T )
and A32:
HM (
q,
T)
= Monom (
(1. L),
s)
;
HC (
q,
T) =
coefficient (Monom ((1. L),s))
by A32, TERMORD:22
.=
1. L
by POLYNOM7:9
;
then
q <> 0_ (
n,
L)
by A30, TERMORD:17;
hence
contradiction
by A25, A31, A32;
verum end;
A33:
now for u being object st u in x holds
u in {p9}let u be
object ;
( u in x implies u in {p9} )assume
u in x
;
u in {p9}then consider u9 being
Polynomial of
n,
L such that A34:
u9 = u
and A35:
(
u9 in I &
HM (
u9,
T)
= Monom (
(1. L),
s) )
and
u9 <> 0_ (
n,
L)
and A36:
for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < u9,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
s) )
by A13;
now for q being Polynomial of n,L holds
( not q in I or not q < u9,T or not HM (q,T) = Monom ((1. L),s) )A37:
1. L <> 0. L
;
assume
ex
q being
Polynomial of
n,
L st
(
q in I &
q < u9,
T &
HM (
q,
T)
= Monom (
(1. L),
s) )
;
contradictionthen consider q being
Polynomial of
n,
L such that A38:
(
q in I &
q < u9,
T )
and A39:
HM (
q,
T)
= Monom (
(1. L),
s)
;
HC (
q,
T) =
coefficient (Monom ((1. L),s))
by A39, TERMORD:22
.=
1. L
by POLYNOM7:9
;
then
q <> 0_ (
n,
L)
by A37, TERMORD:17;
hence
contradiction
by A36, A38, A39;
verum end; then
u9 = p9
by A22, A23, A29, A35, Th37;
hence
u in {p9}
by A34, TARSKI:def 1;
verum end;
take
p9
;
( p9 in I & x = {p9} & p9 <> 0_ (n,L) )
p9 in x
by A13, A22, A23, A24, A25;
then
for
u being
object st
u in {p9} holds
u in x
by TARSKI:def 1;
hence
(
p9 in I &
x = {p9} &
p9 <> 0_ (
n,
L) )
by A22, A24, A33, TARSKI:2;
verum
end;
then A45:
{ r where r is Polynomial of n,L : ex x being Element of M st x = {r} } c= I
;
A46:
M is finite
proof
defpred S1[
object ,
object ]
means $2
= { p where p is Polynomial of n,L : ex b being bag of n st
( b = $1 & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } ;
A47:
for
x being
object st
x in S holds
ex
y being
object st
S1[
x,
y]
;
consider f being
Function such that A48:
(
dom f = S & ( for
x being
object st
x in S holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A47);
A49:
now for u being object st u in rng f holds
u in Mlet u be
object ;
( u in rng f implies u in M )assume
u in rng f
;
u in Mthen consider s being
object such that A50:
s in dom f
and A51:
u = f . s
by FUNCT_1:def 3;
reconsider s =
s as
Element of
Bags n by A48, A50;
set V =
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ;
A52:
ex
b being
bag of
n st
f . s = { p where p is Polynomial of n,L : ex b being bag of n st
( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) }
by A48, A50;
A53:
now for v being object st v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } holds
v in f . slet v be
object ;
( v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } implies v in f . s )assume
v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
;
v in f . sthen
ex
p being
Polynomial of
n,
L st
(
v = p &
p in I &
HM (
p,
T)
= Monom (
(1. L),
s) &
p <> 0_ (
n,
L) & ( for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < p,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
s) ) ) )
;
hence
v in f . s
by A52;
verum end; now for v being object st v in f . s holds
v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } let v be
object ;
( v in f . s implies v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } )assume
v in f . s
;
v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } then
ex
p being
Polynomial of
n,
L st
(
v = p & ex
b being
bag of
n st
(
b = s &
p in I &
HM (
p,
T)
= Monom (
(1. L),
b) &
p <> 0_ (
n,
L) & ( for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < p,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
b) ) ) ) )
by A52;
hence
v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
;
verum end; then
u = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
by A51, A53, TARSKI:2;
hence
u in M
by A48, A50;
verum end;
now for u being object st u in M holds
u in rng flet u be
object ;
( u in M implies u in rng f )reconsider uu =
u as
set by TARSKI:1;
assume
u in M
;
u in rng fthen consider s being
Element of
Bags n such that A54:
u = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
and A55:
s in S
;
A56:
ex
b being
bag of
n st
f . s = { p where p is Polynomial of n,L : ex b being bag of n st
( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) }
by A48, A55;
f . s in rng f
by A48, A55, FUNCT_1:3;
hence
u in rng f
by A57, A58, TARSKI:2;
verum end;
then
rng f = M
by A49, TARSKI:2;
hence
M is
finite
by A48, FINSET_1:8;
verum
end;
A59:
{ r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite
proof
defpred S1[
object ,
object ]
means ex
p being
Polynomial of
n,
L ex
x being
Element of
M st
( $1
= x & $2
= p &
x = {p} );
A60:
for
x being
object st
x in M holds
ex
y being
object st
S1[
x,
y]
proof
let x be
object ;
( x in M implies ex y being object st S1[x,y] )
assume A61:
x in M
;
ex y being object st S1[x,y]
then reconsider x9 =
x as
Element of
M ;
consider q being
Polynomial of
n,
L such that
q in I
and A62:
x = {q}
and
q <> 0_ (
n,
L)
by A12, A61;
take
q
;
S1[x,q]
take
q
;
ex x being Element of M st
( x = x & q = q & x = {q} )
take
x9
;
( x = x9 & q = q & x9 = {q} )
thus
x = x9
;
( q = q & x9 = {q} )
thus
q = q
;
x9 = {q}
thus
x9 = {q}
by A62;
verum
end;
consider f being
Function such that A63:
(
dom f = M & ( for
x being
object st
x in M holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A60);
A64:
now for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds
u in rng flet u be
object ;
( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in rng f )assume
u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }
;
u in rng fthen consider r being
Polynomial of
n,
L such that A65:
u = r
and A66:
ex
x being
Element of
M st
x = {r}
;
consider x being
Element of
M such that A67:
x = {r}
by A66;
S1[
x,
f . x]
by A63;
then consider p9 being
Polynomial of
n,
L,
x9 being
Element of
M such that
x9 = x
and A68:
p9 = f . x
and A69:
x = {p9}
;
A70:
f . x in rng f
by A63, FUNCT_1:3;
p9 in {r}
by A67, A69, TARSKI:def 1;
hence
u in rng f
by A65, A70, A68, TARSKI:def 1;
verum end;
then
rng f = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }
by A64, TARSKI:2;
hence
{ r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is
finite
by A46, A63, FINSET_1:8;
verum
end;
then reconsider G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;
G <> {}
then reconsider G = G as non empty finite Subset of (Polynom-Ring (n,L)) by A59;
take
G
; ( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )
proof
let b be
bag of
n;
( b in HT (I,T) implies ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) )
reconsider bb =
b as
Element of
RelStr(#
(Bags n),
(DivOrder n) #)
by PRE_POLY:def 12;
assume
b in HT (
I,
T)
;
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )
then consider bb9 being
Element of
RelStr(#
(Bags n),
(DivOrder n) #)
such that A74:
bb9 in S
and A75:
bb9 <= bb
by A6, DICKSON:def 9;
A76:
[bb9,bb] in DivOrder n
by A75, ORDERS_2:def 5;
reconsider b9 =
bb9 as
bag of
n ;
set N =
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } ;
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } in M
by A74;
then reconsider N =
{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } as
Element of
M ;
take
b9
;
( b9 in HT (G,T) & b9 divides b )
consider r being
Polynomial of
n,
L such that
r in I
and A77:
N = {r}
and
r <> 0_ (
n,
L)
by A12;
r in N
by A77, TARSKI:def 1;
then consider r9 being
Polynomial of
n,
L such that A78:
r = r9
and
r9 in I
and A79:
HM (
r9,
T)
= Monom (
(1. L),
b9)
and A80:
r9 <> 0_ (
n,
L)
and
for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < r9,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
b9) )
;
A81:
r9 in G
by A77, A78;
b9 =
term (HM (r9,T))
by A79, POLYNOM7:10
.=
HT (
r9,
T)
by TERMORD:22
;
hence
(
b9 in HT (
G,
T) &
b9 divides b )
by A76, A80, A81, Def5;
verum
end;
then
HT (I,T) c= multiples (HT (G,T))
by Th28;
hence
G is_Groebner_basis_of I,T
by A45, Th29; G is_reduced_wrt T
now for q being Polynomial of n,L st q in G holds
( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )let q be
Polynomial of
n,
L;
( q in G implies ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T ) )assume A82:
q in G
;
( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )then consider rr being
Polynomial of
n,
L such that A83:
q = rr
and A84:
ex
x being
Element of
M st
x = {rr}
;
consider x being
Element of
M such that A85:
x = {rr}
by A84;
x in M
;
then consider s being
Element of
Bags n such that A86:
x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }
and A87:
s in S
;
rr in x
by A85, TARSKI:def 1;
then consider p being
Polynomial of
n,
L such that A88:
rr = p
and
p in I
and A89:
HM (
p,
T)
= Monom (
(1. L),
s)
and
p <> 0_ (
n,
L)
and A90:
for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < p,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
s) )
by A86;
A91:
1. L =
coefficient (HM (rr,T))
by A88, A89, POLYNOM7:9
.=
HC (
rr,
T)
by TERMORD:22
;
hence
q is_monic_wrt T
by A83;
q is_irreducible_wrt G \ {q},TA92:
s =
term (HM (rr,T))
by A88, A89, POLYNOM7:10
.=
HT (
q,
T)
by A83, TERMORD:22
;
now ( q is_reducible_wrt G \ {q},T implies q is_irreducible_wrt G \ {q},T )reconsider htq =
HT (
q,
T) as
Element of
RelStr(#
(Bags n),
(DivOrder n) #) ;
assume
q is_reducible_wrt G \ {q},
T
;
q is_irreducible_wrt G \ {q},Tthen consider pp being
Polynomial of
n,
L such that A93:
q reduces_to pp,
G \ {q},
T
by POLYRED:def 9;
consider g being
Polynomial of
n,
L such that A94:
g in G \ {q}
and A95:
q reduces_to pp,
g,
T
by A93, POLYRED:def 7;
A96:
g in G
by A94, XBOOLE_0:def 5;
A97:
not
g in {q}
by A94, XBOOLE_0:def 5;
reconsider htg =
HT (
g,
T) as
Element of
RelStr(#
(Bags n),
(DivOrder n) #) ;
consider b being
bag of
n such that A98:
q reduces_to pp,
g,
b,
T
by A95, POLYRED:def 6;
A99:
b in Support q
by A98, POLYRED:def 5;
A100:
ex
s being
bag of
n st
(
s + (HT (g,T)) = b &
pp = q - (((q . b) / (HC (g,T))) * (s *' g)) )
by A98, POLYRED:def 5;
now ( ( b = HT (q,T) & q is_irreducible_wrt G \ {q},T ) or ( b <> HT (q,T) & contradiction ) )per cases
( b = HT (q,T) or b <> HT (q,T) )
;
case A101:
b = HT (
q,
T)
;
q is_irreducible_wrt G \ {q},Tset S9 =
S \ {htq};
consider z being
Polynomial of
n,
L such that A102:
g = z
and A103:
ex
x being
Element of
M st
x = {z}
by A96;
consider x1 being
Element of
M such that A104:
x1 = {z}
by A103;
x1 in M
;
then consider t being
Element of
Bags n such that A105:
x1 = { u where u is Polynomial of n,L : ( u in I & HM (u,T) = Monom ((1. L),t) & u <> 0_ (n,L) & ( for q being Polynomial of n,L holds
( not q in I or not q < u,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),t) ) ) ) }
and A106:
t in S
;
z in x1
by A104, TARSKI:def 1;
then consider p1 being
Polynomial of
n,
L such that A107:
z = p1
and
p1 in I
and A108:
HM (
p1,
T)
= Monom (
(1. L),
t)
and
p1 <> 0_ (
n,
L)
and
for
q being
Polynomial of
n,
L holds
( not
q in I or not
q < p1,
T or not
q <> 0_ (
n,
L) or not
HM (
q,
T)
= Monom (
(1. L),
t) )
by A105;
A109:
t =
term (HM (p1,T))
by A108, POLYNOM7:10
.=
htg
by A102, A107, TERMORD:22
;
then A110:
htg in S \ {htq}
by A106, A109, XBOOLE_0:def 5;
HT (
g,
T)
divides HT (
q,
T)
by A100, A101, PRE_POLY:50;
then
[htg,htq] in DivOrder n
by Def5;
then A111:
htg <= htq
by ORDERS_2:def 5;
S \ {htq} c= S
by XBOOLE_1:36;
then
S \ {htq} c= hti
by A10;
then
S \ {htq} is_Dickson-basis_of hti,
RelStr(#
(Bags n),
(DivOrder n) #)
by A112, DICKSON:def 9;
then
S c= S \ {htq}
by A7;
hence
q is_irreducible_wrt G \ {q},
T
by A87, A92, A115;
verum end; case A116:
b <> HT (
q,
T)
;
contradiction
b <= HT (
q,
T),
T
by A99, TERMORD:def 6;
then
b < HT (
q,
T),
T
by A116, TERMORD:def 3;
then A117:
pp . (HT (q,T)) =
q . (HT (q,T))
by A98, POLYRED:41
.=
1. L
by A83, A91, TERMORD:def 7
;
1. L <> 0. L
;
then A118:
HT (
q,
T)
in Support pp
by A117, POLYNOM1:def 4;
now not HT (q,T) < HT (pp,T),TA119:
b <= HT (
q,
T),
T
by A99, TERMORD:def 6;
assume A120:
HT (
q,
T)
< HT (
pp,
T),
T
;
contradictionthen
HT (
q,
T)
<= HT (
pp,
T),
T
by TERMORD:def 3;
then
(
b <= HT (
pp,
T),
T &
b <> HT (
pp,
T) )
by A116, A119, TERMORD:7, TERMORD:8;
then
b < HT (
pp,
T),
T
by TERMORD:def 3;
then
(
HT (
pp,
T)
in Support q iff
HT (
pp,
T)
in Support pp )
by A98, POLYRED:40;
then
HT (
pp,
T)
<= HT (
q,
T),
T
by A118, TERMORD:def 6;
hence
contradiction
by A120, TERMORD:5;
verum end; then A121:
HT (
pp,
T)
<= HT (
q,
T),
T
by TERMORD:5;
HT (
q,
T)
<= HT (
pp,
T),
T
by A118, TERMORD:def 6;
then
HT (
pp,
T)
= HT (
q,
T)
by A121, TERMORD:7;
then
Monom (
(HC (pp,T)),
(HT (pp,T)))
= Monom (
(1. L),
s)
by A92, A117, TERMORD:def 7;
then A122:
HM (
pp,
T)
= HM (
q,
T)
by A83, A88, A89, TERMORD:def 8;
A123:
now not pp = 0_ (n,L)end; consider m being
Monomial of
n,
L such that A124:
pp = q - (m *' g)
by A95, Th1;
reconsider gg =
g,
qq =
q,
mm =
m as
Element of
(Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider gg =
gg,
qq =
qq,
mm =
mm as
Element of
(Polynom-Ring (n,L)) ;
g in G
by A94, XBOOLE_0:def 5;
then
mm * gg in I
by A45, IDEAL_1:def 2;
then
- (mm * gg) in I
by IDEAL_1:13;
then A125:
qq + (- (mm * gg)) in I
by A45, A82, IDEAL_1:def 1;
mm * gg = m *' g
by POLYNOM1:def 11;
then
q - (m *' g) = qq - (mm * gg)
by Lm2;
then
pp in I
by A124, A125;
hence
contradiction
by A83, A88, A89, A90, A95, A122, A123, POLYRED:43;
verum end; end; end; hence
q is_irreducible_wrt G \ {q},
T
;
verum end; hence
q is_irreducible_wrt G \ {q},
T
;
verum end;
hence
G is_reduced_wrt T
; verum