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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds
G 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 well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds
G is_Groebner_basis_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 ; :: thesis: for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds
G is_Groebner_basis_wrt T
let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) implies G is_Groebner_basis_wrt T )
assume A1: not 0_ (n,L) in G ; :: thesis: ( ex g1, g2 being Polynomial of n,L st
( g1 in G & g2 in G & not PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or G is_Groebner_basis_wrt T )
assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: G is_Groebner_basis_wrt T

now :: thesis: for g1, g2 being Polynomial of n,L st g1 <> g2 & g1 in G & g2 in G holds
for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

let g1, g2 be Polynomial of n,L; :: thesis: ( g1 <> g2 & g1 in G & g2 in G implies for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )
assume that
g1 <> g2 and
A3: g1 in G and
A4: g2 in G ; :: thesis: for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)
thus for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) :: thesis: verum

proof

set a1 = HC (g1,T);
set a2 = HC (g2,T);
set t1 = HT (g1,T);
set t2 = HT (g2,T);
let m1, m2 be Monomial of n,L; :: thesis: ( HM ((m1 *' g1),T) = HM ((m2 *' g2),T) implies PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )
assume A5: HM ((m1 *' g1),T) = HM ((m2 *' g2),T) ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)
A6: HC (g2,T) <> 0. L by A1, A4, TERMORD:17;
reconsider g1 = g1, g2 = g2 as non-zero Polynomial of n,L by A1, A3, A4, POLYNOM7:def 1;
set b1 = coefficient m1;
set b2 = coefficient m2;
set u1 = term m1;
set u2 = term m2;
A7: HC (g1,T) <> 0. L by A1, A3, TERMORD:17;
then reconsider a1 = HC (g1,T), a2 = HC (g2,T) as non zero Element of L by A6, STRUCT_0:def 12;
A8: HC ((m1 *' g1),T) = coefficient (HM ((m1 *' g1),T)) by TERMORD:22
.= HC ((m2 *' g2),T) by A5, TERMORD:22 ;

now :: thesis: ( ( ( coefficient m1 = 0. L or coefficient m2 = 0. L ) & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) or ( coefficient m1 <> 0. L & coefficient m2 <> 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) )

per cases ( coefficient m1 = 0. L or coefficient m2 = 0. L or ( coefficient m1 <> 0. L & coefficient m2 <> 0. L ) ) ;

case A9: ( coefficient m1 = 0. L or coefficient m2 = 0. L ) ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

now :: thesis: ( ( coefficient m1 = 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) or ( coefficient m2 = 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) )

per cases ( coefficient m1 = 0. L or coefficient m2 = 0. L ) by A9;

case coefficient m1 = 0. L ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then HC (m1,T) = 0. L by TERMORD:23;
then m1 = 0_ (n,L) by TERMORD:17;
then A10: m1 *' g1 = 0_ (n,L) by POLYRED:5;
then HC ((m2 *' g2),T) = 0. L by A8, TERMORD:17;
then m2 *' g2 = 0_ (n,L) by TERMORD:17;
then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A10, POLYRED:4;
hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

end;

case coefficient m2 = 0. L ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then HC (m2,T) = 0. L by TERMORD:23;
then m2 = 0_ (n,L) by TERMORD:17;
then A11: m2 *' g2 = 0_ (n,L) by POLYRED:5;
then HC ((m1 *' g1),T) = 0. L by A8, TERMORD:17;
then m1 *' g1 = 0_ (n,L) by TERMORD:17;
then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A11, POLYRED:4;
hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

end;

end;

end;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ; :: thesis: verum

end;

case A12: ( coefficient m1 <> 0. L & coefficient m2 <> 0. L ) ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then reconsider b1 = coefficient m1, b2 = coefficient m2 as non zero Element of L by STRUCT_0:def 12;
b2 * a2 <> 0. L by VECTSP_2:def 1;
then A13: not b2 * a2 is zero ;
HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;
then consider s1 being bag of n such that
A14: (HT (g1,T)) + s1 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;
HC (m2,T) <> 0. L by A12, TERMORD:23;
then A15: m2 <> 0_ (n,L) by TERMORD:17;
HC (m1,T) <> 0. L by A12, TERMORD:23;
then m1 <> 0_ (n,L) by TERMORD:17;
then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by A15, POLYNOM7:def 1;
A16: Monom ((b1 * a1),((term m1) + (HT (g1,T)))) = (Monom (b1,(term m1))) *' (Monom (a1,(HT (g1,T)))) by TERMORD:3
.= m1 *' (Monom (a1,(HT (g1,T)))) by POLYNOM7:11
.= (HM (m1,T)) *' (Monom (a1,(HT (g1,T)))) by TERMORD:23
.= (HM (m1,T)) *' (HM (g1,T)) by TERMORD:def 8
.= HM ((m2 *' g2),T) by A5, TERMORD:33
.= (HM (m2,T)) *' (HM (g2,T)) by TERMORD:33
.= (HM (m2,T)) *' (Monom (a2,(HT (g2,T)))) by TERMORD:def 8
.= m2 *' (Monom (a2,(HT (g2,T)))) by TERMORD:23
.= (Monom (b2,(term m2))) *' (Monom (a2,(HT (g2,T)))) by POLYNOM7:11
.= Monom ((b2 * a2),((term m2) + (HT (g2,T)))) by TERMORD:3 ;
then b1 * a1 = coefficient (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by POLYNOM7:9
.= b2 * a2 by POLYNOM7:9 ;
then (b1 * a1) / a2 = (b2 * a2) * (a2 ")
.= b2 * (a2 * (a2 ")) by GROUP_1:def 3
.= b2 * (1. L) by A6, VECTSP_1:def 10 ;
then A17: b2 / a1 = ((b1 * a1) / a2) / a1
.= ((b1 * a1) * (a2 ")) / a1
.= ((b1 * a1) * (a2 ")) * (a1 ")
.= ((b1 * (a2 ")) * a1) * (a1 ") by GROUP_1:def 3
.= (b1 * (a2 ")) * (a1 * (a1 ")) by GROUP_1:def 3
.= (b1 * (a2 ")) * (1. L) by A7, VECTSP_1:def 10
.= b1 * (a2 ")
.= b1 / a2 ;
b1 * a1 <> 0. L by VECTSP_2:def 1;
then not b1 * a1 is zero ;
then A18: (term m1) + (HT (g1,T)) = term (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by A16, POLYNOM7:10
.= (term m2) + (HT (g2,T)) by A13, POLYNOM7:10 ;
then ( HT (g1,T) divides (term m1) + (HT (g1,T)) & HT (g2,T) divides (term m1) + (HT (g1,T)) ) by TERMORD:1;
then lcm ((HT (g1,T)),(HT (g2,T))) divides (term m1) + (HT (g1,T)) by Th4;
then consider v being bag of n such that
A19: (term m1) + (HT (g1,T)) = (lcm ((HT (g1,T)),(HT (g2,T)))) + v by TERMORD:1;
(term m1) + (HT (g1,T)) = (v + s1) + (HT (g1,T)) by A14, A19, PRE_POLY:35;
then A20: term m1 = ((v + s1) + (HT (g1,T))) -' (HT (g1,T)) by PRE_POLY:48
.= v + s1 by PRE_POLY:48 ;
HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;
then consider s2 being bag of n such that
A21: (HT (g2,T)) + s2 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;
(term m2) + (HT (g2,T)) = (v + s2) + (HT (g2,T)) by A18, A21, A19, PRE_POLY:35;
then A22: term m2 = ((v + s2) + (HT (g2,T))) -' (HT (g2,T)) by PRE_POLY:48
.= v + s2 by PRE_POLY:48 ;
HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;
then A23: s2 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g2,T)) by A21, Def1;
A24: (b2 / a1) * a1 = (b2 * (a1 ")) * a1
.= b2 * ((a1 ") * a1) by GROUP_1:def 3
.= b2 * (1. L) by A7, VECTSP_1:def 10
.= b2 ;
HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;
then A25: s1 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g1,T)) by A14, Def1;
A26: (b1 / a2) * a2 = (b1 * (a2 ")) * a2
.= b1 * ((a2 ") * a2) by GROUP_1:def 3
.= b1 * (1. L) by A6, VECTSP_1:def 10 ;
(m1 *' g1) - (m2 *' g2) = ((Monom (b1,(term m1))) *' g1) - (m2 *' g2) by POLYNOM7:11
.= ((Monom (b1,(term m1))) *' g1) - ((Monom (b2,(term m2))) *' g2) by POLYNOM7:11
.= (b1 * ((v + s1) *' g1)) - ((Monom (b2,(v + s2))) *' g2) by A20, A22, POLYRED:22
.= (b1 * (v *' (s1 *' g1))) - ((Monom (b2,(v + s2))) *' g2) by POLYRED:18
.= (b1 * (v *' (s1 *' g1))) - (b2 * ((v + s2) *' g2)) by POLYRED:22
.= (b1 * (v *' (s1 *' g1))) - (b2 * (v *' (s2 *' g2))) by POLYRED:18
.= (b1 * (v *' (s1 *' g1))) + (- (b2 * (v *' (s2 *' g2)))) by POLYNOM1:def 7
.= (b1 * (v *' (s1 *' g1))) + (b2 * (- (v *' (s2 *' g2)))) by POLYRED:9
.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (- (v *' (s2 *' g2)))) by A26, A24
.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (v *' (- (s2 *' g2)))) by Th13
.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by A17, POLYRED:11
.= ((b1 / a2) * (a2 * (v *' (s1 *' g1)))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by POLYRED:11
.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (a1 * (v *' (- (s2 *' g2))))) by Th15
.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (a1 * (- (s2 *' g2))))) by Th14
.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by POLYRED:9
.= (b1 / a2) * ((v *' (a2 * (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by Th14
.= (b1 / a2) * (v *' ((a2 * (s1 *' g1)) + (- (a1 * (s2 *' g2))))) by Th12
.= (b1 / a2) * (v *' (S-Poly (g1,g2,T))) by A25, A23, POLYNOM1:def 7
.= (Monom ((b1 / a2),v)) *' (S-Poly (g1,g2,T)) by POLYRED:22 ;
hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by A2, A3, A4, POLYRED:48; :: thesis: verum

end;

end;

end;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ; :: thesis: verum

end;

end;

hence G is_Groebner_basis_wrt T by Th17; :: thesis: verum