I have a set $G$ , and I am trying to prove that the set is a groebner basis .
From chapter $2$ of Ideals,Varieties and Algorithm I have the following theorem,
A basis $G = \{g_1,\cdots, g_n \}$ for an ideal I is a Gröbner basis if and only if $S(g_i, g_j) \to_{G} 0 $ for all $i \ne j$.
My ideal $I$ is generated by $y_1+ y_2*x_3 + y_3*x_3^2$,$y_1+ y_2*x_2 + y_3*x_2^2$,$y_1 + y_2*x_1+y_2*x_1^2$ and the monomial order is $(y_1>y_2>y_3>x_1>x_2>x_3)$ lexicographic ordering
The set $G$ is $\{y_3*x_1^2*x_2 - y_3*x_1^2*x_3 - y_3*x_1*x_2^2 + y_3*x_1*x_3^2 + y_3*x_2^2*x_3 - y_3*x_2*x_3^2 , y_2*x_2 - y_2*x_3 + y_3*x_2^2 - y_3*x_3^2 , y_2*x_1 - y_2*x_3 + y_3*x_1^2 - y_3*x_3^2 , y_1+ y_2*x_3 + y_3*x_3^2\}$
I am trying to claim is that this set $G$ is the groebner basis of $I$
I calculated the $6$, S-polynomials of the polynomials in $G$ and I have shown that the remainder obtained after dividing these (by the polynomials present in G) is $0$ .
Is this process enough to conclude that $G$ is a groebner basis of $I$?
Or should I be calculating the leading term of $S(g_i,g_j)$ where $i \ne j$ and $g_i,g_j \in G$ and then checking whether the leading term of this $S$-polynomial is present in the ideal generated by $\langle LT(g_1),Lt(g_2) ,\cdots Lt(g_n) \rangle$?
Edit 1:I have done the calculations and I wanted someone to check the way that I have **written and done ** the proof is correct or not.
A basis $G = \{g_1 \cdots g_n\}$ for an ideal $I$ is a Gröbner basis if and only if $S(g_i, g_j) \to_{G} 0$ for all $i \ne j$.
$I = \langle y_1+y_2*x_1+y_3*x_1^2,y_1+y_2*x_2+y_3*x_2^2,y_1+y_2*x_3+y_3*x_3^2 \rangle $
Then the set $G$ is a basis if $y_1+y_2*x_1+y_3*x_1^2 (mod G) = 0$,$,y_1+y_2*x_2+y_3*x_2^2 (mod G) = 0$, $y_1+y_2*x_3+y_3*x_3^2 (mod G) = 0 $
**We try to prove that after using the multivaraite divison algorithm $y_1+y_2*x_1+y_3*x_1^2$ (mod G) $= 0$ **
Dividing $y_1+y_2*x_1+y_3*x_1^2$ by $y_1+y_2*x_3+y_3*x_3^2$ we get the remainder as $y_2*x_1 - y_2*x_3 + y_3*x_1^2 - y_3*x_3^2 $
Then, dividing $y_2*x_1 - y_2*x_3 + y_3*x_1^2 - y_3*x_3^2 $ by $y_2*x_3 - y_2*x_1 + y_3*x_3^2 - y_3*x_1^2 $ we get the remiander as $0$ and the quotient as $-1$
Then, $y_1+y_2*x_1+y_3*x_1^2=1.(y_1+y_2*x_3+y_3*x_3^2)+-1.(y_2*x_3 - y_2*x_1 + y_3*x_3^2 - y_3*x_1^2 )$
So the remainder obtained is $0$ after dividing it by $G$
We try to prove that after using the multivaraite divison algorithm $y_1+y_2*x_2+y_3*x_2^2$ (mod G) $= 0$
Dividing $y_1+y_2*x_2+y_3*x_2^2$ by $y_1+y_2*x_3+y_3*x_3^2$ we get the remainder as $y_2*x_1 - y_2*x_3 + y_3*x_1^2 - y_3*x_3^2 $
Then, dividing $-y_2*x_2 + y_2*x_3 - y_3*x_2^2 + y_3*x_3^2 $ by $y_2*x_3 - y_2*x_1 + y_3*x_3^2 - y_3*x_1^2 $ we get the remainder as $0$ and the quotient as $-1$
Then, $y_1+y_2*x_1+y_3*x_1^2=1.(y_1+y_2*x_3+y_3*x_3^2)+-1.((-y_2*x_2 + y_2*x_3 - y_3*x_2^2 + y_3*x_3^2 )$
So the remainder obtained is $0$ after dividing it by $G$
We try to prove that after using the multivaraite divison algorithm $y_1+y_2*x_3+y_3*x_3^2$ (mod G) $= 0$
It is easy to see because the polynomial is itself present in the set $G$.
So we conclude from here that $G$ is a basis
We try to prove that $G$ is a Gröbner basis by showing that $S(g_i, g_j) \to_{G} 0$ for all $i \ne j$
i)S($ y_2*x_3 - y_2*x_1 + y_3*x_3^2 - y_3*x_1^2 ,y_1+ y_2*x_3 + y_3*x_3^2$)=$y_1*y_2*x_3 - y_1*y_3*x_1^2 + y_1*y_3*x_3^2 + y_2^2*x_1*x_3 + y_2*y_3*x_1*x_3^2$
We try to show that this $S$-polynomial obtained gives a zero remainder after division by $G$.
1.dividing by $(y_1 + y_2*x_3 + y_3*x_3^2)$
a)substract: $(y_1 + y_2*x_3 + y_3*x_3^2)(y_2*x_3)$ from becomes $-y_1*y_3*x_1^2 + y_1*y_3*x_3^2 + y_2^2*x_1*x_3 - y_2^2*x_3^2 + y_2*y_3*x_1*x_3^2 - y_2*y_3*x_3^3 $
b)subtract $(y_1 + y_2*x_3 + y_3*x_3^2)(-y_3*x_1^2)$ from f becomes $y_1*y_3*x_3^2 + y_2^2*x_1*x_3 - y_2^2*x_3^2 + y_2*y_3*x_1^2*x_3 + y_2*y_3*x_1*x_3^2 - y_2*y_3*x_3^3 + y_3^2*x_1^2*x_3^2$
c)substract $(y_1 + y_2*x_3 + y_3*x_3^2)(y_3*x_3^2)$ from f becomes $y_2^2*x_1*x_3 - y_2^2*x_3^2 + y_2*y_3*x_1^2*x_3 + y_2*y_3*x_1*x_3^2 - 2*y_2*y_3*x_3^3 + y_3^2*x_1^2*x_3^2 - y_3^2*x_3^4$
2.dividing $(-y_2*x_1 + y_2*x_3 - y_3*x_1^2 + y_3*x_3^2)$
a)substract $(-y_2*x_1 + y_2*x_3 - y_3*x_1^2 + y_3*x_3^2)(-y_2*x_3)$ from f becomes $y_2*y_3*x_1*x_3^2 - y_2*y_3*x_3^3 + y_3^2*x_1^2*x_3^2 - y_3^2*x_3^4$
b)substract$ (-y_2*x_1 + y_2*x_3 - y_3*x_1^2 + y_3*x_3^2)(-y_3*x_3^2)$ from f becomes $0$.
$y_1*y_2*x_3 - y_1*y_3*x_1^2 + y_1*y_3*x_3^2 + y_2^2*x_1*x_3 + y_2*y_3*x_1*x_3^2$=$0*y_3*x_1^2*x_2 - y_3*x_1^2*x_3 - y_3*x_1*x_2^2 + y_3*x_1*x_3^2 + y_3*x_2^2*x_3 - y_3*x_2*x_3^2 + 0*y_2*x_2 - y_2*x_3 + y_3*x_2^2 - y_3*x_3^2 + (y_2*x_3 + y_3*x_3^2)*y_2*x_1 - y_2*x_3 + y_3*x_1^2 - y_3*x_3^2 + (y_2*x_3 - y_3*x_1^2 + y_3*x_3^2)*y_1+ y_2*x_3 + y_3*x_3^2 $
I have adopted the similar process for the rest of the $S$-polynomial to get a zero remainder after division by the polynomials in the set $G$.
I need someone to look into my proof and also for the way I have written it.