let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let P be Subset of (Polynom-Ring (n,L)); :: thesis:
assume A1: for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
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) ; :: thesis:
set R = PolyRedRel (P,T);
A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

now :: thesis:

let a, b, c be object ; :: thesis:
assume that
A3: [a,b] in PolyRedRel (P,T) and
A4: [a,c] in PolyRedRel (P,T) ; :: thesis:
consider f, f1 being object such that
A5: f in NonZero (Polynom-Ring (n,L)) and
A6: f1 in the carrier of (Polynom-Ring (n,L)) and
A7: [a,b] = [f,f1] by A3, ZFMISC_1:def 2;
A8: not f in {(0_ (n,L))} by A2, A5, XBOOLE_0:def 5;
reconsider f = f as Polynomial of n,L by A5, POLYNOM1:def 11;
f <> 0_ (n,L) by A8, TARSKI:def 1;
then reconsider f = f as non-zero Polynomial of n,L by POLYNOM7:def 1;
reconsider f1 = f1 as Polynomial of n,L by A6, POLYNOM1:def 11;
f reduces_to f1,P,T by A3, A7, POLYRED:def 13;
then consider g1 being Polynomial of n,L such that
A9: g1 in P and
A10: f reduces_to f1,g1,T by POLYRED:def 7;
ex b1 being bag of n st f reduces_to f1,g1,b1,T by A10, POLYRED:def 6;
then A11: g1 <> 0_ (n,L) by POLYRED:def 5;
consider f9, f2 being object such that
f9 in NonZero (Polynom-Ring (n,L)) and
A12: f2 in the carrier of (Polynom-Ring (n,L)) and
A13: [a,c] = [f9,f2] by A4, ZFMISC_1:def 2;
reconsider f2 = f2 as Polynomial of n,L by A12, POLYNOM1:def 11;
A14: f2 = c by A13, XTUPLE_0:1;
reconsider g1 = g1 as non-zero Polynomial of n,L by A11, POLYNOM7:def 1;
consider m1 being Monomial of n,L such that
A15: f1 = f - (m1 *' g1) and
A16: not HT ((m1 *' g1),T) in Support f1 and
HT ((m1 *' g1),T) <= HT (f,T),T by A10, GROEB_1:2;
A17: f9 = a by A13, XTUPLE_0:1;
A18: f9 = a by A13, XTUPLE_0:1
.= f by A7, XTUPLE_0:1 ;
then f reduces_to f2,P,T by A4, A13, POLYRED:def 13;
then consider g2 being Polynomial of n,L such that
A19: g2 in P and
A20: f reduces_to f2,g2,T by POLYRED:def 7;
ex b2 being bag of n st f reduces_to f2,g2,b2,T by A20, POLYRED:def 6;
then A21: g2 <> 0_ (n,L) by POLYRED:def 5;
then reconsider g2 = g2 as non-zero Polynomial of n,L by POLYNOM7:def 1;
consider m2 being Monomial of n,L such that
A22: f2 = f - (m2 *' g2) and
A23: not HT ((m2 *' g2),T) in Support f2 and
HT ((m2 *' g2),T) <= HT (f,T),T by A20, GROEB_1:2;
set mg1 = m1 *' g1;
set mg2 = m2 *' g2;
A24: f1 = b by A7, XTUPLE_0:1;

now :: thesis:

per cases ;

case m1 = 0_ (n,L) ; :: thesis:

then f1 = f - (0_ (n,L)) by A15, POLYRED:5
.= f by POLYRED:4 ;
then A25: PolyRedRel (P,T) reduces b,c by A4, A18, A24, A17, REWRITE1:15;
PolyRedRel (P,T) reduces c,c by REWRITE1:12;
hence b,c are_convergent_wrt PolyRedRel (P,T) by A25, REWRITE1:def 7; :: thesis:

end;

case m2 = 0_ (n,L) ; :: thesis:

then f2 = f - (0_ (n,L)) by A22, POLYRED:5
.= f by POLYRED:4 ;
then A26: PolyRedRel (P,T) reduces c,b by A3, A18, A14, A17, REWRITE1:15;
PolyRedRel (P,T) reduces b,b by REWRITE1:12;
hence b,c are_convergent_wrt PolyRedRel (P,T) by A26, REWRITE1:def 7; :: thesis:

end;

case ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) ; :: thesis:

then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by POLYNOM7:def 1;
(HT (m1,T)) + (HT (g1,T)) in Support (m1 *' g1) by TERMORD:29;
then A27: m1 *' g1 <> 0_ (n,L) by POLYNOM7:1;
(HT (m2,T)) + (HT (g2,T)) in Support (m2 *' g2) by TERMORD:29;
then A28: m2 *' g2 <> 0_ (n,L) by POLYNOM7:1;
A29: HC (g2,T) <> 0. L ;
A30: - (- (m1 *' g1)) = m1 *' g1 by POLYNOM1:19;
A31: f2 - f1 = (f + (- (m2 *' g2))) - (f - (m1 *' g1)) by A15, A22, POLYNOM1:def 7
.= (f + (- (m2 *' g2))) - (f + (- (m1 *' g1))) by POLYNOM1:def 7
.= (f + (- (m2 *' g2))) + (- (f + (- (m1 *' g1)))) by POLYNOM1:def 7
.= (f + (- (m2 *' g2))) + ((- f) + (- (- (m1 *' g1)))) by POLYRED:1
.= f + ((- (m2 *' g2)) + ((- f) + (m1 *' g1))) by A30, POLYNOM1:21
.= f + ((- f) + ((- (m2 *' g2)) + (m1 *' g1))) by POLYNOM1:21
.= (f + (- f)) + ((- (m2 *' g2)) + (m1 *' g1)) by POLYNOM1:21
.= (0_ (n,L)) + ((- (m2 *' g2)) + (m1 *' g1)) by POLYRED:3
.= (m1 *' g1) + (- (m2 *' g2)) by POLYRED:2
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 7 ;
A32: HC (g1,T) <> 0. L ;
A33: - (- (m1 *' g1)) = m1 *' g1 by POLYNOM1:19;
PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)

proof

now :: thesis:

per cases ) - (m2 *' g2) = 0_ (n,L) or (m1 *' g1) - (m2 *' g2) <> 0_ (n,L) ) ;

case (m1 *' g1) - (m2 *' g2) = 0_ (n,L) ; :: thesis:

hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A31, REWRITE1:12; :: thesis:

end;

case A34: (m1 *' g1) - (m2 *' g2) <> 0_ (n,L) ; :: thesis:

now :: thesis:

per cases ;

case g1 = g2 ; :: thesis:

then f2 - f1 = (m1 *' g1) + (- (m2 *' g1)) by A31, POLYNOM1:def 7
.= (g1 *' m1) + ((- m2) *' g1) by POLYRED:6
.= (m1 + (- m2)) *' g1 by POLYNOM1:26 ;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A9, POLYRED:45; :: thesis:

end;

case A35: g1 <> g2 ; :: thesis:

now :: thesis:

per cases ;

case A36: HT ((m1 *' g1),T) <> HT ((m2 *' g2),T) ; :: thesis:

now :: thesis:

per cases ;

case HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T ; :: thesis:

then not HT ((m1 *' g1),T) <= HT ((m2 *' g2),T),T by TERMORD:5;
then not HT ((m1 *' g1),T) in Support (m2 *' g2) by TERMORD:def 6;
then A37: (m2 *' g2) . (HT ((m1 *' g1),T)) = 0. L by POLYNOM1:def 4;
A38: ((m1 *' g1) - (m2 *' g2)) . (HT ((m1 *' g1),T)) = ((m1 *' g1) + (- (m2 *' g2))) . (HT ((m1 *' g1),T)) by POLYNOM1:def 7
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + ((- (m2 *' g2)) . (HT ((m1 *' g1),T))) by POLYNOM1:15
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + (- ((m2 *' g2) . (HT ((m1 *' g1),T)))) by POLYNOM1:17
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + (0. L) by A37, RLVECT_1:12
.= (m1 *' g1) . (HT ((m1 *' g1),T)) by RLVECT_1:def 4
.= HC ((m1 *' g1),T) by TERMORD:def 7 ;
then ((m1 *' g1) - (m2 *' g2)) . (HT ((m1 *' g1),T)) <> 0. L by A27, TERMORD:17;
then A39: HT ((m1 *' g1),T) in Support ((m1 *' g1) - (m2 *' g2)) by POLYNOM1:def 4;
A40: (HT (m1,T)) + (HT (g1,T)) = HT ((m1 *' g1),T) by TERMORD:31;
((m1 *' g1) - (m2 *' g2)) - (((((m1 *' g1) - (m2 *' g2)) . (HT ((m1 *' g1),T))) / (HC (g1,T))) * ((HT (m1,T)) *' g1)) = ((m1 *' g1) - (m2 *' g2)) - ((((HC (m1,T)) * (HC (g1,T))) / (HC (g1,T))) * ((HT (m1,T)) *' g1)) by A38, TERMORD:32
.= ((m1 *' g1) - (m2 *' g2)) - ((((HC (m1,T)) * (HC (g1,T))) * ((HC (g1,T)) ")) * ((HT (m1,T)) *' g1))
.= ((m1 *' g1) - (m2 *' g2)) - (((HC (m1,T)) * ((HC (g1,T)) * ((HC (g1,T)) "))) * ((HT (m1,T)) *' g1)) by GROUP_1:def 3
.= ((m1 *' g1) - (m2 *' g2)) - (((HC (m1,T)) * (1. L)) * ((HT (m1,T)) *' g1)) by A32, VECTSP_1:def 10
.= ((m1 *' g1) - (m2 *' g2)) - ((HC (m1,T)) * ((HT (m1,T)) *' g1))
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom ((HC (m1,T)),(HT (m1,T)))) *' g1) by POLYRED:22
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom ((coefficient m1),(HT (m1,T)))) *' g1) by TERMORD:23
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom ((coefficient m1),(term m1))) *' g1) by TERMORD:23
.= ((m1 *' g1) - (m2 *' g2)) - (m1 *' g1) by POLYNOM7:11
.= ((m1 *' g1) + (- (m2 *' g2))) - (m1 *' g1) by POLYNOM1:def 7
.= ((m1 *' g1) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:def 7
.= ((m1 *' g1) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:21
.= (0_ (n,L)) + (- (m2 *' g2)) by POLYRED:3
.= - (m2 *' g2) by POLYRED:2 ;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),g1, HT ((m1 *' g1),T),T by A11, A34, A39, A40, POLYRED:def 5;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),g1,T by POLYRED:def 6;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),P,T by A9, POLYRED:def 7;
then [((m1 *' g1) - (m2 *' g2)),(- (m2 *' g2))] in PolyRedRel (P,T) by POLYRED:def 13;
then A41: PolyRedRel (P,T) reduces (m1 *' g1) - (m2 *' g2), - (m2 *' g2) by REWRITE1:15;
PolyRedRel (P,T) reduces (- m2) *' g2, 0_ (n,L) by A19, POLYRED:45;
then PolyRedRel (P,T) reduces - (m2 *' g2), 0_ (n,L) by POLYRED:6;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A31, A41, REWRITE1:16; :: thesis:

end;

case not HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T ; :: thesis:

then HT ((m1 *' g1),T) <= HT ((m2 *' g2),T),T by TERMORD:5;
then HT ((m1 *' g1),T) < HT ((m2 *' g2),T),T by A36, TERMORD:def 3;
then not HT ((m2 *' g2),T) <= HT ((m1 *' g1),T),T by TERMORD:5;
then not HT ((m2 *' g2),T) in Support (m1 *' g1) by TERMORD:def 6;
then A42: (m1 *' g1) . (HT ((m2 *' g2),T)) = 0. L by POLYNOM1:def 4;
A43: ((m2 *' g2) - (m1 *' g1)) . (HT ((m2 *' g2),T)) = ((m2 *' g2) + (- (m1 *' g1))) . (HT ((m2 *' g2),T)) by POLYNOM1:def 7
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + ((- (m1 *' g1)) . (HT ((m2 *' g2),T))) by POLYNOM1:15
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + (- ((m1 *' g1) . (HT ((m2 *' g2),T)))) by POLYNOM1:17
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + (0. L) by A42, RLVECT_1:12
.= (m2 *' g2) . (HT ((m2 *' g2),T)) by RLVECT_1:def 4
.= HC ((m2 *' g2),T) by TERMORD:def 7 ;
then ((m2 *' g2) - (m1 *' g1)) . (HT ((m2 *' g2),T)) <> 0. L by A28, TERMORD:17;
then A44: HT ((m2 *' g2),T) in Support ((m2 *' g2) - (m1 *' g1)) by POLYNOM1:def 4;
reconsider x = - (0_ (n,L)) as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A45: (HT (m2,T)) + (HT (g2,T)) = HT ((m2 *' g2),T) by TERMORD:31;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;
then A46: x + (0. (Polynom-Ring (n,L))) = (- (0_ (n,L))) + (0_ (n,L)) by POLYNOM1:def 11
.= 0_ (n,L) by POLYRED:3
.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;

A47: now :: thesis:

assume (m2 *' g2) - (m1 *' g1) = 0_ (n,L) ; :: thesis:
then - ((m2 *' g2) + (- (m1 *' g1))) = - (0_ (n,L)) by POLYNOM1:def 7;
then (- (m2 *' g2)) + (- (- (m1 *' g1))) = - (0_ (n,L)) by POLYRED:1;
then (m1 *' g1) + (- (m2 *' g2)) = - (0. (Polynom-Ring (n,L))) by A33, A46, RLVECT_1:6
.= 0. (Polynom-Ring (n,L)) by RLVECT_1:12
.= 0_ (n,L) by POLYNOM1:def 11 ;
hence contradiction by A34, POLYNOM1:def 7; :: thesis:

end;

((m2 *' g2) - (m1 *' g1)) - (((((m2 *' g2) - (m1 *' g1)) . (HT ((m2 *' g2),T))) / (HC (g2,T))) * ((HT (m2,T)) *' g2)) = ((m2 *' g2) - (m1 *' g1)) - ((((HC (m2,T)) * (HC (g2,T))) / (HC (g2,T))) * ((HT (m2,T)) *' g2)) by A43, TERMORD:32
.= ((m2 *' g2) - (m1 *' g1)) - ((((HC (m2,T)) * (HC (g2,T))) * ((HC (g2,T)) ")) * ((HT (m2,T)) *' g2))
.= ((m2 *' g2) - (m1 *' g1)) - (((HC (m2,T)) * ((HC (g2,T)) * ((HC (g2,T)) "))) * ((HT (m2,T)) *' g2)) by GROUP_1:def 3
.= ((m2 *' g2) - (m1 *' g1)) - (((HC (m2,T)) * (1. L)) * ((HT (m2,T)) *' g2)) by A29, VECTSP_1:def 10
.= ((m2 *' g2) - (m1 *' g1)) - ((HC (m2,T)) * ((HT (m2,T)) *' g2))
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom ((HC (m2,T)),(HT (m2,T)))) *' g2) by POLYRED:22
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom ((coefficient m2),(HT (m2,T)))) *' g2) by TERMORD:23
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom ((coefficient m2),(term m2))) *' g2) by TERMORD:23
.= ((m2 *' g2) - (m1 *' g1)) - (m2 *' g2) by POLYNOM7:11
.= ((m2 *' g2) + (- (m1 *' g1))) - (m2 *' g2) by POLYNOM1:def 7
.= ((m2 *' g2) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:def 7
.= ((m2 *' g2) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:21
.= (0_ (n,L)) + (- (m1 *' g1)) by POLYRED:3
.= - (m1 *' g1) by POLYRED:2 ;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),g2, HT ((m2 *' g2),T),T by A21, A44, A45, A47, POLYRED:def 5;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),g2,T by POLYRED:def 6;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),P,T by A19, POLYRED:def 7;
then [((m2 *' g2) - (m1 *' g1)),(- (m1 *' g1))] in PolyRedRel (P,T) by POLYRED:def 13;
then A48: PolyRedRel (P,T) reduces (m2 *' g2) - (m1 *' g1), - (m1 *' g1) by REWRITE1:15;
A49: - (1_ (n,L)) = - ((1. L) | (n,L)) by POLYNOM7:20
.= (- (1. L)) | (n,L) by Th16 ;
PolyRedRel (P,T) reduces (- m1) *' g1, 0_ (n,L) by A9, POLYRED:45;
then PolyRedRel (P,T) reduces - (m1 *' g1), 0_ (n,L) by POLYRED:6;
then PolyRedRel (P,T) reduces (m2 *' g2) - (m1 *' g1), 0_ (n,L) by A48, REWRITE1:16;
then A50: PolyRedRel (P,T) reduces (- (1_ (n,L))) *' ((m2 *' g2) - (m1 *' g1)),(- (1_ (n,L))) *' (0_ (n,L)) by A49, POLYRED:47;
(- (1_ (n,L))) *' ((m2 *' g2) - (m1 *' g1)) = (- (1_ (n,L))) *' ((m2 *' g2) + (- (m1 *' g1))) by POLYNOM1:def 7
.= ((- (1_ (n,L))) *' (m2 *' g2)) + ((- (1_ (n,L))) *' (- (m1 *' g1))) by POLYNOM1:26
.= (- ((1_ (n,L)) *' (m2 *' g2))) + ((- (1_ (n,L))) *' (- (m1 *' g1))) by POLYRED:6
.= ((1_ (n,L)) *' (- (m2 *' g2))) + ((- (1_ (n,L))) *' (- (m1 *' g1))) by POLYRED:6
.= ((1_ (n,L)) *' (- (m2 *' g2))) + (- ((1_ (n,L)) *' (- (m1 *' g1)))) by POLYRED:6
.= ((1_ (n,L)) *' (- (m2 *' g2))) + ((1_ (n,L)) *' (- (- (m1 *' g1)))) by POLYRED:6
.= (- (m2 *' g2)) + ((1_ (n,L)) *' (m1 *' g1)) by A33, POLYNOM1:30
.= (m1 *' g1) + (- (m2 *' g2)) by POLYNOM1:30
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 7 ;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A31, A50, POLYNOM1:28; :: thesis:

end;

hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis:

end;

case A51: HT ((m1 *' g1),T) = HT ((m2 *' g2),T) ; :: thesis:

(f - (m2 *' g2)) . (HT ((m2 *' g2),T)) = 0. L by A22, A23, POLYNOM1:def 4;
then (f + (- (m2 *' g2))) . (HT ((m2 *' g2),T)) = 0. L by POLYNOM1:def 7;
then (f . (HT ((m2 *' g2),T))) + ((- (m2 *' g2)) . (HT ((m2 *' g2),T))) = 0. L by POLYNOM1:15;
then (f . (HT ((m2 *' g2),T))) + (- ((m2 *' g2) . (HT ((m2 *' g2),T)))) = 0. L by POLYNOM1:17;
then A52: f . (HT ((m2 *' g2),T)) = - (- ((m2 *' g2) . (HT ((m2 *' g2),T)))) by RLVECT_1:6;
(f - (m1 *' g1)) . (HT ((m1 *' g1),T)) = 0. L by A15, A16, POLYNOM1:def 4;
then (f + (- (m1 *' g1))) . (HT ((m1 *' g1),T)) = 0. L by POLYNOM1:def 7;
then (f . (HT ((m1 *' g1),T))) + ((- (m1 *' g1)) . (HT ((m1 *' g1),T))) = 0. L by POLYNOM1:15;
then (f . (HT ((m1 *' g1),T))) + (- ((m1 *' g1) . (HT ((m1 *' g1),T)))) = 0. L by POLYNOM1:17;
then A53: f . (HT ((m1 *' g1),T)) = - (- ((m1 *' g1) . (HT ((m1 *' g1),T)))) by RLVECT_1:6;
HC ((m1 *' g1),T) = (m1 *' g1) . (HT ((m1 *' g1),T)) by TERMORD:def 7
.= f . (HT ((m1 *' g1),T)) by A53, RLVECT_1:17
.= (m2 *' g2) . (HT ((m2 *' g2),T)) by A51, A52, RLVECT_1:17
.= HC ((m2 *' g2),T) by TERMORD:def 7 ;
then HM ((m1 *' g1),T) = Monom ((HC ((m2 *' g2),T)),(HT ((m2 *' g2),T))) by A51, TERMORD:def 8
.= HM ((m2 *' g2),T) by TERMORD:def 8 ;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A1, A9, A19, A31, A35; :: thesis:

end;

hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis:

end;

hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis:

end;

hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis:

end;

hence b,c are_convergent_wrt PolyRedRel (P,T) by A24, A14, POLYRED:50, REWRITE1:40; :: thesis:

end;

hence b,c are_convergent_wrt PolyRedRel (P,T) ; :: thesis:

end;

then PolyRedRel (P,T) is locally-confluent by REWRITE1:def 24;
hence P is_Groebner_basis_wrt T by GROEB_1:def 3; :: thesis: