[proofplan] We expand the pullback explicitly. Since pullback commutes with the [exterior derivative](/theorems/1525) and the wedge product, $f^*(dy_1 \wedge \cdots \wedge dy_n)$ equals the $n$-fold wedge product $df_1 \wedge \cdots \wedge df_n$. Expanding each one-form $df_i$ in the coordinate basis $(dx_1, \dots, dx_n)$ and using the alternating property of the wedge product collapses the sum from $n^n$ index tuples to $n!$ permutations. The signs produced by reordering the wedge factors back to the standard order combine with the partial derivatives to reproduce the Leibniz expansion of $\det(Jf_x)$. [/proofplan]

[step:Reduce the pullback to a wedge of differentials of the component functions]The pullback of $1$-forms by a smooth map satisfies $f^*(d\phi) = d(\phi \circ f)$ for any $\phi \in C^\infty(V)$, and pullback distributes over the wedge product: $f^*(\alpha \wedge \beta) = f^*\alpha \wedge f^*\beta$ for any forms $\alpha, \beta$. Applying these identities with $\phi = y_i$ (so that $y_i \circ f = f_i$), we obtain \begin{align*} f^*(dy_1 \wedge \cdots \wedge dy_n) = (f^* dy_1) \wedge \cdots \wedge (f^* dy_n) = df_1 \wedge \cdots \wedge df_n. \end{align*}[/step]

[guided]The first task is to convert the pullback, which is defined abstractly, into a concrete expression in the coordinates $(x_1, \dots, x_n)$ on $U$. Two structural properties of pullback do this work. **Property 1 — Naturality of the [exterior derivative](/theorems/1525).** For any smooth $\phi: V \to \mathbb{R}$, the pullback of the $1$-form $d\phi$ is $f^*(d\phi) = d(\phi \circ f)$. Applied to the coordinate function $\phi = y_i: V \to \mathbb{R}$, this gives $f^*(dy_i) = d(y_i \circ f) = df_i$, since $y_i \circ f = f_i$ by definition of the components of $f$. **Property 2 — Pullback distributes over the wedge product.** For any forms $\alpha, \beta$ on $V$, $f^*(\alpha \wedge \beta) = f^*\alpha \wedge f^*\beta$. Iterating $n - 1$ times, \begin{align*} f^*(dy_1 \wedge \cdots \wedge dy_n) = (f^* dy_1) \wedge \cdots \wedge (f^* dy_n). \end{align*} Combining these, \begin{align*} f^*(dy_1 \wedge \cdots \wedge dy_n) = df_1 \wedge \cdots \wedge df_n. \end{align*} The geometric idea is that pulling back a top form on $V$ by $f$ measures how $f$ distorts $n$-dimensional volume locally, and this distortion factor is recorded entirely by the differentials of the component functions of $f$.[/guided]

[step:Expand each $df_i$ in the coordinate basis and apply multilinearity]Each $df_i$ is a smooth $1$-form on $U$, so by the coordinate expansion of a $1$-form, \begin{align*} df_i = \sum_{j=1}^n \partial_{x_j} f_i \, dx_j, \qquad i = 1, \dots, n. \end{align*} The wedge product is multilinear over $C^\infty(U)$ in each slot. Expanding the $n$-fold wedge yields \begin{align*} df_1 \wedge \cdots \wedge df_n = \sum_{j_1 = 1}^n \cdots \sum_{j_n = 1}^n \left( \prod_{i=1}^n \partial_{x_{j_i}} f_i \right) dx_{j_1} \wedge \cdots \wedge dx_{j_n}. \end{align*}[/step]

[guided]We have reduced the problem to computing the wedge product of $n$ explicit $1$-forms. Each $df_i$ is a smooth $1$-form on $U$, and the coordinate basis $(dx_1, \dots, dx_n)$ for the cotangent space at each point gives the pointwise expansion \begin{align*} df_i(x) = \sum_{j=1}^n \frac{\partial f_i}{\partial x_j}(x) \, dx_j, \qquad i = 1, \dots, n, \end{align*} which we abbreviate to $df_i = \sum_{j=1}^n \partial_{x_j} f_i \, dx_j$. To wedge these together, we use that the wedge product is **multilinear over $C^\infty(U)$** in each of its slots: scalars (smooth functions on $U$) can be pulled out, and sums distribute. Distributing across all $n$ slots, \begin{align*} df_1 \wedge \cdots \wedge df_n = \left(\sum_{j_1} \partial_{x_{j_1}} f_1 \, dx_{j_1}\right) \wedge \cdots \wedge \left(\sum_{j_n} \partial_{x_{j_n}} f_n \, dx_{j_n}\right) = \sum_{j_1, \dots, j_n = 1}^n \left( \prod_{i=1}^n \partial_{x_{j_i}} f_i \right) dx_{j_1} \wedge \cdots \wedge dx_{j_n}. \end{align*} The sum has $n^n$ index tuples $(j_1, \dots, j_n) \in \{1, \dots, n\}^n$. Most of them will turn out to contribute zero.[/guided]

