[proofplan]
The Hodge star is defined as the unique linear map $\star: \Lambda^p T_x^* M \to \Lambda^{n-p} T_x^* M$ satisfying $\alpha \wedge \star\beta = (\alpha, \beta)_g \, \omega_g$ for all $\alpha, \beta \in \Lambda^p T_x^* M$, where $(\cdot, \cdot)_g$ is the metric on $\Lambda^p$ induced by $g$ and $\omega_g$ is the Riemannian volume form. We verify the basis formula by substituting the candidate $\star \omega_I = \omega_{I^c}$ (with the sign fixed by the volume-form ordering) into the defining identity, evaluating against every basis multivector $\omega_J$ with $|J| = p$, and using orthonormality of the coframe to compute both sides explicitly. The case $J = I$ produces $\omega_g$ on each side; for $J \neq I$ both sides vanish because the wedge product contains a repeated factor.
[/proofplan]
[step:Set up the orthonormal coframe and the basis of $\Lambda^p T_x^* M$]
Fix $x \in M$ and an orthonormal coframe $\omega_1, \ldots, \omega_n$ for $T_x^* M$, meaning $(\omega_i, \omega_j)_g = \delta_{ij}$ where $(\cdot, \cdot)_g$ denotes the inner product on $T_x^* M$ induced by $g_x$ (musical isomorphism). The volume form at $x$ is
\begin{align*}
\omega_g = \omega_1 \wedge \omega_2 \wedge \cdots \wedge \omega_n,
\end{align*}
oriented so that $(\omega_1, \ldots, \omega_n)$ is positively oriented.
For each strictly increasing index set $K = \{k_1 < \cdots < k_p\} \subseteq \{1, \ldots, n\}$, write
\begin{align*}
\omega_K := \omega_{k_1} \wedge \omega_{k_2} \wedge \cdots \wedge \omega_{k_p} \in \Lambda^p T_x^* M.
\end{align*}
The collection $\{\omega_K : K \subseteq \{1,\ldots,n\}, |K| = p\}$ is a basis of $\Lambda^p T_x^* M$, and the induced inner product on $\Lambda^p T_x^* M$ — extended from $(\omega_i, \omega_j)_g = \delta_{ij}$ to $\Lambda^p$ via the determinant formula — satisfies
\begin{align*}
(\omega_K, \omega_L)_g = \det\big[(\omega_{k_a}, \omega_{l_b})_g\big]_{a,b} = \delta_{KL},
\end{align*}
where $\delta_{KL} = 1$ if $K = L$ and $0$ otherwise. Hence $\{\omega_K\}$ is an orthonormal basis of $\Lambda^p T_x^* M$.
[/step]
[step:State the defining identity for $\star$ as a linear map]
The Hodge star is the unique linear map
\begin{align*}
\star : \Lambda^p T_x^* M &\to \Lambda^{n-p} T_x^* M
\end{align*}
characterised by the identity
\begin{align*}
\alpha \wedge \star \beta = (\alpha, \beta)_g \cdot \omega_g \qquad \text{for all } \alpha, \beta \in \Lambda^p T_x^* M.
\end{align*}
Since $\{\omega_K\}_{|K|=p}$ is a basis, the map $\star$ is determined by its values on each $\omega_K$, and the defining identity for fixed $\beta = \omega_K$ is determined by its values against each basis element $\alpha = \omega_J$, $|J| = p$. Therefore $\star \omega_K$ is the unique $(n-p)$-form $\eta_K$ such that
\begin{align*}
\omega_J \wedge \eta_K = (\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g \qquad \text{for every } J \subseteq \{1,\ldots,n\} \text{ with } |J| = p.
\end{align*}
Our task is to show that the candidate $\eta_K := \omega_{K^c}$ — where $K^c = \{j_1 < \cdots < j_{n-p}\} = \{1,\ldots,n\} \setminus K$ is the increasing complement — satisfies this identity, after fixing the sign so that $\omega_K \wedge \omega_{K^c} = \omega_g$.
[/step]
[step:Define the sign $\varepsilon(K)$ and write the candidate $\star \omega_K = \varepsilon(K) \, \omega_{K^c}$]
For each increasing $K \subseteq \{1,\ldots,n\}$ with $|K| = p$, the wedge $\omega_K \wedge \omega_{K^c}$ uses each $\omega_i$ exactly once and equals a signed multiple of $\omega_g$:
\begin{align*}
\omega_K \wedge \omega_{K^c} = \varepsilon(K) \cdot \omega_g,
\end{align*}
where $\varepsilon(K) \in \{+1, -1\}$ is the sign of the permutation $(k_1, \ldots, k_p, j_1, \ldots, j_{n-p})$ relative to $(1, 2, \ldots, n)$ (the *shuffle sign* of $K$). For the special case $K = \{1, \ldots, p\}$, no shuffles are required and $\varepsilon(K) = +1$, giving $\omega_K \wedge \omega_{K^c} = \omega_g$ directly.
We define
\begin{align*}
\star \omega_K := \varepsilon(K) \cdot \omega_{K^c} \in \Lambda^{n-p} T_x^* M,
\end{align*}
and extend linearly to all of $\Lambda^p T_x^* M$. We now verify that this $\star \omega_K$ satisfies the defining identity $\omega_J \wedge \star \omega_K = \delta_{JK} \omega_g$.
[guided]
What should $\star \omega_K$ be? The defining identity at $\beta = \omega_K$ requires that $\star \omega_K$ is some $(n-p)$-form whose wedge against each $\omega_J$ ($|J|=p$) equals $\delta_{JK} \omega_g$. In particular, taking $J = K$ gives $\omega_K \wedge \star \omega_K = (\omega_K, \omega_K)_g \omega_g = \omega_g$. So we need an $(n-p)$-form that, wedged with $\omega_K$, produces $\omega_g$. The natural candidate is the basis $(n-p)$-form built from the indices *not* in $K$, namely $\omega_{K^c}$ — this is the unique basis multivector whose wedge with $\omega_K$ uses each $\omega_i$ exactly once and is therefore proportional to $\omega_g$. We compute the proportionality constant.
For increasing $K = \{k_1 < \cdots < k_p\}$ with complement $K^c = \{j_1 < \cdots < j_{n-p}\}$, the wedge $\omega_K \wedge \omega_{K^c} = \omega_{k_1} \wedge \cdots \wedge \omega_{k_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}}$ uses each $\omega_i$ exactly once. To match the canonical order $(1, 2, \ldots, n)$ defining $\omega_g$, we permute, picking up a sign equal to the sign of the permutation $(k_1, \ldots, k_p, j_1, \ldots, j_{n-p})$ relative to $(1, 2, \ldots, n)$. Call this sign $\varepsilon(K) \in \{+1, -1\}$ (the *shuffle sign* of $K$). Then
\begin{align*}
\omega_K \wedge \omega_{K^c} = \varepsilon(K) \cdot \omega_g.
\end{align*}
For the special case $K = \{1, \ldots, p\}$, the tuple $(1, \ldots, p, p+1, \ldots, n)$ is already in canonical order, no shuffles are required, and $\varepsilon(K) = +1$, so $\omega_K \wedge \omega_{K^c} = \omega_g$ directly.
This forces the sign in the definition of $\star$. Writing $\star \omega_K = c \cdot \omega_{K^c}$ for an unknown scalar $c$, the defining identity at $J = K$ reads $c \cdot \omega_K \wedge \omega_{K^c} = \omega_g$, i.e., $c \cdot \varepsilon(K) \omega_g = \omega_g$, forcing $c = \varepsilon(K)$ (since $\varepsilon(K)^2 = 1$). We therefore *define*
\begin{align*}
\star \omega_K := \varepsilon(K) \cdot \omega_{K^c} \in \Lambda^{n-p} T_x^* M,
\end{align*}
and extend linearly to all of $\Lambda^p T_x^* M$. The next two steps verify that this $\star \omega_K$ does satisfy the full defining identity $\omega_J \wedge \star \omega_K = \delta_{JK} \omega_g$ for every $J$, not just $J = K$.
The hypothesis stated in the theorem — "$I$ and $I^c$ arranged so that $\omega_{i_1} \wedge \cdots \wedge \omega_{i_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}} = \omega_g$" — is precisely the assertion $\varepsilon(I) = +1$. Under that hypothesis the formula simplifies to $\star \omega_I = \omega_{I^c}$, with no sign. The case $I = \{1, \ldots, p\}$ in the theorem's first display has $I^c = \{p+1, \ldots, n\}$, $\varepsilon(I) = +1$, and recovers $\star(\omega_1 \wedge \cdots \wedge \omega_p) = \omega_{p+1} \wedge \cdots \wedge \omega_n$ as a special case.
[/guided]
[/step]
[step:Verify the defining identity for $J = K$]
For $J = K$, evaluate the wedge:
\begin{align*}
\omega_K \wedge \star \omega_K = \omega_K \wedge \big[ \varepsilon(K) \cdot \omega_{K^c} \big] = \varepsilon(K) \cdot (\omega_K \wedge \omega_{K^c}) = \varepsilon(K) \cdot \varepsilon(K) \cdot \omega_g = \omega_g,
\end{align*}
where the last equality uses $\varepsilon(K)^2 = 1$. On the other side, $(\omega_K, \omega_K)_g \cdot \omega_g = 1 \cdot \omega_g = \omega_g$. The two sides agree:
\begin{align*}
\omega_K \wedge \star \omega_K = (\omega_K, \omega_K)_g \cdot \omega_g.
\end{align*}
[/step]
[step:Verify the defining identity for $J \neq K$ via repeated factors]
Fix increasing $J, K \subseteq \{1, \ldots, n\}$ with $|J| = |K| = p$ and $J \neq K$. We compute
\begin{align*}
\omega_J \wedge \star \omega_K = \varepsilon(K) \cdot \omega_J \wedge \omega_{K^c}.
\end{align*}
Since $J \neq K$, the set $J$ is not the increasing complement of $K^c$, so $J \cap K^c \neq \varnothing$: pick any $i \in J \cap K^c$. Then $\omega_i$ appears as a factor in $\omega_J$ and again as a factor in $\omega_{K^c}$. The wedge product of any multivector containing $\omega_i$ twice vanishes by skew-symmetry of $\wedge$:
\begin{align*}
\omega_J \wedge \omega_{K^c} = 0.
\end{align*}
(Justification of $J \cap K^c \neq \varnothing$: if $J \cap K^c = \varnothing$, then $J \subseteq K$, and since $|J| = |K|$ this forces $J = K$, contradicting $J \neq K$.)
Therefore $\omega_J \wedge \star \omega_K = 0$. On the other side of the defining identity,
\begin{align*}
(\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g = 0
\end{align*}
since $J \neq K$. The two sides agree.
[guided]
We need to check that the candidate $\star \omega_K = \varepsilon(K) \omega_{K^c}$ satisfies the defining identity not only at $J = K$ (handled in the previous step) but at *every* $J$ with $|J| = p$. The strategy is to show that both sides of $\omega_J \wedge \star \omega_K = (\omega_J, \omega_K)_g \omega_g$ vanish whenever $J \neq K$ — for the same structural reason on each side.
Fix increasing $J, K \subseteq \{1, \ldots, n\}$ with $|J| = |K| = p$ and $J \neq K$. Pulling out the scalar $\varepsilon(K)$,
\begin{align*}
\omega_J \wedge \star \omega_K = \omega_J \wedge \big[\varepsilon(K) \omega_{K^c}\big] = \varepsilon(K) \cdot \omega_J \wedge \omega_{K^c}.
\end{align*}
Why does $\omega_J \wedge \omega_{K^c}$ vanish? The wedge is a $p$-fold wedge times an $(n-p)$-fold wedge, so it lives in $\Lambda^n T_x^* M$, a one-dimensional space spanned by $\omega_g$. The wedge equals a non-zero multiple of $\omega_g$ if and only if it uses each coframe element $\omega_i$ exactly once — equivalently, $J \sqcup K^c = \{1, \ldots, n\}$, i.e., $J = K$. Whenever $J \neq K$ some index is repeated, and the wedge vanishes by skew-symmetry. Concretely: if $J \neq K$, then since $|J| = |K|$, $J$ cannot be contained in $K$ (otherwise $J = K$), so $J \cap K^c \neq \varnothing$. Pick any $i \in J \cap K^c$; then $\omega_i$ appears as a factor in $\omega_J$ and again in $\omega_{K^c}$, and
\begin{align*}
\omega_J \wedge \omega_{K^c} = 0.
\end{align*}
Therefore $\omega_J \wedge \star \omega_K = 0$.
On the right-hand side of the defining identity, the same disjointness condition appears through orthogonality: by the determinant formula for the induced inner product on $\Lambda^p T_x^* M$, $(\omega_J, \omega_K)_g = \det[(\omega_{j_a}, \omega_{k_b})_g]_{a,b} = \delta_{JK}$, since the matrix is a permutation matrix exactly when $J = K$ and otherwise has a zero row. So
\begin{align*}
(\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g = 0
\end{align*}
since $J \neq K$. Both sides vanish, and the defining identity holds at $(J, K)$ with $J \neq K$.
The structural moral: $\omega_J$ and $\omega_K$ "use up" different subsets of the coframe, and the wedge $\omega_J \wedge \omega_{K^c}$ vanishes precisely because the disjoint union $J \sqcup K^c$ fails to be all of $\{1, \ldots, n\}$ exactly once. The orthogonality $(\omega_J, \omega_K)_g = \delta_{JK}$ reflects exactly the same disjointness condition through the determinant formula — which is why both sides of the defining identity vanish in lockstep.
[/guided]
[/step]
[step:Combine the two cases to conclude]
For every $J, K$ with $|J| = |K| = p$,
\begin{align*}
\omega_J \wedge \star \omega_K = \delta_{JK} \cdot \omega_g = (\omega_J, \omega_K)_g \cdot \omega_g.
\end{align*}
Both sides of $\alpha \wedge \star \beta = (\alpha, \beta)_g \omega_g$ are bilinear in $(\alpha, \beta)$, and the basis $\{\omega_J\} \times \{\omega_K\}$ generates $\Lambda^p T_x^* M \times \Lambda^p T_x^* M$. Hence the identity extends by bilinearity to all $\alpha, \beta \in \Lambda^p T_x^* M$, and the defined map $\star: \Lambda^p T_x^* M \to \Lambda^{n-p} T_x^* M$ with
\begin{align*}
\star \omega_K = \varepsilon(K) \cdot \omega_{K^c}
\end{align*}
satisfies the defining identity for the Hodge star. By uniqueness of $\star$ (the identity $\alpha \wedge \star \beta = (\alpha, \beta)_g \omega_g$ characterises $\star \beta$ for each $\beta$, since the linear functional $\alpha \mapsto (\alpha, \beta)_g \omega_g$ has a unique representative under the perfect pairing $\Lambda^p \otimes \Lambda^{n-p} \to \Lambda^n \cong \mathbb{R}$ provided by $\wedge$), this is the Hodge star.
In particular, taking $K = \{1, \ldots, p\}$ gives $\varepsilon(K) = +1$, $K^c = \{p+1, \ldots, n\}$, and
\begin{align*}
\star(\omega_1 \wedge \cdots \wedge \omega_p) = \omega_{p+1} \wedge \cdots \wedge \omega_n.
\end{align*}
For general $I = \{i_1 < \cdots < i_p\}$ ordered so that $\omega_{i_1} \wedge \cdots \wedge \omega_{i_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}} = \omega_g$ — i.e., $\varepsilon(I) = +1$ — the formula reads
\begin{align*}
\star(\omega_{i_1} \wedge \cdots \wedge \omega_{i_p}) = \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}},
\end{align*}
as claimed. This completes the proof.
[/step]