let n be Element of NAT ; :: thesis: 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))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let T be connected admissible TermOrder of n; :: thesis: 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))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= I & HT (I,T) c= multiples (HT (P,T)) implies P is_Groebner_basis_of I,T )

assume A1: P c= I ; :: thesis: ( not HT (I,T) c= multiples (HT (P,T)) or P is_Groebner_basis_of I,T )

set R = PolyRedRel (P,T);

assume A2: HT (I,T) c= multiples (HT (P,T)) ; :: thesis: P is_Groebner_basis_of I,T

A3: for f being Polynomial of n,L st f in I & f <> 0_ (n,L) holds

f is_reducible_wrt P,T

A13: for f being Polynomial of n,L st f in I holds

PolyRedRel (P,T) reduces f, 0_ (n,L)

hence P is_Groebner_basis_of I,T by A22; :: thesis: verum

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

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let T be connected admissible TermOrder of n; :: thesis: 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))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))

for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds

G is_Groebner_basis_of I,T

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= I & HT (I,T) c= multiples (HT (P,T)) implies P is_Groebner_basis_of I,T )

assume A1: P c= I ; :: thesis: ( not HT (I,T) c= multiples (HT (P,T)) or P is_Groebner_basis_of I,T )

set R = PolyRedRel (P,T);

assume A2: HT (I,T) c= multiples (HT (P,T)) ; :: thesis: P is_Groebner_basis_of I,T

A3: for f being Polynomial of n,L st f in I & f <> 0_ (n,L) holds

f is_reducible_wrt P,T

proof

A12:
PolyRedRel (P,T) c= PolyRedRel (I,T)
by A1, Th4;
let f be Polynomial of n,L; :: thesis: ( f in I & f <> 0_ (n,L) implies f is_reducible_wrt P,T )

assume that

A4: f in I and

A5: f <> 0_ (n,L) ; :: thesis: f is_reducible_wrt P,T

HT (f,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A4, A5;

then HT (f,T) in multiples (HT (P,T)) by A2;

then ex b being Element of Bags n st

( b = HT (f,T) & ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) ;

then consider b9 being bag of n such that

A6: b9 in HT (P,T) and

A7: b9 divides HT (f,T) ;

consider p being Polynomial of n,L such that

A8: b9 = HT (p,T) and

A9: p in P and

A10: p <> 0_ (n,L) by A6;

consider s being bag of n such that

A11: b9 + s = HT (f,T) by A7, TERMORD:1;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p));

Support f <> {} by A5, POLYNOM7:1;

then HT (f,T) in Support f by TERMORD:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p, HT (f,T),T by A5, A8, A10, A11, POLYRED:def 5;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p,T by POLYRED:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),P,T by A9, POLYRED:def 7;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;assume that

A4: f in I and

A5: f <> 0_ (n,L) ; :: thesis: f is_reducible_wrt P,T

HT (f,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A4, A5;

then HT (f,T) in multiples (HT (P,T)) by A2;

then ex b being Element of Bags n st

( b = HT (f,T) & ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) ;

then consider b9 being bag of n such that

A6: b9 in HT (P,T) and

A7: b9 divides HT (f,T) ;

consider p being Polynomial of n,L such that

A8: b9 = HT (p,T) and

A9: p in P and

A10: p <> 0_ (n,L) by A6;

consider s being bag of n such that

A11: b9 + s = HT (f,T) by A7, TERMORD:1;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p));

Support f <> {} by A5, POLYNOM7:1;

then HT (f,T) in Support f by TERMORD:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p, HT (f,T),T by A5, A8, A10, A11, POLYRED:def 5;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),p,T by POLYRED:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * (s *' p)),P,T by A9, POLYRED:def 7;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

A13: for f being Polynomial of n,L st f in I holds

PolyRedRel (P,T) reduces f, 0_ (n,L)

proof

then A22:
P -Ideal = I
by A1, Lm7;
let f be Polynomial of n,L; :: thesis: ( f in I implies PolyRedRel (P,T) reduces f, 0_ (n,L) )

assume A14: f in I ; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)

end;assume A14: f in I ; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)

per cases
( f = 0_ (n,L) or f <> 0_ (n,L) )
;

