[proofplan] The only missing condition in the definition of a Euclidean diffeomorphism is the smoothness of the inverse map, since $f$ is already assumed to be a smooth bijection between open subsets of $\mathbb{R}^n$. At each point $x \in U$, the invertibility of $Jf_x$ allows us to apply the [Inverse Function Theorem](/theorems/51) and obtain a local smooth inverse near $f(x)$. Bijectivity identifies this local inverse with the restriction of the global inverse $f^{-1}$. Since this happens around every point of $V$, the inverse map is smooth on all of $V$. [/proofplan] [step:Define the global inverse and reduce the conclusion to proving its smoothness] Because $f: U \to V$ is bijective, there exists a unique inverse map \begin{align*} g: V \to U \end{align*} defined by the condition that, for every $y \in V$, $g(y)$ is the unique point $x \in U$ satisfying $f(x)=y$. By definition of inverse maps, \begin{align*} g \circ f = \operatorname{id}_U \end{align*} and \begin{align*} f \circ g = \operatorname{id}_V. \end{align*} A Euclidean diffeomorphism is a smooth bijection between open subsets of Euclidean space whose inverse is smooth. Since $f$ is already a smooth bijection by hypothesis, it remains only to prove that $g: V \to U$ is smooth. [/step] [step:Apply the Inverse Function Theorem at an arbitrary point of the domain] Fix $x_0 \in U$, and define $y_0 := f(x_0) \in V$. Since $Jf_{x_0}$ is invertible by hypothesis, the total derivative $Df_{x_0}: \mathbb{R}^n \to \mathbb{R}^n$ is a linear isomorphism, with matrix representation $Jf_{x_0}$ in the standard bases. The Inverse Function Theorem applies to the smooth map $f: U \to V$ at $x_0$, because $U \subset \mathbb{R}^n$ is open, $f$ is smooth on $U$, and $Df_{x_0}$ is invertible. Therefore there exist open neighbourhoods $A_{x_0} \subset U$ of $x_0$ and $B_{y_0} \subset V$ of $y_0$ such that the restriction $f|_{A_{x_0}}: A_{x_0} \to B_{y_0}$ is a Euclidean diffeomorphism. In particular, there is a smooth inverse map $h_{y_0}: B_{y_0} \to A_{x_0}$ satisfying $h_{y_0} \circ f|_{A_{x_0}} = \operatorname{id}_{A_{x_0}}$ and $f|_{A_{x_0}} \circ h_{y_0} = \operatorname{id}_{B_{y_0}}$. [/step] [step:Identify the local inverse with the restriction of the global inverse] We claim that \begin{align*} g|_{B_{y_0}} = h_{y_0}. \end{align*} Let $y \in B_{y_0}$. Since $h_{y_0}$ is the inverse of $f|_{A_{x_0}}$, we have \begin{align*} f(h_{y_0}(y)) = y. \end{align*} By the definition of the global inverse $g$, the point $g(y)$ is the unique element of $U$ mapped to $y$ by $f$. Hence $g(y)=h_{y_0}(y)$. Since $y \in B_{y_0}$ was arbitrary, $g|_{B_{y_0}}=h_{y_0}$. [guided] The local inverse supplied by the Inverse Function Theorem is initially only an inverse for the restricted map $f|_{A_{x_0}}: A_{x_0} \to B_{y_0}$. We must check that this local inverse is the same map as the global inverse $g: V \to U$ when both are evaluated on points of $B_{y_0}$. Let $y \in B_{y_0}$. The map \begin{align*} h_{y_0}: B_{y_0} \to A_{x_0} \end{align*} is the inverse of $f|_{A_{x_0}}$, so applying $f$ to $h_{y_0}(y)$ gives \begin{align*} f(h_{y_0}(y)) = y. \end{align*} On the other hand, the global inverse \begin{align*} g: V \to U \end{align*} was defined using the bijectivity of $f$: for each $y \in V$, the point $g(y)$ is the unique element of $U$ satisfying $f(g(y))=y$. Since $h_{y_0}(y) \in A_{x_0} \subset U$ is also mapped to $y$, uniqueness forces \begin{align*} g(y)=h_{y_0}(y). \end{align*} Thus the global inverse and the local inverse agree at every point of $B_{y_0}$, so \begin{align*} g|_{B_{y_0}} = h_{y_0}. \end{align*} This is exactly where global bijectivity is used: without injectivity, the local inverse near $x_0$ might select only one branch of a multi-valued inverse, and it would not determine a globally defined inverse map. [/guided] [/step] [step:Use local smoothness around every point of $V$ to prove that the global inverse is smooth] Let $y \in V$ be arbitrary. Since $f: U \to V$ is surjective, there exists $x \in U$ such that $y=f(x)$. Applying the previous two steps with this point $x$ gives an open neighbourhood $B_y \subset V$ of $y$ and a smooth map \begin{align*} h_y: B_y \to U \end{align*} such that \begin{align*} g|_{B_y} = h_y. \end{align*} Therefore $g$ is smooth on the neighbourhood $B_y$ of $y$. Because $y \in V$ was arbitrary, every point of $V$ has an open neighbourhood on which $g$ agrees with a smooth Euclidean map. Smoothness of maps between open subsets of Euclidean space is a local property, so $g: V \to U$ is smooth on all of $V$. [/step] [step:Conclude that the original map is a Euclidean diffeomorphism] The map $f: U \to V$ is a smooth bijection by hypothesis. The preceding step proves that its inverse $f^{-1}=g: V \to U$ is smooth. Hence $f$ is a Euclidean diffeomorphism. [/step]