Show how Eliminate arrives at reduction

Question

Does anyone know how to get Mathematica to show how it arrives at the following result?

  Eliminate[{7*x == -(x*y) + (9*y^4)/(1 + 3*x)^2, 5*y == -2*x^2 + (6*y^3)/(1 + 3*x)}, x]

The output is correct and is:

$$223503 y^5-89394 y^4-692789 y^3-44380 y^2-980 y=0 $$

Is there a way to get MMA to actually show how it reduced in order to perform the elimination?

I can verify the result as part of a larger calculation not shown here.

Answer 1

In biref, clear denominators and form a lexicographic Groebner basis with variable ordering x>y. Now throw out anything with x in it.

eqns = {7*x == -(x*y) + (9*y^4)/(1 + 3*x)^2, 
   5*y == -2*x^2 + (6*y^3)/(1 + 3*x)};
rats = Subtract @@@ eqns;
polys = Numerator[Together[rats]]

(* Out[112]= {7 x + 42 x^2 + 63 x^3 + x y + 6 x^2 y + 9 x^3 y - 9 y^4, 
 2 x^2 + 6 x^3 + 5 y + 15 x y - 6 y^3} *)

GroebnerBasis[polys, {x, y}]

(* Out[119]= {-980 y^4 - 44380 y^5 - 692789 y^6 - 89394 y^7 + 223503 y^8,
  22376839800 y + 67130519400 x y + 1028416965310 y^4 + 
  50966648905843 y^5 + 7352301429078 y^6 - 16547763614151 y^7, 
 187965454320 x + 563896362960 x^2 + 1691689088880 y^3 + 
  64548598500890 y^4 + 3210933385300829 y^5 + 463189747121364 y^6 - 
  1042508399187003 y^7} *)

--- edit ---

Okay, I did say "in brief" (or actually "In biref", since I was taught to capitalize the first word of sentences, and also my "i" finger is faster than my "r" finger). But the result above has a degree that is too high in the polynomial in y. Below I correct for this.

So what is going on? We need to account for not letting denominators vanish. This is done behind the scenes in a manner similar to what I show below. We again form our rational function expressions but now obtain the unique denominators and create new variable/equation pairs that force them not to vanish (in this case there is actually only one denominator once we remove powers, but what I show is appropriate for the general case).

eqns = {7*x == -(x*y) + (9*y^4)/(1 + 3*x)^2, 
   5*y == -2*x^2 + (6*y^3)/(1 + 3*x)};
rats = Together[Subtract @@@ eqns];
denoms = Union[
  Flatten[Join[Map[Rest[FactorList[#]] &, Denominator[rats]]], 
    1][[All, 1]]]
rvars = Array[r, Length[denoms]];
rpolys = rvars*denoms - 1

(* Out[164]= {1 + 3 x}

Out[166]= {-1 + (1 + 3 x) r[1]} *)

Now form the full set and use a term order that puts the reciprocal variables and x all above y.

polys = Join[Numerator[rats], rpolys]

(* Out[167]= {7 x + 42 x^2 + 63 x^3 + x y + 6 x^2 y + 9 x^3 y - 9 y^4, 
 2 x^2 + 6 x^3 + 5 y + 15 x y - 6 y^3, -1 + (1 + 3 x) r[1]} *)

GroebnerBasis[polys, Join[rvars, {x, y}]]

(* Out[168]= {-980 y - 44380 y^2 - 692789 y^3 - 89394 y^4 + 223503 y^5, 
 27400212 x - 412299580 y - 6426803545 y^2 - 826223919 y^3 + 
  2069637780 y^4, -73067232 + 770534933630 y + 2706567452975 y^2 + 
  140755226664 y^3 - 843332918253 y^4 + 73067232 r[1]} *)

This time the first polynomial has the right degree.

--- end edit ---