end;

suppose
f <> 0_ (n,L)
; :: thesis: PolyRedRel (P,T) reduces f, 0_ (n,L)

then
f is_reducible_wrt P,T
by A3, A14;

then consider v being Polynomial of n,L such that

A15: f reduces_to v,P,T by POLYRED:def 9;

[f,v] in PolyRedRel (P,T) by A15, POLYRED:def 13;

then f in field (PolyRedRel (P,T)) by RELAT_1:15;

then f has_a_normal_form_wrt PolyRedRel (P,T) by REWRITE1:def 14;

then consider g being object such that

A16: g is_a_normal_form_of f, PolyRedRel (P,T) by REWRITE1:def 11;

A17: PolyRedRel (P,T) reduces f,g by A16, REWRITE1:def 6;

then reconsider g9 = g as Polynomial of n,L by Lm4;

reconsider ff = f, gg = g9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider ff = ff, gg = gg as Element of (Polynom-Ring (n,L)) ;

f - g9 = ff - gg by Lm2;

then ff - gg in I -Ideal by A12, A17, POLYRED:59, REWRITE1:22;

then ff - gg in I by IDEAL_1:44;

then A18: (ff - gg) - ff in I by A14, IDEAL_1:16;

(ff - gg) - ff = (ff + (- gg)) - ff

.= (ff + (- gg)) + (- ff)

.= (ff + (- ff)) + (- gg) by RLVECT_1:def 3

.= (0. (Polynom-Ring (n,L))) + (- gg) by RLVECT_1:5

.= - gg by ALGSTR_1:def 2 ;

then - (- gg) in I by A18, IDEAL_1:14;

then A19: g in I by RLVECT_1:17;

assume not PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: contradiction

then g <> 0_ (n,L) by A16, REWRITE1:def 6;

then g9 is_reducible_wrt P,T by A3, A19;

then consider u being Polynomial of n,L such that

A20: g9 reduces_to u,P,T by POLYRED:def 9;

A21: [g9,u] in PolyRedRel (P,T) by A20, POLYRED:def 13;

g is_a_normal_form_wrt PolyRedRel (P,T) by A16, REWRITE1:def 6;

hence contradiction by A21, REWRITE1:def 5; :: thesis: verum

end;then consider v being Polynomial of n,L such that

A15: f reduces_to v,P,T by POLYRED:def 9;

[f,v] in PolyRedRel (P,T) by A15, POLYRED:def 13;

then f in field (PolyRedRel (P,T)) by RELAT_1:15;

then f has_a_normal_form_wrt PolyRedRel (P,T) by REWRITE1:def 14;

then consider g being object such that

A16: g is_a_normal_form_of f, PolyRedRel (P,T) by REWRITE1:def 11;

A17: PolyRedRel (P,T) reduces f,g by A16, REWRITE1:def 6;

then reconsider g9 = g as Polynomial of n,L by Lm4;

reconsider ff = f, gg = g9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider ff = ff, gg = gg as Element of (Polynom-Ring (n,L)) ;

f - g9 = ff - gg by Lm2;

then ff - gg in I -Ideal by A12, A17, POLYRED:59, REWRITE1:22;

then ff - gg in I by IDEAL_1:44;

then A18: (ff - gg) - ff in I by A14, IDEAL_1:16;

(ff - gg) - ff = (ff + (- gg)) - ff

.= (ff + (- gg)) + (- ff)

.= (ff + (- ff)) + (- gg) by RLVECT_1:def 3

.= (0. (Polynom-Ring (n,L))) + (- gg) by RLVECT_1:5

.= - gg by ALGSTR_1:def 2 ;

then - (- gg) in I by A18, IDEAL_1:14;

then A19: g in I by RLVECT_1:17;

assume not PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: contradiction

then g <> 0_ (n,L) by A16, REWRITE1:def 6;

then g9 is_reducible_wrt P,T by A3, A19;

then consider u being Polynomial of n,L such that

A20: g9 reduces_to u,P,T by POLYRED:def 9;

A21: [g9,u] in PolyRedRel (P,T) by A20, POLYRED:def 13;

g is_a_normal_form_wrt PolyRedRel (P,T) by A16, REWRITE1:def 6;

