[proofplan] We invoke the axiomatic characterisation of the [Exterior Derivative](/theorems/1525) as the unique $\mathbb{R}$-linear operator on $\Omega^*(U)$ satisfying the graded Leibniz rule, the nilpotency $d \circ d = 0$, and the identity $df = \sum_j (\partial_{x_j} f)\, dx_j$ on $0$-forms. By $\mathbb{R}$-linearity it suffices to compute $d(a_I\, dx_I)$ for a single monomial. The graded Leibniz rule, combined with $d(dx_I) = 0$ (proved by induction from $d \circ d = 0$ on the $0$-forms $x_{i_\ell}$), reduces this to $da_I \wedge dx_I$. Expanding $da_I$ via the formula for $d$ on $0$-forms yields the claimed coordinate formula. [/proofplan]

[step:Recall the defining properties of the exterior derivative on $\Omega^*(U)$]Let $\Omega^*(U) = \bigoplus_{k=0}^{n} \Omega^k(U)$ denote the graded $\mathbb{R}$-algebra of smooth differential forms on $U$, where $\Omega^0(U) = C^\infty(U)$. By the [Exterior Derivative](/theorems/1525) theorem there exists a unique family of $\mathbb{R}$-linear maps \begin{align*} d &: \Omega^k(U) \to \Omega^{k+1}(U), \qquad k = 0, 1, \dots, n, \end{align*} satisfying the following three properties: (D1) **Action on $0$-forms.** For every $f \in C^\infty(U) = \Omega^0(U)$, \begin{align*} df &= \sum_{j=1}^{n} \frac{\partial f}{\partial x_j} \, dx_j. \end{align*} (D2) **Graded Leibniz rule.** For all $\alpha \in \Omega^p(U)$ and $\beta \in \Omega^q(U)$, \begin{align*} d(\alpha \wedge \beta) &= d\alpha \wedge \beta + (-1)^{p}\, \alpha \wedge d\beta. \end{align*} (D3) **Nilpotency.** For every $\alpha \in \Omega^k(U)$, \begin{align*} d(d\alpha) &= 0. \end{align*} These three properties are the entire input to the proof.[/step]

[guided]The strategy of the proof is to use the three defining axioms of $d$ to compute $d\omega$ on a general $k$-form expressed in standard coordinates. We must be careful: nothing in the statement asserts that $d$ is *defined* by the coordinate formula; rather, $d$ is characterised by the axioms (D1)–(D3), and our task is to derive the formula as a *consequence*. Let us unpack each axiom briefly. - (D1) defines $d$ on $0$-forms. Here $\Omega^0(U) = C^\infty(U)$, and for $f \in C^\infty(U)$ the $1$-form $df$ is the ordinary total differential. In particular, taking $f = x_\ell$ — the $\ell$-th coordinate function on $U \subseteq \mathbb{R}^n$ — we obtain $d(x_\ell) = \sum_j (\partial_{x_j} x_\ell)\, dx_j = dx_\ell$ since $\partial_{x_j} x_\ell = \delta_{j\ell}$. Thus the symbol "$dx_\ell$" appearing in our wedge products is literally the $1$-form $d(x_\ell)$. - (D2) is the antiderivation property: $d$ behaves like a derivation, except that when it moves past a $p$-form it picks up the sign $(-1)^p$. The $\mathbb{R}$-linearity of $d$ is built into the statement that $d : \Omega^k(U) \to \Omega^{k+1}(U)$ is linear. - (D3) states $d \circ d = 0$, i.e., $d$ squared annihilates everything. Equivalently, the de Rham complex is a chain complex. We will combine these axioms to compute $d$ on a monomial $a_I\, dx_I$ and then sum.[/guided]

[step:Reduce to the case of a single monomial $a_I\, dx_I$ by $\mathbb{R}$-linearity]Since $d : \Omega^k(U) \to \Omega^{k+1}(U)$ is $\mathbb{R}$-linear by (D1)–(D3) of the previous step, and since $\omega = \sum_I a_I\, dx_I$ is a finite $\mathbb{R}$-linear combination of monomials $a_I\, dx_I$ (the multi-index $I$ ranges over the finite set of strictly increasing $k$-tuples in $\{1, \dots, n\}$), we have \begin{align*} d\omega &= \sum_{\substack{I \\ |I| = k}} d(a_I\, dx_I). \end{align*} It therefore suffices to prove \begin{align*} d(a_I\, dx_I) &= \sum_{j=1}^{n} \frac{\partial a_I}{\partial x_j} \, dx_j \wedge dx_I \tag{$\ast$} \end{align*} for each fixed strictly increasing multi-index $I = (i_1, \dots, i_k)$ and each $a_I \in C^\infty(U)$.[/step]

