Okay, today we’re going to prove the implicit function theorem. We’re going to think of our function as taking an -dimensional vector and a -dimensional vector and giving back an -dimensional vector . In essence, what we want to do is see how this output vector must change as we change , and then undo that by making a corresponding change in . And to do that, we need to know how changing the output changes , at least in a neighborhood of . That is, we’ve got to invert a function, and we’ll need to use the inverse function theorem.
But we’re not going to apply it directly as the above heuristic suggests. Instead, we’re going to “puff up” the function into a bigger function that will give us some room to maneuver. For we define
just copying over our original function. Then we continue by defining for
That is, the new component functions are just the coordinate functions . We can easily calculate the Jacobian matrix
where is the zero matrix and is the identity matrix. From here it’s straightforward to find the Jacobian determinant
which is exactly the determinant we assert to be nonzero at . We also easily see that .
And so the inverse function theorem tells us that there are neighborhoods of and of so that is injective on and , and that there is a continuously differentiable inverse function so that for all . We want to study this inverse function to recover our implicit function from it.
First off, we can write for two functions: which takes -dimensional vector values, and which takes -dimensional vector values. Our inverse relation tells us that
But since is injective from onto , we can write any point as , and in this case we must have by the definition of . That is, we have
And so we see that , where is the -dimensional vector so that . We thus have for every .
Now define be the collection of vectors so that , and for each such define , so . As a slice of the open set in the product topology on , the set is open in . Further, is continuously differentiable on since is continuously differentiable on , and the components of are taken directly from those of . Finally, is in since , and by assumption. This also shows that .
The only thing left is to show that is uniquely defined. But there can only be one such function, by the injectivity of . If there were another such function then we’d have , and thus , or for every .