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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( 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) ) holds
P is_Groebner_basis_wrt T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( 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) ) holds
P is_Groebner_basis_wrt T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st ( 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) ) holds
P is_Groebner_basis_wrt T
let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( 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) ) implies P is_Groebner_basis_wrt T )
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: P is_Groebner_basis_wrt T
set R = PolyRedRel (P,T);
A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 27;
now
let a, b, c be set ; :: thesis: ( [a,b] in PolyRedRel (P,T) & [a,c] in PolyRedRel (P,T) implies b,c are_convergent_wrt PolyRedRel (P,T) )
assume that
A3: [a,b] in PolyRedRel (P,T) and
A4: [a,c] in PolyRedRel (P,T) ; :: thesis: b,c are_convergent_wrt PolyRedRel (P,T)
consider f, f1 being set 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 27;
f <> 0_ (n,L) by A8, TARSKI:def 1;
then reconsider f = f as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider f1 = f1 as Polynomial of n,L by A6, POLYNOM1:def 27;
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 set 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 27;
A14: f2 = [a,c] `2 by A13, MCART_1:def 2
.= c by MCART_1:def 2 ;
reconsider g1 = g1 as non-zero Polynomial of n,L by A11, POLYNOM7:def 2;
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,c] `1 by A13, MCART_1:def 1
.= a by MCART_1:def 1 ;
A18: f9 = [a,c] `1 by A13, MCART_1:def 1
.= a by MCART_1:def 1
.= [f,f1] `1 by A7, MCART_1:def 1
.= f by MCART_1:def 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 2;
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 = [a,b] `2 by A7, MCART_1:def 2
.= b by MCART_1:def 2 ;
now
per cases ( m1 = 0_ (n,L) or m2 = 0_ (n,L) or ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) ) ;
case ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) ; :: thesis: b,c are_convergent_wrt PolyRedRel (P,T)
then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
(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: f2 - f1 = (f + (- (m2 *' g2))) - (f - (m1 *' g1)) by A15, A22, 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
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 23 ;
A31: HC (g1,T) <> 0. L ;
PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
proof
now
per cases ( (m1 *' g1) - (m2 *' g2) = 0_ (n,L) or (m1 *' g1) - (m2 *' g2) <> 0_ (n,L) ) ;
case (m1 *' g1) - (m2 *' g2) = 0_ (n,L) ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A30, REWRITE1:13; :: thesis: verum
end;
case A32: (m1 *' g1) - (m2 *' g2) <> 0_ (n,L) ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
now
per cases ( g1 = g2 or g1 <> g2 ) ;
case g1 = g2 ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
then f2 - f1 = (m1 *' g1) + (- (m2 *' g1)) by A30, POLYNOM1:def 23
.= (g1 *' m1) + ((- m2) *' g1) by POLYRED:6
.= (m1 + (- m2)) *' g1 by POLYNOM1:85 ;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A9, POLYRED:45; :: thesis: verum
end;
case A33: g1 <> g2 ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
now
per cases ( HT ((m1 *' g1),T) <> HT ((m2 *' g2),T) or HT ((m1 *' g1),T) = HT ((m2 *' g2),T) ) ;
case A34: HT ((m1 *' g1),T) <> HT ((m2 *' g2),T) ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
now
per cases ( HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T or not HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T ) ;
case HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
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 A35: (m2 *' g2) . (HT ((m1 *' g1),T)) = 0. L by POLYNOM1:def 9;
A36: ((m1 *' g1) - (m2 *' g2)) . (HT ((m1 *' g1),T)) = ((m1 *' g1) + (- (m2 *' g2))) . (HT ((m1 *' g1),T)) by POLYNOM1:def 23
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + ((- (m2 *' g2)) . (HT ((m1 *' g1),T))) by POLYNOM1:def 21
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + (- ((m2 *' g2) . (HT ((m1 *' g1),T)))) by POLYNOM1:def 22
.= ((m1 *' g1) . (HT ((m1 *' g1),T))) + (0. L) by A35, RLVECT_1:25
.= (m1 *' g1) . (HT ((m1 *' g1),T)) by RLVECT_1:def 7
.= HC ((m1 *' g1),T) by TERMORD:def 7 ;
then ((m1 *' g1) - (m2 *' g2)) . (HT ((m1 *' g1),T)) <> 0. L by A27, TERMORD:17;
then A37: HT ((m1 *' g1),T) in Support ((m1 *' g1) - (m2 *' g2)) by POLYNOM1:def 9;
A38: (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 A36, TERMORD:32
.= ((m1 *' g1) - (m2 *' g2)) - ((((HC (m1,T)) * (HC (g1,T))) * ((HC (g1,T)) ")) * ((HT (m1,T)) *' g1)) by VECTSP_1:def 23
.= ((m1 *' g1) - (m2 *' g2)) - (((HC (m1,T)) * ((HC (g1,T)) * ((HC (g1,T)) "))) * ((HT (m1,T)) *' g1)) by GROUP_1:def 4
.= ((m1 *' g1) - (m2 *' g2)) - (((HC (m1,T)) * (1. L)) * ((HT (m1,T)) *' g1)) by A31, VECTSP_1:def 22
.= ((m1 *' g1) - (m2 *' g2)) - ((HC (m1,T)) * ((HT (m1,T)) *' g1)) by VECTSP_1:def 19
.= ((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 23
.= ((m1 *' g1) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:def 23
.= ((m1 *' g1) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:80
.= (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, A32, A37, A38, 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 A39: PolyRedRel (P,T) reduces (m1 *' g1) - (m2 *' g2), - (m2 *' g2) by REWRITE1:16;
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 A30, A39, REWRITE1:17; :: thesis: verum
end;
case not HT ((m2 *' g2),T) < HT ((m1 *' g1),T),T ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
then HT ((m1 *' g1),T) <= HT ((m2 *' g2),T),T by TERMORD:5;
then HT ((m1 *' g1),T) < HT ((m2 *' g2),T),T by A34, 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 A40: (m1 *' g1) . (HT ((m2 *' g2),T)) = 0. L by POLYNOM1:def 9;
A41: ((m2 *' g2) - (m1 *' g1)) . (HT ((m2 *' g2),T)) = ((m2 *' g2) + (- (m1 *' g1))) . (HT ((m2 *' g2),T)) by POLYNOM1:def 23
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + ((- (m1 *' g1)) . (HT ((m2 *' g2),T))) by POLYNOM1:def 21
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + (- ((m1 *' g1) . (HT ((m2 *' g2),T)))) by POLYNOM1:def 22
.= ((m2 *' g2) . (HT ((m2 *' g2),T))) + (0. L) by A40, RLVECT_1:25
.= (m2 *' g2) . (HT ((m2 *' g2),T)) by RLVECT_1:def 7
.= HC ((m2 *' g2),T) by TERMORD:def 7 ;
then ((m2 *' g2) - (m1 *' g1)) . (HT ((m2 *' g2),T)) <> 0. L by A28, TERMORD:17;
then A42: HT ((m2 *' g2),T) in Support ((m2 *' g2) - (m1 *' g1)) by POLYNOM1:def 9;
reconsider x = - (0_ (n,L)) as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 27;
A43: (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 27;
then A44: 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 ;
A45: now
assume (m2 *' g2) - (m1 *' g1) = 0_ (n,L) ; :: thesis: contradiction
then - ((m2 *' g2) + (- (m1 *' g1))) = - (0_ (n,L)) by POLYNOM1:def 23;
then (- (m2 *' g2)) + (- (- (m1 *' g1))) = - (0_ (n,L)) by POLYRED:1;
then (m1 *' g1) + (- (m2 *' g2)) = - (0. (Polynom-Ring (n,L))) by A44, RLVECT_1:19
.= 0. (Polynom-Ring (n,L)) by RLVECT_1:25
.= 0_ (n,L) by POLYNOM1:def 27 ;
hence contradiction by A32, POLYNOM1:def 23; :: thesis: verum
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 A41, TERMORD:32
.= ((m2 *' g2) - (m1 *' g1)) - ((((HC (m2,T)) * (HC (g2,T))) * ((HC (g2,T)) ")) * ((HT (m2,T)) *' g2)) by VECTSP_1:def 23
.= ((m2 *' g2) - (m1 *' g1)) - (((HC (m2,T)) * ((HC (g2,T)) * ((HC (g2,T)) "))) * ((HT (m2,T)) *' g2)) by GROUP_1:def 4
.= ((m2 *' g2) - (m1 *' g1)) - (((HC (m2,T)) * (1. L)) * ((HT (m2,T)) *' g2)) by A29, VECTSP_1:def 22
.= ((m2 *' g2) - (m1 *' g1)) - ((HC (m2,T)) * ((HT (m2,T)) *' g2)) by VECTSP_1:def 19
.= ((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 23
.= ((m2 *' g2) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:def 23
.= ((m2 *' g2) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:80
.= (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, A42, A43, A45, 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 A46: PolyRedRel (P,T) reduces (m2 *' g2) - (m1 *' g1), - (m1 *' g1) by REWRITE1:16;
A47: - (1_ (n,L)) = - ((1. L) | (n,L)) by POLYNOM7:20
.= (- (1. L)) | (n,L) by Th20 ;
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 A46, REWRITE1:17;
then A48: PolyRedRel (P,T) reduces (- (1_ (n,L))) *' ((m2 *' g2) - (m1 *' g1)),(- (1_ (n,L))) *' (0_ (n,L)) by A47, POLYRED:47;
(- (1_ (n,L))) *' ((m2 *' g2) - (m1 *' g1)) = (- (1_ (n,L))) *' ((m2 *' g2) + (- (m1 *' g1))) by POLYNOM1:def 23
.= ((- (1_ (n,L))) *' (m2 *' g2)) + ((- (1_ (n,L))) *' (- (m1 *' g1))) by POLYNOM1:85
.= (- ((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 POLYNOM1:89
.= (m1 *' g1) + (- (m2 *' g2)) by POLYNOM1:89
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 23 ;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) by A30, A48, POLYNOM1:87; :: thesis: verum
end;
end;
end;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis: verum
end;
case A49: HT ((m1 *' g1),T) = HT ((m2 *' g2),T) ; :: thesis: PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L)
(f - (m2 *' g2)) . (HT ((m2 *' g2),T)) = 0. L by A22, A23, POLYNOM1:def 9;
then (f + (- (m2 *' g2))) . (HT ((m2 *' g2),T)) = 0. L by POLYNOM1:def 23;
then (f . (HT ((m2 *' g2),T))) + ((- (m2 *' g2)) . (HT ((m2 *' g2),T))) = 0. L by POLYNOM1:def 21;
then (f . (HT ((m2 *' g2),T))) + (- ((m2 *' g2) . (HT ((m2 *' g2),T)))) = 0. L by POLYNOM1:def 22;
then A50: f . (HT ((m2 *' g2),T)) = - (- ((m2 *' g2) . (HT ((m2 *' g2),T)))) by RLVECT_1:19;
(f - (m1 *' g1)) . (HT ((m1 *' g1),T)) = 0. L by A15, A16, POLYNOM1:def 9;
then (f + (- (m1 *' g1))) . (HT ((m1 *' g1),T)) = 0. L by POLYNOM1:def 23;
then (f . (HT ((m1 *' g1),T))) + ((- (m1 *' g1)) . (HT ((m1 *' g1),T))) = 0. L by POLYNOM1:def 21;
then (f . (HT ((m1 *' g1),T))) + (- ((m1 *' g1) . (HT ((m1 *' g1),T)))) = 0. L by POLYNOM1:def 22;
then A51: f . (HT ((m1 *' g1),T)) = - (- ((m1 *' g1) . (HT ((m1 *' g1),T)))) by RLVECT_1:19;
HC ((m1 *' g1),T) = (m1 *' g1) . (HT ((m1 *' g1),T)) by TERMORD:def 7
.= f . (HT ((m1 *' g1),T)) by A51, RLVECT_1:30
.= (m2 *' g2) . (HT ((m2 *' g2),T)) by A49, A50, RLVECT_1:30
.= HC ((m2 *' g2),T) by TERMORD:def 7 ;
then HM ((m1 *' g1),T) = Monom ((HC ((m2 *' g2),T)),(HT ((m2 *' g2),T))) by A49, 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, A30, A33; :: thesis: verum
end;
end;
end;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis: verum
end;
end;
end;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis: verum
end;
end;
end;
hence PolyRedRel (P,T) reduces f2 - f1, 0_ (n,L) ; :: thesis: verum
end;
hence b,c are_convergent_wrt PolyRedRel (P,T) by A24, A14, POLYRED:50, REWRITE1:41; :: thesis: verum
end;
end;
end;
hence b,c are_convergent_wrt PolyRedRel (P,T) ; :: thesis: verum
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: verum