[guided]The reduction step is mechanical but worth making explicit: $\mathbb{R}$-linearity of $d$ means that for any finite collection of forms $\eta_1, \dots, \eta_N \in \Omega^k(U)$ and scalars $c_1, \dots, c_N \in \mathbb{R}$, \begin{align*} d\!\left(\sum_{r=1}^{N} c_r \eta_r\right) &= \sum_{r=1}^{N} c_r\, d\eta_r. \end{align*} Applying this with $\eta_I = a_I\, dx_I$ and $c_I = 1$ gives $d\omega = \sum_I d(a_I\, dx_I)$. Crucially the scalars $c_I$ are [real numbers](/page/Real%20Numbers), not functions; the coefficients $a_I$ are absorbed into the monomials themselves and require the graded Leibniz rule (D2) to be moved across $d$. That manipulation is the content of the next step.[/guided]

[step:Apply the graded Leibniz rule to split off the coefficient]Fix a strictly increasing multi-index $I = (i_1, \dots, i_k)$ and a coefficient $a_I \in C^\infty(U)$. The monomial $a_I \, dx_I = a_I \wedge dx_I$ is the wedge product of the $0$-form $a_I \in \Omega^0(U)$ with the $k$-form $dx_I \in \Omega^k(U)$. Applying (D2) with $\alpha = a_I$ (so $p = 0$) and $\beta = dx_I$: \begin{align*} d(a_I \, dx_I) &= d(a_I \wedge dx_I) \\ &= da_I \wedge dx_I + (-1)^{0}\, a_I \wedge d(dx_I) \\ &= da_I \wedge dx_I + a_I \wedge d(dx_I). \end{align*} In the next step we shall prove $d(dx_I) = 0$, which reduces this identity to \begin{align*} d(a_I \, dx_I) &= da_I \wedge dx_I. \tag{$\ast\ast$} \end{align*}[/step]

[guided]We are using the graded Leibniz rule (D2) on the factorisation $a_I \, dx_I = a_I \wedge dx_I$. The sign factor $(-1)^p$ in (D2) depends on the degree $p$ of the *left* factor; since $a_I$ is a $0$-form, $p = 0$ and the sign is $+1$, so no sign tracking is needed at this stage. The expression now has two terms: $da_I \wedge dx_I$ (the "good" term whose expansion will give the coordinate formula) and $a_I \wedge d(dx_I)$ (an "error" term we must show vanishes). The latter requires us to compute $d$ applied to a wedge of basic $1$-forms $dx_{i_1} \wedge \cdots \wedge dx_{i_k}$. This is where nilpotency (D3) enters: each $dx_{i_\ell}$ equals $d(x_{i_\ell})$, so $d(dx_{i_\ell}) = d(d(x_{i_\ell})) = 0$ by (D3), and the entire wedge $d(dx_I)$ collapses to $0$ via repeated applications of (D2). We do this carefully in the next step.[/guided]

[step:Prove $d(dx_I) = 0$ by induction on the length $k$ of the multi-index]We show by induction on $k \in \{0, 1, \dots, n\}$ that for every strictly increasing multi-index $I = (i_1, \dots, i_k)$ with entries in $\{1, \dots, n\}$, \begin{align*} d(dx_I) &= 0 \quad \text{in } \Omega^{k+1}(U). \end{align*} **Base case $k = 0$.** Here $dx_\varnothing = 1 \in C^\infty(U) = \Omega^0(U)$ is the constant function $1$. By (D1), \begin{align*} d(1) &= \sum_{j=1}^{n} \frac{\partial 1}{\partial x_j} \, dx_j = 0. \end{align*} **Base case $k = 1$.** Here $I = (i_1)$ with $i_1 \in \{1, \dots, n\}$, so $dx_I = dx_{i_1}$. The coordinate function $x_{i_1} \in C^\infty(U)$ satisfies, by (D1), \begin{align*} d(x_{i_1}) &= \sum_{j=1}^{n} \frac{\partial x_{i_1}}{\partial x_j} \, dx_j = \sum_{j=1}^{n} \delta_{j, i_1}\, dx_j = dx_{i_1}. \end{align*} Hence $dx_{i_1} = d(x_{i_1})$, and applying $d$ once more, \begin{align*} d(dx_{i_1}) &= d(d(x_{i_1})) = 0 \end{align*} by the nilpotency axiom (D3). **Inductive step.** Suppose $k \ge 1$ and the claim $d(dx_J) = 0$ holds for every strictly increasing multi-index $J$ of length $k$. Let $I = (i_1, \dots, i_k, i_{k+1})$ be a strictly increasing multi-index of length $k+1$, and write $J = (i_1, \dots, i_k)$, so that $dx_I = dx_J \wedge dx_{i_{k+1}}$ with $dx_J \in \Omega^k(U)$ and $dx_{i_{k+1}} \in \Omega^1(U)$. Apply (D2) with $\alpha = dx_J$ (so $p = k$) and $\beta = dx_{i_{k+1}}$: \begin{align*} d(dx_I) &= d(dx_J \wedge dx_{i_{k+1}}) \\ &= d(dx_J) \wedge dx_{i_{k+1}} + (-1)^k\, dx_J \wedge d(dx_{i_{k+1}}). \end{align*} By the inductive hypothesis $d(dx_J) = 0$. By the $k=1$ base case $d(dx_{i_{k+1}}) = 0$. Hence both terms vanish and $d(dx_I) = 0$, completing the induction.[/step]

