Proof of The Inverse Function Theorem for Smooth Functions

Throughout, the arithmetic and order of $\mathbb{R}$ are used through The Structure of ℝ as a Field and an Ordered Ring (i), The Structure of ℝ as a Field and an Ordered Ring (ii), Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (v), Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (ix), Rules of Arithmetic and Order in an Ordered Field (iii) and The Quotient 1/x, Order Rules for Sums, and Nesting of Closed Intervals in ℝ (i); norms and distances in $\mathbb{R}^{n}$ through Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (ii), Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (v), Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (vi) and Standard Basis Vectors of ℝ^q: Coordinates, Orthonormality and Unit Length (iii); and the metric spaces $(\mathbb{R}^{n},d_{E})$ and $(\mathbb{R},d_{\mathbb{R}})$ through $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence (i) and The Absolute Value Metric on the Real Numbers (i).

We prove (i). Since $f$ is smooth on $U$, it is of class $C^{1}$ on $U$ by Basic Properties of Cᵏ Functions (ii). By The Inverse Function Theorem (i) there is an open set $W$ with $a\in W\subseteq U$ such that $V=f(W)$ is open, $f$ is injective on $W$, and the inverse function $g:V\to W$ of $f|_{W}$ is of class $C^{1}$ on $V$, with

$$Dg\bigl(f(x)\bigr)=Df(x)^{-1}\qquad(x\in W).$$

This is the derivative formula of the statement; it remains to show that $f|_{W}$ is a smooth diffeomorphism of $W$ onto $V$.

Let $k\in\mathbb{N}$. Then $f$ is of class $C^{k}$ on $U$ (Basic Properties of Cᵏ Functions (ii)), and $W$ satisfies the hypotheses of The Inverse Function Theorem (ii), so $g$ is of class $C^{k}$ on $V$. Being of class $C^{1}$, $g$ is also of class $C^{0}$ on $V$ (Basic Properties of Cᵏ Functions (ii)). Hence $g$ is smooth on $V$ (Smooth Functions on an Open Subset of ℝⁿ (ii)). The restriction $f|_{W}$ is smooth on the open set $W$ by Restriction of a Cᵏ Function to an Open Subset (ii). Since $f|_{W}$ is injective with image $V$ and both it and its inverse $g$ are smooth, $f|_{W}$ is a smooth diffeomorphism of $W$ onto $V$ (Cᵏ Diffeomorphisms Between Open Subsets of ℝⁿ (i)). Finally, $W$ is open with $a\in W\subseteq U$ and $f(W)=V$ is open, so $f$ is a local smooth diffeomorphism at $a$ (Local Cᵏ Diffeomorphisms (i)).