Below is the proof of the inverse function theorem for multivariable functions given in Spivaks "Calculus on Manifolds". I have made a few interpretations regarding his reasoning and want to know if I have interpreted correctly.
He spends the majority of the first part of the proof proving that $f$ is bijective, as this implies the existence of an inverse.
The only time we use that $Df(a)=I$ is when we define $\mu=Df(a)$ and write $\mu^{-1}\big(f(x_1)-f(x)\big)=\mu^{-1}\big(\mu(x_1-x)+\phi(x_1-x)\big)$ $=$ $\mu^{-1}\big(\mu(x_1-x)\big)+\mu^{-1}\big(\phi(x_1-x)\big)$, since $\mu=I$ implies that $\mu^{-1}=\mu=I$ ,which gives that $\mu^{-1}$ is linear. Besides that I don't see any other application of the property $Df(a)=I$ we established in the opening lines of the proof.
- $detf'(a)\neq 0$ is only used in the proof to guarantee that there exists a neighborhood around $f'(a)$ such that every element is non-zero; and then this implication is used to show that we must have $y^{i}-f^i(x)=0$, $\forall i$
Thanks in advance!
No, the main thing you've overlooked is that he uses $Df(a)=I$ in a crucial way when he considers $g(x)=f(x)-x$ to prove 4. (Intuitively, if $Df(a)=I$, then near $a$ the function $f$ is close to the identity function.) And, no, $\det Df(a)\ne 0$ is used to know that $Df(a)$ is invertible. That's what makes the whole proof get started.