[proofplan] We prove directly that the inverse map is bijective, holomorphic, and has non-vanishing complex derivative at every point of $V$. Bijectivity follows from the definition of inverse map. For holomorphicity and the derivative formula, we apply the [holomorphic inverse function theorem](/theorems/4950) locally at each point, using the conformality hypothesis $f'(z)\neq 0$. The resulting formula for $(f^{-1})'$ also gives non-vanishing of the inverse derivative. [/proofplan] [step:Declare the inverse map and reduce the proof to local holomorphicity] Define the inverse map \begin{align*} g:V\to U,\quad g(w)=f^{-1}(w). \end{align*} Since $f:U\to V$ is bijective, $g$ is bijective, $g\circ f=\operatorname{id}_U$, and $f\circ g=\operatorname{id}_V$. It remains to prove that $g$ is holomorphic on $V$ and that $g'(w)\neq 0$ for every $w\in V$. [/step] [step:Apply the holomorphic inverse function theorem at an arbitrary point of $V$] Let $w_0\in V$, and define $z_0:=g(w_0)\in U$. Since $f$ is conformal on $U$, the map $f:U\to V$ is holomorphic and satisfies $f'(z_0)\neq 0$. By the holomorphic [inverse function theorem](/theorems/51) (citing a result not yet in the wiki: Holomorphic inverse function theorem), applied to the holomorphic map $f$ at the point $z_0$, there exist open neighbourhoods $A\subset U$ of $z_0$ and $B\subset V$ of $w_0$ such that $f|_A:A\to B$ is biholomorphic. Its inverse \begin{align*} (f|_A)^{-1}:B\to A \end{align*} is holomorphic, and for every $w\in B$, \begin{align*} ((f|_A)^{-1})'(w)=\frac{1}{f'((f|_A)^{-1}(w))}. \end{align*} For every $w\in B$, the equality $f((f|_A)^{-1}(w))=w$ and injectivity of $f:U\to V$ imply $(f|_A)^{-1}(w)=g(w)$. Hence $g|_B=(f|_A)^{-1}$, so $g$ is holomorphic on the neighbourhood $B$ of $w_0$ and \begin{align*} g'(w_0)=\frac{1}{f'(g(w_0))}. \end{align*} Because $f'(g(w_0))\neq 0$, this gives $g'(w_0)\neq 0$. [guided] Fix an arbitrary point $w_0\in V$. To prove that $g$ is holomorphic on all of $V$, it is enough to prove that $g$ is holomorphic on some neighbourhood of each such $w_0$. Define the point of $U$ lying above $w_0$ by \begin{align*} z_0:=g(w_0). \end{align*} Since $g=f^{-1}$, this means $f(z_0)=w_0$. The conformality of $f$ supplies the key hypothesis for the local inverse theorem: $f$ is holomorphic on $U$, and \begin{align*} f'(z_0)\neq 0. \end{align*} The holomorphic inverse function theorem (citing a result not yet in the wiki: Holomorphic inverse function theorem) applies to the holomorphic map $f$ at $z_0$. Its hypotheses are exactly that $U$ is open, that $f$ is holomorphic in a neighbourhood of $z_0$, and that $f'(z_0)\neq 0$; these hold because $U$ is open and $f$ is conformal on $U$. Therefore there are open neighbourhoods $A\subset U$ of $z_0$ and $B\subset V$ of $w_0$ such that the restricted map \begin{align*} f|_A:A\to B \end{align*} has a holomorphic inverse \begin{align*} (f|_A)^{-1}:B\to A. \end{align*} Moreover, for every $w\in B$, the inverse derivative formula gives \begin{align*} ((f|_A)^{-1})'(w)=\frac{1}{f'((f|_A)^{-1}(w))}. \end{align*} We now compare the local inverse with the global inverse $g$. If $w\in B$, then $(f|_A)^{-1}(w)\in A\subset U$ and \begin{align*} f((f|_A)^{-1}(w))=w. \end{align*} Also $g(w)\in U$ and $f(g(w))=w$. Since $f:U\to V$ is injective, these two preimages of $w$ are equal: \begin{align*} (f|_A)^{-1}(w)=g(w). \end{align*} Thus $g|_B=(f|_A)^{-1}$, so $g$ is holomorphic on the neighbourhood $B$ of $w_0$. Evaluating the inverse derivative formula at $w_0$ gives \begin{align*} g'(w_0)=\frac{1}{f'(g(w_0))}. \end{align*} The denominator is nonzero because $f$ is conformal and $g(w_0)\in U$. Therefore $g'(w_0)\neq 0$. [/guided] [/step] [step:Conclude that the inverse is conformal on all of $V$] The point $w_0\in V$ was arbitrary. Hence $g=f^{-1}:V\to U$ is holomorphic at every point of $V$ and satisfies $g'(w)\neq 0$ for every $w\in V$. Together with the bijectivity established above, this proves that $f^{-1}:V\to U$ is a bijective [conformal map](/page/Conformal%20Map). Therefore $f^{-1}$ is a conformal isomorphism. [/step]