Sphere eversion

$\iota$ and $\iota \circ a$ are regularly homotopic: by [F1] their formal data lie in one path component of $\mathrm{FImm}(S^2,{\mathbb{R}}^3)$, and the derivative map is a weak homotopy equivalence, hence a bijection on path components by [F2]; path components of $\mathrm{Imm}(S^2,{\mathbb{R}}^3)$ are the regular homotopy classes by [F2], so there is a regular homotopy $S^2\times [0,1]\to {\mathbb{R}}^3$ from $\iota$ to $\iota \circ a$. Follow this homotopy by $t\mapsto A_t\circ (\iota \circ a)$, where $A_t$ is a smooth rotation path from $I$ to $A=-r$. For a reflection in a plane with unit normal $u$, $A$ fixes $u$ and rotates $u^{\perp }$ by $\pi$, so rotation through $\pi t$ supplies this path. Reparametrizing both paths to be constant near their endpoints makes their concatenation smooth, with initial map $\iota$ and final map $r\circ \iota$.

$\mathrm{Imm}(S^2,{\mathbb{R}}^3)$ is path connected: by [F3] every two immersions of $S^2$ into ${\mathbb{R}}^3$ are regularly homotopic, and regular homotopies are paths in the immersion space by [F4].

No regular homotopy from $\iota$ to $r\circ \iota$ can be chosen through embeddings. Suppose $H:S^2\times [0,1]\to {\mathbb{R}}^3$ were such a family with every slice an embedding. Define the flux $S(t)={\int }_{S^2}{H}_t^{\ast }\omega$, where $\omega$ is the $2$-form of the field $\frac{1}{3}x$, that is, the integral over the parametrised surface of $\frac{1}{3}H\cdot ({\mathrm{\partial }}_{1}H\times {\mathrm{\partial }}_{2}H)$ in positively oriented local coordinates. The integrand depends continuously on $(x,t)$ and $S^2\times [0,1]$ is compact, so $S$ is continuous. For each $t$, $H_t$ is a smooth embedding of the compact sphere, so by [F5] its image bounds a compact region $B_t$; the divergence theorem in the form of [F6] identifies $S(t)$ with $\pm \mathrm{vol}(B_t)$, the sign being $+$ or $-$ according to the orientation of the parametrisation, so $S(t)\mathrm{\ne }0$ for every $t$; a continuous nonzero function on $[0,1]$ has constant sign.

Evaluating the two ends: for $H_0=\iota$ with the positively oriented coordinates of $S^2$ as the boundary of the unit ball, ${\iota }^{\ast }\omega$ is the outward-oriented flux form of $\frac{1}{3}x$ through the unit sphere, whose integral is the volume $\frac{4\pi }{3}$ of the unit ball by [F6]. For $H_1=r\circ \iota$ or $H_1=\iota \circ a=(-I)\circ \iota$, the chain rule gives ${\mathrm{\partial }}_i(r\circ \iota )=r\circ {\mathrm{\partial }}_i\iota$, and the identity $(Au)\times (Av)=\det (A)A(u\times v)$ for either orthogonal map with determinant $-1$ shows that the pulled-back flux form changes sign: ${\int }_{S^2}(r\circ \iota {)}^{\ast }\omega =-{\int }_{S^2}{\iota }^{\ast }\omega =-\frac{4\pi }{3}$. Hence $S(0)>0>S(1)$, contradicting the constant sign forced in step 1.3. Therefore no homotopy from $\iota$ to $r\circ \iota$ through embeddings exists, every regular homotopy between them has non-injective slices, and the inside/outside labelling necessarily changes along any eversion. The existence assertion of the theorem is step 1.1 and the path-connectedness is step 1.2; the Jordan–Brouwer input of step 1.3 carries AC, while the existence and classification assertions inherit countable choice from Smale–Hirsch.