Well, while messing around with my next proof, I found I had the same dilemma and ended up solving both proofs.
Starting with 6 field axioms, I'm proving a sequence of 15 algebraic laws.
Number 13 in my list is:
Using the axioms and prior theorems:
I'm stuck here. I'm not seeing how to get from to thus allowing the final step achieving the RHS. Unfortunately, the general case is the next theorem in the list, and so, not available.
If you can provide a hint, I'd appreciate it.