What the implicit function theorem is actually showing

Theorem: Let $F: X\subseteq \mathbb{R}^n \rightarrow \mathbb{R}$ be of class of $C^1$ and let $a$ be a point of the level set $S=\{x\in\mathbb{R}^n \mid F(x)=c\}$. If $F_{x_n}(a)\neq 0$ then there is a neighborhood $U$ of $(a_1,a_1\dots a_{n-1}) \in \mathbb{R}^{n-1}$, a neighborhood $V$ for of $a_n\in\mathbb{R}$ and a function $f:U\subseteq\mathbb{R}^{n-1} \rightarrow V$ of class $C^1$ such that if $(x_1,x_2,\ldots,x_{n-1})\in U$ and $x_n \in V$ satisfy $F(x_1,x_2,\ldots,x_n)=c$ ,then $x_n = f(x_1,x_2,\ldots,x_{n-1})$ is representable as a function of $(x_1,\ldots,x_{n-1})$ .

I don't quite get what the theorem is trying to show. Can someone explain it? Is it just as simple as we just consider different part of the function?

-

Intuitively the implicit theorem is telling us that if a sufficiently smooth function $F$ defined on some Euclidean space (more generally on manifolds) satisfies a regularity condition then the equation $F(x_1,\cdots,x_n)=0$ can be locally "solved" for one of the coordinates.
For example, consider the map $F:\mathbb{R}^2\to\mathbb{R}$ defined $F(x,y)=x^2+y^2-1$. Note then that the equation $F(x,y)=0$ is nothing more than the usual locus for the unit circle $\mathbb{S}^1$. Consider the North pole of the cirlce, e.g. $(0,1)$, note then that $D_F(0,1)$ is nonsingular, and thus the IFT says that the equation $F(x,y)=0$ is locally solvable for one of the coordinates, say $y$. Of course this is true, locally around $(0,1)$ $\mathbb{S}^1$ one can solve the equation $x^2+y^2-1=0$ for $y$ to get $y=\sqrt{1-x^2}$.
Moreover, note that the validity of the theorem is further cemented by noting that while almost everywhere on $\mathbb{S}^1$ the equation $F(x,y)=0$ is locally solvable, there are two problem spots--the intersections with the $x$-axis. The reason why we might believe these to actually be problem spots is the second (easily deducible) interpretation of the IFT--if $F$ satisfies the regularity conditions at a point then the curve $F(x,y)=0$ locally looks like the graph of a (in this case) single-variable function. Going back to the previous paragraph, we see that locally at the North pole $\mathbb{S}^1$ does indeed look like the graph of $x\mapsto \sqrt{1-x^2}$. Moreover, now it's intuitively clear that the IFT should nto apply at the intersections with the $x$-axis since in any neighborhood of those points the curve $F(x,y)=0$ fails the "vertical line test" (i.e. isn't the graph of single-variable function). The reassuring part is that the IFT does not apply there since you can easily check, for example, that $D_F(1,0)$ is not invertible.
I think this is a fine explanation. However the part about $D_F(0,1)$ being invertible and $D_F(1,0)$ being non-invertible could perhaps be described more clearly: this Jacobian (assuming that is what you meant) is a nonsquare ($2\times 1$-) matrix. You are specifically considering one of its 'blocks', namely $\partial_yF$. So I would replace "solvable for one of the coordinates, say y" by " solvable for y". – wildildildlife Jan 9 '12 at 20:16