[step:Discard terms with repeated indices using the alternating property]The wedge product on $1$-forms is alternating: $dx_a \wedge dx_b = -\, dx_b \wedge dx_a$, and in particular $dx_a \wedge dx_a = 0$. Consequently, whenever the index tuple $(j_1, \dots, j_n)$ has a repeated entry, the wedge $dx_{j_1} \wedge \cdots \wedge dx_{j_n}$ vanishes. The only tuples that survive are those with all indices distinct, i.e., those of the form $(\sigma(1), \dots, \sigma(n))$ for some permutation $\sigma \in S_n$. Thus \begin{align*} df_1 \wedge \cdots \wedge df_n = \sum_{\sigma \in S_n} \left( \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i \right) dx_{\sigma(1)} \wedge \cdots \wedge dx_{\sigma(n)}. \end{align*}[/step]

[guided]The wedge product of $1$-forms is **alternating**: for any two $1$-forms $\alpha, \beta$, we have $\alpha \wedge \beta = -\, \beta \wedge \alpha$, and in particular $\alpha \wedge \alpha = 0$. More generally, if among $1$-forms $\alpha_1, \dots, \alpha_n$ any two are equal (say $\alpha_a = \alpha_b$ for $a \ne b$), then $\alpha_1 \wedge \cdots \wedge \alpha_n = 0$, because we can swap these two adjacent-up-to-sign factors and produce the same expression with opposite sign. Apply this to our sum. A summand indexed by $(j_1, \dots, j_n)$ contains the wedge $dx_{j_1} \wedge \cdots \wedge dx_{j_n}$. If $j_a = j_b$ for some $a \ne b$, this wedge is zero, and the entire summand vanishes — regardless of the value of the coefficient $\prod_i \partial_{x_{j_i}} f_i$. So only tuples $(j_1, \dots, j_n)$ with **pairwise distinct** entries from $\{1, \dots, n\}$ contribute. Such a tuple is precisely a bijection $i \mapsto j_i$ from $\{1, \dots, n\}$ to itself, i.e., a permutation $\sigma \in S_n$, with $j_i = \sigma(i)$. The number of surviving tuples drops from $n^n$ to $n!$, namely \begin{align*} df_1 \wedge \cdots \wedge df_n = \sum_{\sigma \in S_n} \left( \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i \right) dx_{\sigma(1)} \wedge \cdots \wedge dx_{\sigma(n)}. \end{align*} This is where the Jacobian's structure first becomes visible: we are now summing over permutations, which is exactly the index set of the Leibniz expansion of a determinant.[/guided]

[step:Reorder each permuted wedge to the standard order, producing the sign of the permutation]For each $\sigma \in S_n$, repeated application of the antisymmetry $dx_a \wedge dx_b = -\, dx_b \wedge dx_a$ allows us to reorder the factors $dx_{\sigma(1)}, \dots, dx_{\sigma(n)}$ into the standard order $dx_1, \dots, dx_n$. The number of adjacent transpositions required has the same parity as $\sigma$, so the reordering produces a factor of $\operatorname{sgn}(\sigma) \in \{+1, -1\}$: \begin{align*} dx_{\sigma(1)} \wedge \cdots \wedge dx_{\sigma(n)} = \operatorname{sgn}(\sigma) \, dx_1 \wedge \cdots \wedge dx_n. \end{align*} Substituting, \begin{align*} df_1 \wedge \cdots \wedge df_n = \left( \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i \right) dx_1 \wedge \cdots \wedge dx_n. \end{align*}[/step]

