Preimage Theorem
Theorem
Let $y$ be a regular value of a smooth submersion $f:X \to Y$.
Then the preimage $f^{-1}(y)$ is a smooth submanifold of $X$, with $\dim f^{-1}(y) = \dim X - \dim Y$.
In what context is $y$? Is it an element or a subset of $Y$?
You can help ProofWiki by explaining it.
To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
If you would welcome a second opinion as to whether your explanation is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Proof
Let $k,l$ be natural numbers with $k \geq l$.
By the Local Submersion Theorem, there exists coordinates in some open sets of $x,y$ such that $f(x_1, x_2, \ldots, x_k)=(x_1, \ldots,x_l)$ and $y$ corresponds to $(0, \ldots, 0)$.
Let $V$ be that neighborhood of $x$.
Then $f^{-1}(y) \cap V$ is the set of points where $x_1=0, \ldots, x_l=0$.
The functions $x_{l+1}, \ldots, x_k$ therefore form a coordinate system on the set $f^{-1}(y) \cap V$, which is a relatively open subset of $f^{-1}(y)$.
Together these functions then form a diffeomorphism to a Euclidean space.
We also have, by the regular value properties of $y$, a surjection of tangent spaces from $x$ to $y$.
This ensures smoothness of the solution set $f^{-1}(y)$.
$\blacksquare$
