Proof Verification: Implication from Field Axioms Prove that if $ a \neq 0$ then $b/(b/a) = a$
Proof:
$ b/(b/a) = b. 1/(b/a)$ (by Multiplication Axiom 4 (M4))
$\implies  b/(b/a) $ = $b.(b/a)^{-1}$ (by M5)
$\implies $ $b/(b/a)$ = $b.(b.(1/a))^{-1}$ 
$\implies $ $b/(b/a)$ = $b.(b.(a)^{-1})^{-1}$
$\implies $ $b/(b/a)$ = $b.[1/(b.(a)^{-1})]$
$\implies $ $b/(b/a)$ = $b . (1/b) . (1/a^{-1})$
$\implies $ $b/(b/a)$ = $1 .(1/a^{-1})$
$\implies $ $b/(b/a)$ = $(a^{-1})^{-1}$
$\implies $ $b/(b/a)$ = a
Is this correct? Can anyone please verify?
 A: As OP's comments suggest, to derive the proof from the five multiplication axioms in Baby Rudin, break $1$ into the product of $a$ and $1/a$ in the second step.
$\require{action}$
$$
  \begin{aligned}
    b / (b/a) &=
    \texttip{b \cdot 1 \cdot \left( \frac{1}{b/a} \right)}
    {(M4): multiplication by identity} \\
    &= \texttip{b \cdot \left( \frac{1}{a} \right) \cdot a \cdot
    \left( \frac{1}{b/a} \right)}
    {(M5): existence of inverse} \\
    &= \texttip{(b/a) \cdot a \cdot \left( \frac{1}{b/a} \right)}
    {(M3): regroup the leftmost two factors} \\
    &= \texttip{a \cdot (b/a) \cdot \left( \frac{1}{b/a} \right)}
    {(M2): multiplication is commutative} \\
    &= \texttip{a \cdot \left( (b/a) \cdot \left(
    \frac{1}{b/a} \right) \right)}
    {(M3): multiplication is associative} \\
    &= \texttip{a \cdot 1}{(M5): multiplication by inverse} \\
    &= \texttip{a}{(M4): multiplication by identity}
  \end{aligned}
\bbox[4pt,border: 1px solid red]{
\begin{array}{l}
\text{If you cannot figure out why a line}\\
\text{is true, move your mouse over}\\
\text{RHS of that line for hint.}
\end{array}}
$$
Remarks: The above proof is one line shorter than OP's one.