[guided]The induction packages the computation cleanly, but the underlying mechanism is just two facts: 1. Every basic $1$-form $dx_\ell$ is the [exterior derivative](/theorems/1525) of the coordinate function $x_\ell$, i.e., $dx_\ell = d(x_\ell)$. This follows from (D1) applied to the coordinate function. 2. By nilpotency (D3), the [exterior derivative](/theorems/1525) of an [exterior derivative](/theorems/1525) is zero: $d(d(x_\ell)) = 0$, hence $d(dx_\ell) = 0$. For higher-degree wedges, the graded Leibniz rule (D2) lets us peel off factors one by one. At each peel, the new term $d(dx_{i_{k+1}})$ vanishes by step (2) above, and the remaining factor $d(dx_J)$ vanishes by induction. Why is the induction on the *length* of $I$, rather than, say, on $n$? Because the wedge $dx_I$ is built from $k$ basic factors, and the graded Leibniz rule attacks one factor at a time. The induction unwinds these factors one at a time, reducing each $k$-form to a wedge of one $1$-form (handled by $d \circ d = 0$) and a $(k-1)$-form (handled by the inductive hypothesis). A subtle point: nothing requires $I$ to be *strictly increasing* for the argument; the same induction works for arbitrary tuples. We restricted to strictly increasing $I$ only because that is the form in which $\omega$ is written in the statement.[/guided]

[step:Expand $da_I$ via the action of $d$ on $0$-forms and conclude]Combining the identity $(\ast\ast)$ from the Leibniz-rule step with the vanishing $d(dx_I) = 0$ just proved: \begin{align*} d(a_I \, dx_I) &= da_I \wedge dx_I. \end{align*} Now expand $da_I$ using (D1): \begin{align*} da_I &= \sum_{j=1}^{n} \frac{\partial a_I}{\partial x_j} \, dx_j. \end{align*} Substituting this into the previous identity and using $\mathbb{R}$-linearity of the wedge product in its left argument: \begin{align*} d(a_I \, dx_I) &= \left( \sum_{j=1}^{n} \frac{\partial a_I}{\partial x_j} \, dx_j \right) \wedge dx_I \\ &= \sum_{j=1}^{n} \frac{\partial a_I}{\partial x_j} \, dx_j \wedge dx_I, \end{align*} which is exactly the per-monomial identity $(\ast)$. Summing over the strictly increasing multi-indices $I$ with $|I| = k$ and invoking the linearity reduction from earlier: \begin{align*} d\omega &= \sum_{\substack{I \\ |I| = k}} d(a_I\, dx_I) = \sum_{\substack{I \\ |I| = k}} \sum_{j=1}^{n} \frac{\partial a_I}{\partial x_j} \, dx_j \wedge dx_I. \end{align*} The two parenthetical remarks in the statement now require no further argument: if $j \in \{i_1, \dots, i_k\}$ then $dx_j$ appears twice in the wedge $dx_j \wedge dx_I$, so this summand vanishes by antisymmetry of $\wedge$ in the basic $1$-forms; if $j \notin \{i_1, \dots, i_k\}$ then $dx_j \wedge dx_I$ is, up to a sign determined by the number of transpositions needed to re-sort the indices into increasing order, equal to a standard basis form $dx_{I'}$ where $I' = \{j\} \cup I$ is re-sorted. This completes the proof. $\blacksquare$[/step]

[guided]The final step is a substitution: we plug the explicit formula for $da_I$ on $0$-forms (provided by axiom (D1)) into the simplified Leibniz identity $d(a_I\, dx_I) = da_I \wedge dx_I$, then distribute the wedge product over the finite sum. The wedge product $\wedge : \Omega^1(U) \times \Omega^k(U) \to \Omega^{k+1}(U)$ is bilinear over $C^\infty(U)$, in particular $\mathbb{R}$-bilinear, so we may pull the sum over $j$ outside the wedge. Two clean-up observations close the proof: - *Repeated indices.* The basic $1$-forms $dx_1, \dots, dx_n$ generate the exterior algebra subject to $dx_i \wedge dx_i = 0$ for each $i$ (alternation). Hence if $j$ already appears among $i_1, \dots, i_k$ the summand $dx_j \wedge dx_I$ is automatically zero, and only the $n - k$ values of $j$ outside $I$ contribute non-trivially. - *Re-ordering.* When $j \notin I$, the wedge $dx_j \wedge dx_{i_1} \wedge \cdots \wedge dx_{i_k}$ is not in strictly increasing order. To express it in the standard basis we move $dx_j$ to its correct position by adjacent transpositions, each contributing a sign $-1$. If $j$ sits between $i_\ell$ and $i_{\ell+1}$, then $\ell$ transpositions are needed and the sign is $(-1)^\ell$. The statement of the theorem is in the un-reordered form $dx_j \wedge dx_I$, which is the cleanest way to write the coordinate formula; reordering is purely cosmetic and changes nothing about the form being represented. This concludes the derivation of the coordinate formula from the three defining axioms (D1)–(D3) of the [exterior derivative](/theorems/1525).[/guided]