[guided]We now have $n!$ surviving terms, each containing a wedge $dx_{\sigma(1)} \wedge \cdots \wedge dx_{\sigma(n)}$ where the factors appear in the order determined by $\sigma$. To produce a single common wedge factor that we can pull outside the sum, we reorder each of these wedges into the standard order $dx_1 \wedge \cdots \wedge dx_n$. Each swap of two adjacent factors flips the sign by the antisymmetry rule $dx_a \wedge dx_b = -\, dx_b \wedge dx_a$. To reorder $dx_{\sigma(1)}, \dots, dx_{\sigma(n)}$ into $dx_1, \dots, dx_n$, one performs a sequence of adjacent transpositions; the total number of swaps has the same parity as $\sigma$ (since every permutation factors into transpositions, and parity is well-defined). The sign of the permutation $\operatorname{sgn}(\sigma) \in \{+1, -1\}$ — defined as $+1$ if $\sigma$ is even and $-1$ if odd — is precisely the cumulative sign: \begin{align*} dx_{\sigma(1)} \wedge \cdots \wedge dx_{\sigma(n)} = \operatorname{sgn}(\sigma) \, dx_1 \wedge \cdots \wedge dx_n. \end{align*} Substituting back, \begin{align*} df_1 \wedge \cdots \wedge df_n = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \left( \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i \right) dx_1 \wedge \cdots \wedge dx_n = \left( \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i \right) dx_1 \wedge \cdots \wedge dx_n, \end{align*} where in the last step we use that $dx_1 \wedge \cdots \wedge dx_n$ is independent of $\sigma$ and can be pulled out of the sum.[/guided]

[step:Identify the coefficient as the determinant of the Jacobian via the Leibniz formula]The Leibniz formula for the determinant states that for any matrix $A \in \mathbb{R}^{n \times n}$, \begin{align*} \det A = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n A_{i, \sigma(i)}. \end{align*} Apply this with $A = Jf_x$, whose entries are $(Jf_x)_{i, \sigma(i)} = \partial_{x_{\sigma(i)}} f_i(x)$. The coefficient appearing in the previous step is exactly this Leibniz sum evaluated at $A = Jf_x$: \begin{align*} \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i(x) = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n (Jf_x)_{i, \sigma(i)} = \det(Jf_x). \end{align*} Combining the equalities from this step and the previous ones, \begin{align*} (f^*\omega)_x = (df_1 \wedge \cdots \wedge df_n)_x = \det(Jf_x) \, (dx_1 \wedge \cdots \wedge dx_n)_x, \end{align*} which is the claimed identity. Since $x \in U$ was arbitrary, the identity holds at every point of $U$.[/step]

[guided]The coefficient \begin{align*} \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i(x) \end{align*} is the Leibniz expansion of a determinant in disguise. Recall the [Leibniz formula](/theorems/917): for any $A \in \mathbb{R}^{n \times n}$, \begin{align*} \det A = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n A_{i, \sigma(i)}. \end{align*} We identify our coefficient with this expression by reading off the matrix $A$ from the integrand. The Jacobian matrix $Jf_x$ has entries $(Jf_x)_{ij} = \partial_{x_j} f_i(x)$, so \begin{align*} (Jf_x)_{i, \sigma(i)} = \partial_{x_{\sigma(i)}} f_i(x). \end{align*} Hence $\prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i(x) = \prod_{i=1}^n (Jf_x)_{i, \sigma(i)}$, and our coefficient is precisely $\det(Jf_x)$. It is worth double-checking the index convention. The standard convention adopted in §0 of the notation guide is that the Jacobian matrix represents the total derivative $Df_x: \mathbb{R}^n \to \mathbb{R}^n$ in the standard bases, with rows indexed by the components $f_i$ of $f$ and columns indexed by the input coordinates $x_j$: that is, $(Jf_x)_{ij} = \partial_{x_j} f_i(x)$. Reading $A_{i, \sigma(i)}$ off this matrix gives exactly $\partial_{x_{\sigma(i)}} f_i$, matching what appears in our sum. (If one used the transposed convention $(Jf_x)_{ij} = \partial_{x_i} f_j$, the same computation would give $\det((Jf_x)^\top) = \det(Jf_x)$, so the determinant — being invariant under transpose — agrees in either convention. This is reassuring rather than essential.) Chaining the equalities established in Steps 1–4 with this identification of the determinant, at every $x \in U$ we have \begin{align*} (f^*\omega)_x &= (df_1 \wedge \cdots \wedge df_n)_x && \text{(Step 1)} \\ &= \left( \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_{i=1}^n \partial_{x_{\sigma(i)}} f_i(x) \right) (dx_1 \wedge \cdots \wedge dx_n)_x && \text{(Steps 2–4)} \\ &= \det(Jf_x) \, (dx_1 \wedge \cdots \wedge dx_n)_x && \text{(Leibniz formula)}. \end{align*} Since $x \in U$ was arbitrary, this gives the equality of $n$-forms on $U$, \begin{align*} f^*(dy_1 \wedge \cdots \wedge dy_n) = \det(Jf_x) \, dx_1 \wedge \cdots \wedge dx_n, \end{align*} completing the proof.[/guided]