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 not 0_ n,L in P & ( 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 not 0_ n,L in P & ( 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 not 0_ n,L in P & ( 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: ( not 0_ n,L in P & ( 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 )
X:
0_ n,L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
assume
not 0_ n,L in P
; :: thesis: ( ex p1, p2 being Polynomial of n,L st
( p1 <> p2 & p1 in P & p2 in P & ex m1, m2 being Monomial of n,L st
( HM (m1 *' p1),T = HM (m2 *' p2),T & not PolyRedRel P,T reduces (m1 *' p1) - (m2 *' p2), 0_ n,L ) ) or 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;
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 A2:
(
[a,b] in PolyRedRel P,
T &
[a,c] in PolyRedRel P,
T )
;
:: thesis: b,c are_convergent_wrt PolyRedRel P,Tthen consider f,
f1 being
set such that A3:
(
f in NonZero (Polynom-Ring n,L) &
f1 in the
carrier of
(Polynom-Ring n,L) &
[a,b] = [f,f1] )
by ZFMISC_1:def 2;
reconsider f1 =
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, X, XBOOLE_0:def 5;
reconsider f =
f as
Polynomial of
n,
L by A3, POLYNOM1:def 27;
f <> 0_ n,
L
by A4, TARSKI:def 1;
then reconsider f =
f as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
consider f',
f2 being
set such that A5:
(
f' in NonZero (Polynom-Ring n,L) &
f2 in the
carrier of
(Polynom-Ring n,L) &
[a,c] = [f',f2] )
by A2, ZFMISC_1:def 2;
reconsider f2 =
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
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 =
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
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 =
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;
set mg2 =
m2 *' g2;
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
;
:: thesis: b,c are_convergent_wrt PolyRedRel P,Tthen f1 =
f - (0_ n,L)
by A17, POLYRED:5
.=
f
by POLYRED:4
;
then
(
PolyRedRel P,
T reduces b,
c &
PolyRedRel P,
T reduces c,
c )
by A2, A6, A7, A9, REWRITE1:13, REWRITE1:16;
hence
b,
c are_convergent_wrt PolyRedRel P,
T
by REWRITE1:def 7;
:: thesis: verum end; case
m2 = 0_ n,
L
;
:: thesis: b,c are_convergent_wrt PolyRedRel P,Tthen f2 =
f - (0_ n,L)
by A18, POLYRED:5
.=
f
by POLYRED:4
;
then
(
PolyRedRel P,
T reduces c,
b &
PolyRedRel P,
T reduces b,
b )
by A2, A6, A8, A9, REWRITE1:13, REWRITE1:16;
hence
b,
c are_convergent_wrt PolyRedRel P,
T
by REWRITE1:def 7;
:: thesis: verum end; case
(
m1 <> 0_ n,
L &
m2 <> 0_ n,
L )
;
:: thesis: b,c are_convergent_wrt PolyRedRel P,Tthen 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) &
(HT m2,T) + (HT g2,T) in Support (m2 *' g2) )
by TERMORD:29;
then A19:
(
m1 *' g1 <> 0_ n,
L &
m2 *' g2 <> 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
.=
(m1 *' g1) - (m2 *' g2)
by POLYNOM1:def 23
;
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 A22:
(m1 *' g1) - (m2 *' g2) <> 0_ n,
L
;
:: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,Lnow per cases
( g1 = g2 or g1 <> g2 )
;
case A23:
g1 <> g2
;
:: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,Lnow per cases
( HT (m1 *' g1),T <> HT (m2 *' g2),T or HT (m1 *' g1),T = HT (m2 *' g2),T )
;
case A24:
HT (m1 *' g1),
T <> HT (m2 *' g2),
T
;
:: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,Lnow 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,Lthen
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 A25:
(m2 *' g2) . (HT (m1 *' g1),T) = 0. L
by POLYNOM1:def 9;
A26:
((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 A25, 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 A19, TERMORD:17;
then A27:
HT (m1 *' g1),
T in Support ((m1 *' g1) - (m2 *' g2))
by POLYNOM1:def 9;
A28:
(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 A26, 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 A20, 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 A13, A22, A27, A28, 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 A11, POLYRED:def 7;
then
[((m1 *' g1) - (m2 *' g2)),(- (m2 *' g2))] in PolyRedRel P,
T
by POLYRED:def 13;
then A29:
PolyRedRel P,
T reduces (m1 *' g1) - (m2 *' g2),
- (m2 *' g2)
by REWRITE1:16;
PolyRedRel P,
T reduces (- m2) *' g2,
0_ n,
L
by A14, 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 A21, A29, 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,Lthen
HT (m1 *' g1),
T <= HT (m2 *' g2),
T,
T
by TERMORD:5;
then
HT (m1 *' g1),
T < HT (m2 *' g2),
T,
T
by A24, 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 A30:
(m1 *' g1) . (HT (m2 *' g2),T) = 0. L
by POLYNOM1:def 9;
A31:
((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 A30, 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 A19, TERMORD:17;
then A32:
HT (m2 *' g2),
T in Support ((m2 *' g2) - (m1 *' g1))
by POLYNOM1:def 9;
A33:
(HT m2,T) + (HT g2,T) = HT (m2 *' g2),
T
by TERMORD:31;
reconsider x =
- (0_ n,L) as
Element of
(Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x =
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
;
((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 A31, 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 A20, 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 A16, A32, A33, A35, 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 A14, POLYRED:def 7;
then
[((m2 *' g2) - (m1 *' g1)),(- (m1 *' g1))] in PolyRedRel P,
T
by POLYRED:def 13;
then A36:
PolyRedRel P,
T reduces (m2 *' g2) - (m1 *' g1),
- (m1 *' g1)
by REWRITE1:16;
PolyRedRel P,
T reduces (- m1) *' g1,
0_ n,
L
by A11, POLYRED:45;
then
PolyRedRel P,
T reduces - (m1 *' g1),
0_ n,
L
by POLYRED:6;
then A37:
PolyRedRel P,
T reduces (m2 *' g2) - (m1 *' g1),
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:
PolyRedRel P,
T reduces (- (1_ n,L)) *' ((m2 *' g2) - (m1 *' g1)),
(- (1_ n,L)) *' (0_ n,L)
by A37, 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 A21, A38, POLYNOM1:87;
:: thesis: verum end; hence
PolyRedRel P,
T reduces f2 - f1,
0_ n,
L
;
:: thesis: verum case A39:
HT (m1 *' g1),
T = HT (m2 *' g2),
T
;
:: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L
(f - (m1 *' g1)) . (HT (m1 *' g1),T) = 0. L
by A17, 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 A40:
f . (HT (m1 *' g1),T) = - (- ((m1 *' g1) . (HT (m1 *' g1),T)))
by RLVECT_1:19;
(f - (m2 *' g2)) . (HT (m2 *' g2),T) = 0. L
by A18, 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 A41:
f . (HT (m2 *' g2),T) = - (- ((m2 *' g2) . (HT (m2 *' g2),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 A40, RLVECT_1:30
.=
(m2 *' g2) . (HT (m2 *' g2),T)
by A39, A41, 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 A39, TERMORD:def 8
.=
HM (m2 *' g2),
T
by TERMORD:def 8
;
hence
PolyRedRel P,
T reduces f2 - f1,
0_ n,
L
by A1, A11, A14, A21, A23;
:: thesis: verum end; hence
PolyRedRel P,
T reduces f2 - f1,
0_ n,
L
;
:: thesis: verum hence
PolyRedRel P,
T reduces f2 - f1,
0_ n,
L
;
:: thesis: verum
hence
PolyRedRel P,
T reduces f2 - f1,
0_ n,
L
;
:: thesis: verum
end; hence
b,
c are_convergent_wrt PolyRedRel P,
T
by A7, A8, POLYRED:50, REWRITE1:41;
:: thesis: verum 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