Proof for derivative of implicit functions My book says the following:

$f'(x,y)=-\left(\frac{\frac{\partial f(x,y)}{\partial x}}{\frac{\partial f(x,y)}{\partial x}}\right)$

We can use this for differentiating implicit functions($f(x,y)=0$)
However they have not mentioned a proof, which I would like to know.
My try:
I assumed that $f(x,y)=g(x)*g(y)$
=>$g(x)*g(y)=0$
Differentiating LHS wrt x,
$g(x)*g'(y)*\frac{dy}{dx}+g(y)*g'(x)=0$
Rearranging this,
$\frac{dy}{dx}=-(\frac{g(y)g'(x)}{g'(y)g(x)})$
How do I relate this with partial derivatives?
 A: We can use the inverse function theorem to prove it. I have slightly rewritten a proof from the book Spaces - An Introduction to Real Analysis by Tom Lindstrøm. The proof might be needlessly complicated since originally it proves the implicit function theorem for any complete normed spaces, not only the real numbers. I assume you're just working with the real numbers here.
Let $U$ be an open subset of $\mathbb{R}^2$. Assume $f: \mathbb{R}^2 \to \mathbb{R}$ has continuous partial derivatives in $U$. Assume there exists an $(a,b)$ such that $f(a,b) = 0$. Also, we need to assume the partial derivative of $f$ with regards to $y$ is not $0$ at this point $(a,b)$.
This will let us prove that there exists an implicit function $g$ defined on an open neighbourhood $W$ of $a$ such that $g(a) = b$, and $f \big( x, g(x) \big) = 0$ for all $x \in W$. Also $g$ is differentiable in $W$.
First define a function
$h:U→\mathbb{R}^2$ by
$$h(x,y)=\big(x,f(x,y)\big).$$
The plan is to apply the inverse function theorem to $h$ and then extract our implicit function $g$ from the inverse of $h$. To use the inverse function theorem, we first have to check that the derivative $h′(a,b):\mathbb{R}^2 \to \mathbb{R}^2$ is invertible. The derivative of $h$ in this point can be shown to be given by the Jacobian Matrix
$$h′(a,b)=
\begin{pmatrix}
\frac{\partial h_1}{\partial x}(a,b) & \frac{\partial h_1}{\partial y}(a,b) \\ 
\frac{\partial h_2}{\partial x}(a,b) & \frac{\partial h_2}{\partial y}(a,b)
\end{pmatrix} =
\begin{pmatrix}
1 & 0 \\ 
\frac{\partial f}{\partial x}(a,b) & \frac{\partial f}{\partial y}(a,b)
\end{pmatrix} 
$$
where $\frac{\partial f}{\partial y}(a,b) \neq 0$ by assumption. This means that $h'(a,b)$ is invertible.
Hence $h$ satisfies the conditions of the inverse function theorem, and has a unique local inverse function $k$ around $h(a,b) = \big(a,f(a,b)\big) = (a,0)$. In other words, $k$ is defined on some neighbourhood $V$ near $(a,0)$. Note also that since $h(x,y) = \big( x,f(x,y)\big)$, its inverse $k$ must have the form $k(x,y) = \big(x, l(x,y)\big)$.
Since $h$ and $k$ are inverses, for all $(x,y)$ in $V$
$$
(x,y) = h\big( k(x,y) \big) = h \big( x, l(x,y) \big) =\Big( x, f\big( x, l(x,y) \big) \Big) . 
$$
Which means $y = f \big(x, l(x,y) \big)$, specifically $0 = f \big(x, l(x,0) \big)$.
We can now define our implicit function $g$ by $g(x) = l(x,0)$, and see that $0 = f \big(x, g(x) \big)$ when $(x,0) \in V$.
It only remains to check that $g$ has the properties described. We have $g(a) = b$, since $f\big(x,l(x,0) \big) = 0 = f(a,b)$. Since $l$ is defined on a neighbourhood of $(a,0)$, $g$ clearly is defined on a neighbourhood $W$ of $a$. And since $l$ is differentiable on the neighbourhood of $(a,0)$ (by the inverse function theorem), $g$ is clearly also differentiable at $a$, which we can find by differentiating on both sides of
$$
f\big( x, g(x) \big) = 0 $$ and use the chain rule to get $$
 \frac{\partial f}{\partial x}(a,b) + \frac{\partial f}{\partial y}(a,b) g'(a) = 0.
$$
This gives us an expression for $g'(a)$, since we know $\frac{\partial f}{\partial y}(a,b)$ is nonzero:
$$
g'(a) = - \frac{\frac{\partial f}{\partial x}(a,b)}{\frac{\partial f}{\partial y}(a,b)}.
$$
The partial derivatives of $f$ are continuous, so for $x$ close to $a$ the above expression also works for $g'(x)$ when $x \in V$.
