[proofplan] We verify the two defining properties of a smooth $k$-form: (i) at each point $x \in U$, the multilinear form $(f^*\omega)_x$ is alternating and $k$-multilinear, and (ii) the coefficient functions of $f^*\omega$ are smooth on $U$. Property (i) follows from a direct pointwise calculation that exploits the linearity of $Df_x$ and the alternating multilinearity of $\omega_{f(x)}$. Property (ii) is obtained by expanding $\omega$ in coordinates on $V$, applying the pullback formula, and observing that the resulting coefficients on $U$ are finite sums of products of $C^\infty$ functions — namely, compositions $a_I \circ f$ and partial derivatives $\partial_{x_j} f_i$. [/proofplan] [step:Establish the pullback formula on multivectors at a single point] Fix $x \in U$. By the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323), the total derivative $Df_x: \mathbb{R}^m \to \mathbb{R}^n$ is a [linear map](/page/Linear%20Map), with matrix representation $(Jf_x)_{ij} = \partial_{x_j} f_i(x)$. By hypothesis, $\omega_{f(x)} \in \Lambda^k(\mathbb{R}^n)^*$ is an alternating $k$-multilinear form on $\mathbb{R}^n$. The definition \begin{align*} (f^*\omega)_x(v_1, \ldots, v_k) = \omega_{f(x)}\bigl(Df_x(v_1), \ldots, Df_x(v_k)\bigr) \end{align*} therefore makes sense for all $(v_1, \ldots, v_k) \in (\mathbb{R}^m)^k$. [guided] We begin by checking that the pointwise definition is meaningful. Fix $x \in U$. What objects are in play? - The total derivative $Df_x: \mathbb{R}^m \to \mathbb{R}^n$ is a [linear map](/page/Linear%20Map); this is the content of the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323), which records that $f$ smooth implies $Df_x$ exists and is linear, with matrix entries $(Jf_x)_{ij} = \partial_{x_j} f_i(x)$. - The form $\omega_{f(x)}$ is, by the hypothesis $\omega \in \Omega^k(V)$, an alternating $k$-multilinear form on $\mathbb{R}^n$, i.e., an element of $\Lambda^k(\mathbb{R}^n)^*$. Given $v_1, \ldots, v_k \in \mathbb{R}^m$, the vectors $Df_x(v_1), \ldots, Df_x(v_k)$ are well-defined elements of $\mathbb{R}^n$, so we may feed them into $\omega_{f(x)}$. The definition \begin{align*} (f^*\omega)_x(v_1, \ldots, v_k) := \omega_{f(x)}\bigl(Df_x(v_1), \ldots, Df_x(v_k)\bigr) \end{align*} therefore produces a real number for each input $(v_1, \ldots, v_k) \in (\mathbb{R}^m)^k$. It remains to verify that this assignment is alternating multilinear in the inputs (Step 2) and depends smoothly on $x$ (Steps 3–4). [/guided] [/step] [step:Verify that $(f^*\omega)_x$ is alternating and $k$-multilinear] Fix $x \in U$. We verify multilinearity: for any $i \in \{1, \ldots, k\}$, vectors $v_1, \ldots, v_k, v_i' \in \mathbb{R}^m$, and scalars $\alpha, \beta \in \mathbb{R}$, the linearity of $Df_x$ gives \begin{align*} Df_x(\alpha v_i + \beta v_i') = \alpha\, Df_x(v_i) + \beta\, Df_x(v_i'). \end{align*} Substituting into the definition and using multilinearity of $\omega_{f(x)}$ in the $i$-th slot, \begin{align*} (f^*\omega)_x(v_1, \ldots, \alpha v_i + \beta v_i', \ldots, v_k) &= \omega_{f(x)}\bigl(\ldots, \alpha\, Df_x(v_i) + \beta\, Df_x(v_i'), \ldots\bigr) \\ &= \alpha\, (f^*\omega)_x(v_1, \ldots, v_i, \ldots, v_k) + \beta\, (f^*\omega)_x(v_1, \ldots, v_i', \ldots, v_k). \end{align*} We verify the alternating property: if $v_i = v_j$ for some $i \neq j$, then $Df_x(v_i) = Df_x(v_j)$, and the alternating property of $\omega_{f(x)}$ gives $\omega_{f(x)}\bigl(Df_x(v_1), \ldots, Df_x(v_k)\bigr) = 0$, hence $(f^*\omega)_x(v_1, \ldots, v_k) = 0$. Therefore $(f^*\omega)_x \in \Lambda^k(\mathbb{R}^m)^*$. [guided] We must check the two defining properties of an alternating $k$-multilinear form on $\mathbb{R}^m$: multilinearity (linear in each of the $k$ inputs separately) and the alternating property (the form vanishes whenever two inputs coincide). Both properties propagate from $\omega_{f(x)}$ through $Df_x$ — but we should verify each one explicitly, because the propagation relies on the linearity of $Df_x$. **Multilinearity.** Fix the $i$-th slot. The key observation is that $Df_x$ is linear (by definition of the total derivative), so \begin{align*} Df_x(\alpha v_i + \beta v_i') = \alpha\, Df_x(v_i) + \beta\, Df_x(v_i'). \end{align*} Inserting this into the $i$-th argument of $\omega_{f(x)}$ and using multilinearity of $\omega_{f(x)}$, \begin{align*} (f^*\omega)_x(v_1, \ldots, \alpha v_i + \beta v_i', \ldots, v_k) &= \omega_{f(x)}\bigl(Df_x(v_1), \ldots, \alpha\, Df_x(v_i) + \beta\, Df_x(v_i'), \ldots, Df_x(v_k)\bigr) \\ &= \alpha\, \omega_{f(x)}\bigl(\ldots, Df_x(v_i), \ldots\bigr) + \beta\, \omega_{f(x)}\bigl(\ldots, Df_x(v_i'), \ldots\bigr) \\ &= \alpha\, (f^*\omega)_x(v_1, \ldots, v_i, \ldots, v_k) + \beta\, (f^*\omega)_x(v_1, \ldots, v_i', \ldots, v_k). \end{align*} Since $i$ was arbitrary, $(f^*\omega)_x$ is linear in each argument. **Alternating.** Suppose $v_i = v_j$ with $i \neq j$. Then $Df_x(v_i) = Df_x(v_j)$ — note that this requires no injectivity of $Df_x$; it is a direct consequence of $Df_x$ being a function. Since $\omega_{f(x)}$ is alternating, it vanishes whenever two of its arguments coincide: \begin{align*} (f^*\omega)_x(v_1, \ldots, v_k) = \omega_{f(x)}\bigl(Df_x(v_1), \ldots, Df_x(v_k)\bigr) = 0. \end{align*} Therefore $(f^*\omega)_x \in \Lambda^k(\mathbb{R}^m)^*$ for every $x \in U$. [/guided] [/step] [step:Expand $\omega$ in coordinates and derive the coordinate formula for $f^*\omega$] Let $(y_1, \ldots, y_n)$ denote the standard coordinates on $V \subseteq \mathbb{R}^n$ and $(x_1, \ldots, x_m)$ the standard coordinates on $U \subseteq \mathbb{R}^m$. Let \begin{align*} \mathcal{I}_k^n := \{ I = (i_1, \ldots, i_k) \in \{1, \ldots, n\}^k : i_1 < i_2 < \cdots < i_k \} \end{align*} denote the set of strictly increasing $k$-multi-indices in $\{1, \ldots, n\}$, and analogously define $\mathcal{I}_k^m$. By definition of $\Omega^k(V)$, there exist unique smooth coefficient functions $a_I \in C^\infty(V)$ for each $I \in \mathcal{I}_k^n$ such that \begin{align*} \omega = \sum_{I \in \mathcal{I}_k^n} a_I\, dy_{i_1} \wedge \cdots \wedge dy_{i_k}. \end{align*} By the alternating multilinearity established in Step 2, for any covectors $\alpha_1, \ldots, \alpha_k \in (\mathbb{R}^n)^*$, \begin{align*} f^*(\alpha_1 \wedge \cdots \wedge \alpha_k) = (f^*\alpha_1) \wedge \cdots \wedge (f^*\alpha_k), \end{align*} where for a $1$-form $\alpha$ on $V$ we have $(f^*\alpha)_x(v) = \alpha_{f(x)}(Df_x(v))$. Applying this to $\alpha_\ell = dy_{i_\ell}$ and using \begin{align*} (f^*dy_i)_x(v) = dy_i\bigl(Df_x(v)\bigr) = (Df_x(v))_i = \sum_{j=1}^m \partial_{x_j} f_i(x)\, v_j, \end{align*} we obtain $f^*dy_i = df_i = \sum_{j=1}^m \partial_{x_j} f_i\, dx_j$ for each $i \in \{1, \ldots, n\}$. Combining, \begin{align*} f^*\omega = \sum_{I \in \mathcal{I}_k^n} (a_I \circ f)\, df_{i_1} \wedge \cdots \wedge df_{i_k}. \end{align*} [guided] We now translate the abstract pointwise definition into an explicit coordinate formula. The goal is to write $f^*\omega$ as a finite sum of smooth coefficients times wedge products of the standard $dx_j$'s on $U$; once we have this, smoothness will follow immediately in Step 4. **Expand $\omega$.** By definition of $\Omega^k(V)$, the form $\omega$ admits a unique representation \begin{align*} \omega = \sum_{I \in \mathcal{I}_k^n} a_I\, dy_{i_1} \wedge \cdots \wedge dy_{i_k}, \end{align*} where $\mathcal{I}_k^n = \{I = (i_1 < \cdots < i_k)\}$ indexes strictly increasing $k$-tuples and the coefficients $a_I: V \to \mathbb{R}$ are smooth. **Pullback commutes with wedge products.** We claim that for $1$-forms $\alpha_1, \ldots, \alpha_k$ on $V$, \begin{align*} f^*(\alpha_1 \wedge \cdots \wedge \alpha_k) = (f^*\alpha_1) \wedge \cdots \wedge (f^*\alpha_k). \end{align*} Why? Both sides are alternating multilinear forms on $\mathbb{R}^m$ (Step 2), and evaluation on vectors $v_1, \ldots, v_k \in \mathbb{R}^m$ at the point $x \in U$ gives, by the definition of wedge product as a sum over permutations $\sigma \in S_k$ with sign $\mathrm{sgn}(\sigma)$, \begin{align*} \bigl(f^*(\alpha_1 \wedge \cdots \wedge \alpha_k)\bigr)_x(v_1, \ldots, v_k) &= (\alpha_1 \wedge \cdots \wedge \alpha_k)_{f(x)}\bigl(Df_x(v_1), \ldots, Df_x(v_k)\bigr) \\ &= \sum_{\sigma \in S_k} \mathrm{sgn}(\sigma)\, \prod_{\ell=1}^k (\alpha_\ell)_{f(x)}\bigl(Df_x(v_{\sigma(\ell)})\bigr) \\ &= \sum_{\sigma \in S_k} \mathrm{sgn}(\sigma)\, \prod_{\ell=1}^k (f^*\alpha_\ell)_x(v_{\sigma(\ell)}) \\ &= \bigl((f^*\alpha_1) \wedge \cdots \wedge (f^*\alpha_k)\bigr)_x(v_1, \ldots, v_k). \end{align*} **Pullback of a coordinate differential.** For the coordinate $1$-form $dy_i$ on $V$ (whose value at any point is the linear functional "extract the $i$-th component"), we compute, for $x \in U$ and $v \in \mathbb{R}^m$, \begin{align*} (f^*dy_i)_x(v) = dy_i\bigl(Df_x(v)\bigr) = (Df_x(v))_i. \end{align*} Since the matrix representation of $Df_x$ is the Jacobian $Jf_x$ with entries $(Jf_x)_{ij} = \partial_{x_j} f_i(x)$, we have $(Df_x(v))_i = \sum_{j=1}^m \partial_{x_j} f_i(x)\, v_j$. This is exactly $df_i(v)$, the standard differential of the scalar function $f_i: U \to \mathbb{R}$: \begin{align*} f^*dy_i = df_i = \sum_{j=1}^m \partial_{x_j} f_i\, dx_j. \end{align*} **Pullback of $\omega$.** Combining the linearity of the pullback (immediate from its definition) with the two computations above, \begin{align*} f^*\omega = \sum_{I \in \mathcal{I}_k^n} f^*(a_I\, dy_{i_1} \wedge \cdots \wedge dy_{i_k}) = \sum_{I \in \mathcal{I}_k^n} (a_I \circ f)\, df_{i_1} \wedge \cdots \wedge df_{i_k}. \end{align*} The scalar coefficient $a_I \circ f$ comes out because pullback of a $0$-form (a function) is just precomposition with $f$, and the wedge product distributes by the previous claim. [/guided] [/step] [step:Expand the wedge products and identify smooth coefficient functions] Substituting $df_{i_\ell} = \sum_{j_\ell = 1}^m \partial_{x_{j_\ell}} f_{i_\ell}\, dx_{j_\ell}$ into the formula from Step 3 and expanding the wedge by multilinearity, \begin{align*} f^*\omega = \sum_{I \in \mathcal{I}_k^n} (a_I \circ f) \sum_{(j_1, \ldots, j_k) \in \{1, \ldots, m\}^k} \prod_{\ell=1}^k \partial_{x_{j_\ell}} f_{i_\ell}\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}. \end{align*} For each strictly increasing $J = (j_1 < \cdots < j_k) \in \mathcal{I}_k^m$, the alternating identity $dx_{\sigma(j_1)} \wedge \cdots \wedge dx_{\sigma(j_k)} = \mathrm{sgn}(\sigma)\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}$ for $\sigma \in S_k$ allows us to collect terms into the standard basis, yielding \begin{align*} f^*\omega = \sum_{J \in \mathcal{I}_k^m} b_J\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}, \end{align*} where the coefficient $b_J: U \to \mathbb{R}$ is the finite sum \begin{align*} b_J = \sum_{I \in \mathcal{I}_k^n} (a_I \circ f) \sum_{\sigma \in S_k} \mathrm{sgn}(\sigma) \prod_{\ell=1}^k \partial_{x_{j_{\sigma(\ell)}}} f_{i_\ell}. \end{align*} [guided] We now write the formula from Step 3 in the standard basis $\{dx_{j_1} \wedge \cdots \wedge dx_{j_k} : J \in \mathcal{I}_k^m\}$ of $\Lambda^k(\mathbb{R}^m)^*$, so we can read off the coefficient functions $b_J: U \to \mathbb{R}$. **Expand each $df_{i_\ell}$.** Substituting $df_{i_\ell} = \sum_{j_\ell = 1}^m \partial_{x_{j_\ell}} f_{i_\ell}\, dx_{j_\ell}$ and distributing the wedge over the sum (using multilinearity of $\wedge$ in each slot), \begin{align*} df_{i_1} \wedge \cdots \wedge df_{i_k} = \sum_{(j_1, \ldots, j_k) \in \{1, \ldots, m\}^k} \prod_{\ell=1}^k \partial_{x_{j_\ell}} f_{i_\ell}\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}. \end{align*} This is a finite sum of $m^k$ terms. **Reduce to strictly increasing multi-indices.** Many of these terms either vanish or are sign-equivalent to a term with strictly increasing indices. Specifically, if any two of $j_1, \ldots, j_k$ coincide, the wedge $dx_{j_1} \wedge \cdots \wedge dx_{j_k}$ vanishes (since the wedge is alternating). Otherwise, there is a unique $J = (j_1' < \cdots < j_k') \in \mathcal{I}_k^m$ and a unique $\sigma \in S_k$ such that $j_\ell = j_{\sigma(\ell)}'$, and \begin{align*} dx_{j_1} \wedge \cdots \wedge dx_{j_k} = \mathrm{sgn}(\sigma)\, dx_{j_1'} \wedge \cdots \wedge dx_{j_k'}. \end{align*} Collecting terms by their strictly increasing target multi-index $J$, \begin{align*} f^*\omega = \sum_{J \in \mathcal{I}_k^m} b_J\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}, \end{align*} where, writing $J = (j_1 < \cdots < j_k)$, \begin{align*} b_J = \sum_{I \in \mathcal{I}_k^n} (a_I \circ f) \sum_{\sigma \in S_k} \mathrm{sgn}(\sigma) \prod_{\ell=1}^k \partial_{x_{j_{\sigma(\ell)}}} f_{i_\ell}. \end{align*} (One recognises the inner sum as the determinant of the $k \times k$ minor $\bigl(\partial_{x_{j_\ell'}} f_{i_p}\bigr)_{p, \ell'}$ of the Jacobian $Jf$, but we will not need this identification.) [/guided] [/step] [step:Conclude smoothness of the coefficient functions] The coefficient $b_J: U \to \mathbb{R}$ is a finite sum of finite products of the following functions, each of which lies in $C^\infty(U)$: 1. The composition $a_I \circ f: U \to \mathbb{R}$. Since $a_I \in C^\infty(V)$ by the hypothesis $\omega \in \Omega^k(V)$ and $f: U \to V$ is smooth by hypothesis, the composition is smooth by the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) applied iteratively (which establishes that compositions of smooth maps are smooth). 2. The partial derivatives $\partial_{x_j} f_i: U \to \mathbb{R}$. Since $f_i \in C^\infty(U)$, every partial derivative of $f_i$ is again in $C^\infty(U)$ by the definition of smoothness. 3. The constants $\mathrm{sgn}(\sigma) \in \{-1, +1\}$. Since $C^\infty(U)$ is a commutative $\mathbb{R}$-algebra (closed under finite sums and products), $b_J \in C^\infty(U)$ for every $J \in \mathcal{I}_k^m$. Combined with the pointwise alternating multilinearity established in Step 2 and the coordinate representation derived in Step 4, this shows $f^*\omega \in \Omega^k(U)$, which completes the proof. [guided] We have reduced the question of smoothness of $f^*\omega$ to the question of smoothness of finitely many scalar functions $b_J: U \to \mathbb{R}$. Each $b_J$ is a finite sum of finite products of three types of functions: 1. **Compositions $a_I \circ f$.** By hypothesis $\omega \in \Omega^k(V)$, so each $a_I \in C^\infty(V)$. By hypothesis $f: U \to V$ is smooth, meaning each component $f_i \in C^\infty(U)$. The [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) establishes that the composition of smooth maps between Euclidean open sets is smooth (the chain rule formula expresses derivatives of the composition as polynomial combinations of derivatives of the factors, which propagate smoothness to all orders by induction). Hence $a_I \circ f \in C^\infty(U)$. 2. **Partial derivatives $\partial_{x_j} f_i$.** By definition, $f_i \in C^\infty(U)$ means all partial derivatives of $f_i$ of every order exist and are continuous; in particular, the first partial derivative $\partial_{x_j} f_i$ is itself in $C^\infty(U)$. 3. **Signs $\mathrm{sgn}(\sigma) \in \{-1, +1\}$.** Constants are smooth. Finally, $C^\infty(U)$ is closed under finite sums and finite products (since pointwise sums and products of smooth functions are smooth — Leibniz's rule shows products preserve smoothness to all orders). Therefore each $b_J$, being a finite $\mathbb{R}$-linear combination of finite products of these three types, lies in $C^\infty(U)$. **Putting it all together.** Step 2 showed that $(f^*\omega)_x \in \Lambda^k(\mathbb{R}^m)^*$ at every $x \in U$. Steps 3–4 produced the coordinate representation \begin{align*} f^*\omega = \sum_{J \in \mathcal{I}_k^m} b_J\, dx_{j_1} \wedge \cdots \wedge dx_{j_k} \end{align*} with coefficient functions $b_J \in C^\infty(U)$. By the definition of $\Omega^k(U)$, this is exactly what it means for $f^*\omega$ to be a smooth differential $k$-form on $U$. [/guided] [/step]