[proofplan]
We prove that $\mathcal{F}_n$ is an isomorphism of $\Pi_n$ onto itself by verifying the explicit inversion formula. The argument has two parts: first, we substitute the definition of the DFT into the proposed inverse formula and exchange the order of summation; second, we evaluate the resulting geometric sum using the orthogonality relation $\sum_{j=0}^{n-1} \omega_n^{jk} = n\delta_{k,0 \bmod n}$, which causes the double sum to collapse to the identity.
[/proofplan]
[step:Establish the orthogonality relation for the $n$th roots of unity]
Let $\omega_n := e^{2\pi i / n}$ denote the primitive $n$th root of unity. We establish the identity
\begin{align*}
\sum_{j=0}^{n-1} \omega_n^{jk} = \begin{cases} n & \text{if } k \equiv 0 \pmod{n}, \\ 0 & \text{if } k \not\equiv 0 \pmod{n}. \end{cases}
\end{align*}
When $k \equiv 0 \pmod{n}$, each term $\omega_n^{jk} = (e^{2\pi i})^{jk/n} = 1$, so the sum equals $n$.
When $k \not\equiv 0 \pmod{n}$, the quantity $\omega_n^k \neq 1$ and the sum is a finite geometric series:
\begin{align*}
\sum_{j=0}^{n-1} (\omega_n^k)^j = \frac{(\omega_n^k)^n - 1}{\omega_n^k - 1} = \frac{(\omega_n^n)^k - 1}{\omega_n^k - 1} = \frac{1 - 1}{\omega_n^k - 1} = 0,
\end{align*}
since $\omega_n^n = e^{2\pi i} = 1$.
[guided]
The orthogonality of roots of unity is the engine behind the entire DFT inversion. Why does this identity hold? The $n$th roots of unity $1, \omega_n, \omega_n^2, \ldots, \omega_n^{n-1}$ are equally spaced on the unit circle in $\mathbb{C}$. When $k \not\equiv 0 \pmod{n}$, the map $j \mapsto \omega_n^{jk}$ permutes these roots (since $\gcd(k, n)$ divides into $n$ orbits, but the sum over a complete set of roots of any primitive root is zero). The algebraic proof via the geometric series formula makes this precise:
\begin{align*}
\sum_{j=0}^{n-1} (\omega_n^k)^j = \frac{(\omega_n^k)^n - 1}{\omega_n^k - 1}.
\end{align*}
The numerator vanishes because $(\omega_n^k)^n = (\omega_n^n)^k = 1^k = 1$. The denominator is nonzero because $\omega_n^k \neq 1$ when $k \not\equiv 0 \pmod{n}$. When $k \equiv 0 \pmod{n}$, every term is $1$ and the sum equals $n$.
[/guided]
[/step]
[step:Substitute the DFT definition into the proposed inverse and exchange summation]
The DFT is defined by $y_j := (\mathcal{F}_n x)_j = \sum_{r=0}^{n-1} \omega_n^{jr} x_r$ for $j = 0, \ldots, n-1$. We must verify that the proposed inverse formula recovers $x$. For each $\ell \in \{0, \ldots, n-1\}$, substitute the definition of $y_j$ into the candidate formula:
\begin{align*}
\frac{1}{n} \sum_{j=0}^{n-1} \omega_n^{-j\ell} y_j &= \frac{1}{n} \sum_{j=0}^{n-1} \omega_n^{-j\ell} \left( \sum_{r=0}^{n-1} \omega_n^{jr} x_r \right).
\end{align*}
All sums are finite (each has $n$ terms), so we may exchange the order of summation without justification:
\begin{align*}
\frac{1}{n} \sum_{j=0}^{n-1} \omega_n^{-j\ell} y_j &= \frac{1}{n} \sum_{r=0}^{n-1} x_r \left( \sum_{j=0}^{n-1} \omega_n^{j(r - \ell)} \right).
\end{align*}
[/step]
[step:Apply the orthogonality relation to collapse the sum to $x_\ell$]
Applying the orthogonality relation from the first step with $k = r - \ell$: since $r, \ell \in \{0, \ldots, n-1\}$, the difference $r - \ell$ lies in $\{-(n-1), \ldots, n-1\}$. Thus $r - \ell \equiv 0 \pmod{n}$ if and only if $r = \ell$ (the only solution in that range). Therefore
\begin{align*}
\sum_{j=0}^{n-1} \omega_n^{j(r-\ell)} = \begin{cases} n & \text{if } r = \ell, \\ 0 & \text{if } r \neq \ell. \end{cases}
\end{align*}
Substituting back:
\begin{align*}
\frac{1}{n} \sum_{j=0}^{n-1} \omega_n^{-j\ell} y_j = \frac{1}{n} \sum_{r=0}^{n-1} x_r \cdot n\delta_{r,\ell} = \frac{1}{n} \cdot n \cdot x_\ell = x_\ell.
\end{align*}
This holds for every $\ell \in \{0, \ldots, n-1\}$, so the proposed formula is indeed the inverse of $\mathcal{F}_n$.
[guided]
Substituting back into the double sum:
\begin{align*}
\frac{1}{n} \sum_{r=0}^{n-1} x_r \left( \sum_{j=0}^{n-1} \omega_n^{j(r-\ell)} \right) = \frac{1}{n} \left( x_\ell \cdot n + \sum_{r \neq \ell} x_r \cdot 0 \right) = x_\ell.
\end{align*}
The orthogonality relation acts as a sieve: the inner sum over $j$ picks out exactly the term $r = \ell$ and annihilates all others. This is the discrete analogue of the orthogonality of Fourier modes in $L^2$, where $\frac{1}{2\pi}\int_0^{2\pi} e^{i(r-\ell)\theta} \, d\theta = \delta_{r,\ell}$; here the integral is replaced by a finite sum and the $2\pi$ normalisation is replaced by $n$.
Since the formula $x_\ell = \frac{1}{n}\sum_{j=0}^{n-1} \omega_n^{-j\ell} y_j$ recovers $x$ from $y = \mathcal{F}_n x$ for every $x \in \Pi_n$, the map $\mathcal{F}_n: \Pi_n \to \Pi_n$ is invertible. In particular, $\mathcal{F}_n$ is injective (since $\mathcal{F}_n x = \mathbf{0}$ implies $x = \mathbf{0}$) and surjective (since every $y \in \Pi_n$ is the image of $x = \mathcal{F}_n^{-1}y$), confirming that $\mathcal{F}_n$ is an isomorphism of $\Pi_n$ onto itself.
[/guided]
[/step]