hence contradiction by A21, REWRITE1:def 5; :: thesis: verum

now :: thesis: for a, b, c being object st [a,b] in PolyRedRel (P,T) & [a,c] in PolyRedRel (P,T) holds

b,c are_convergent_wrt PolyRedRel (P,T)

then
PolyRedRel (P,T) is locally-confluent
by REWRITE1:def 24;b,c are_convergent_wrt PolyRedRel (P,T)

let a, b, c be object ; :: thesis: ( [a,b] in PolyRedRel (P,T) & [a,c] in PolyRedRel (P,T) implies b,c are_convergent_wrt PolyRedRel (P,T) )

assume that

A23: [a,b] in PolyRedRel (P,T) and

A24: [a,c] in PolyRedRel (P,T) ; :: thesis: b,c are_convergent_wrt PolyRedRel (P,T)

consider a9, b9 being object such that

a9 in NonZero (Polynom-Ring (n,L)) and

A25: b9 in the carrier of (Polynom-Ring (n,L)) and

A26: [a,b] = [a9,b9] by A23, ZFMISC_1:def 2;

A27: b9 = b by A26, XTUPLE_0:1;

a,b are_convertible_wrt PolyRedRel (P,T) by A23, REWRITE1:29;

then A28: b,a are_convertible_wrt PolyRedRel (P,T) by REWRITE1:31;

consider aa, c9 being object such that

aa in NonZero (Polynom-Ring (n,L)) and

A29: c9 in the carrier of (Polynom-Ring (n,L)) and

A30: [a,c] = [aa,c9] by A24, ZFMISC_1:def 2;

A31: c9 = c by A30, XTUPLE_0:1;

reconsider b9 = b9, c9 = c9 as Polynomial of n,L by A25, A29, POLYNOM1:def 11;

reconsider bb = b9, cc = c9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider bb = bb, cc = cc as Element of (Polynom-Ring (n,L)) ;

a,c are_convertible_wrt PolyRedRel (P,T) by A24, REWRITE1:29;

then bb,cc are_congruent_mod I by A22, A27, A31, A28, POLYRED:57, REWRITE1:30;

then A32: bb - cc in I by POLYRED:def 14;

b9 - c9 = bb - cc by Lm2;

hence b,c are_convergent_wrt PolyRedRel (P,T) by A13, A27, A31, A32, POLYRED:50; :: thesis: verum

end;assume that

A23: [a,b] in PolyRedRel (P,T) and

A24: [a,c] in PolyRedRel (P,T) ; :: thesis: b,c are_convergent_wrt PolyRedRel (P,T)

consider a9, b9 being object such that

a9 in NonZero (Polynom-Ring (n,L)) and

A25: b9 in the carrier of (Polynom-Ring (n,L)) and

A26: [a,b] = [a9,b9] by A23, ZFMISC_1:def 2;

A27: b9 = b by A26, XTUPLE_0:1;

a,b are_convertible_wrt PolyRedRel (P,T) by A23, REWRITE1:29;

then A28: b,a are_convertible_wrt PolyRedRel (P,T) by REWRITE1:31;

consider aa, c9 being object such that

aa in NonZero (Polynom-Ring (n,L)) and

A29: c9 in the carrier of (Polynom-Ring (n,L)) and

A30: [a,c] = [aa,c9] by A24, ZFMISC_1:def 2;

A31: c9 = c by A30, XTUPLE_0:1;

reconsider b9 = b9, c9 = c9 as Polynomial of n,L by A25, A29, POLYNOM1:def 11;

reconsider bb = b9, cc = c9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider bb = bb, cc = cc as Element of (Polynom-Ring (n,L)) ;

a,c are_convertible_wrt PolyRedRel (P,T) by A24, REWRITE1:29;

then bb,cc are_congruent_mod I by A22, A27, A31, A28, POLYRED:57, REWRITE1:30;

then A32: bb - cc in I by POLYRED:def 14;

b9 - c9 = bb - cc by Lm2;

hence b,c are_convergent_wrt PolyRedRel (P,T) by A13, A27, A31, A32, POLYRED:50; :: thesis: verum

hence P is_Groebner_basis_of I,T by A22; :: thesis: verum