[proofplan] Both identities are equalities of smooth differential forms on $M$, hence may be verified pointwise and, in particular, on the domain of any smooth chart. The wedge product identity is a direct consequence of the pointwise definitions: since $dF_p : T_pM \to T_{F(p)}N$ is linear, pullback commutes with every multilinear and alternating operation, of which the wedge product is one. The [exterior derivative](/theorems/1525) identity is verified by reducing to two pieces: (i) for a smooth function $f \in C^\infty(N)$ the identity $d(F^*f) = F^*(df)$ is exactly the chain rule, and (ii) for a general $p$-form, write it locally as $\sum_I a_I\, dy_{i_1} \wedge \cdots \wedge dy_{i_p}$ in a chart on $N$ and propagate the function-level identity through the Leibniz rule together with $d \circ d = 0$, using the wedge identity from part one. [/proofplan]

[step:Reduce both identities to a pointwise verification on chart domains]The two identities are equalities between smooth forms on $M$. A smooth form on $M$ is determined by its values at each point $p \in M$, and each point lies in the domain $U$ of a smooth chart $(U, \varphi)$ with coordinates $(x_1, \dots, x_m)$. Since $F$ is continuous, every $p \in M$ admits a chart $(U, \varphi)$ around $p$ and a chart $(V, \psi)$ around $F(p)$ with coordinates $(y_1, \dots, y_n)$ such that $F(U) \subseteq V$; this is achieved by shrinking the initial chart $(U_0, \varphi_0)$ around $p$ to $U := U_0 \cap F^{-1}(V)$, which is open and contains $p$. Fixing such matched charts $(U, \varphi)$ on $M$ and $(V, \psi)$ on $N$, we may write \begin{align*} F &= (F_1, \dots, F_n) \qquad \text{with } F_j := y_j \circ F \in C^\infty(U), \end{align*} where each coordinate function $y_j \in C^\infty(V)$ is regarded as a smooth function via the chart $\psi$. The pullbacks $F^* dy_j \in \Omega^1(U)$ satisfy, for $p \in U$ and $v \in T_pM$, \begin{align*} (F^* dy_j)_p(v) \;=\; (dy_j)_{F(p)}\bigl(dF_p(v)\bigr) \;=\; dF_p(v)\,[y_j] \;=\; v[y_j \circ F] \;=\; v[F_j] \;=\; (dF_j)_p(v), \end{align*} so $F^* dy_j = dF_j$ on $U$.[/step]

[guided]Why is it enough to work in charts? Both sides of each identity are smooth $k$-forms on $M$; two such forms agree if and only if they agree at every point, and every point lies in the domain of some smooth chart. So once we prove the identity holds on every chart $U$ of $M$, the identity holds globally. We also need the freedom to choose the chart on $N$ so that $F(U) \subseteq V$. This is achieved by *shrinking* $U$: start with any chart $(U_0, \varphi_0)$ around $p$ and any chart $(V, \psi)$ around $F(p)$, then set $U := U_0 \cap F^{-1}(V)$. This is open by continuity of $F$ and contains $p$ by construction; restricting $\varphi_0$ to $U$ gives the required chart. On such matched charts, we have access to local coordinates $(x_1, \dots, x_m)$ on $U$ and $(y_1, \dots, y_n)$ on $V$. The smooth map $F : U \to V$ is determined by its component functions \begin{align*} F_j \;:=\; y_j \circ F \in C^\infty(U), \qquad j = 1, \dots, n. \end{align*} The identity $F^* dy_j = dF_j$ is fundamental and will be the basic building block: applying the definition of pullback to the $1$-form $dy_j$ and any tangent vector $v \in T_pM$, \begin{align*} (F^* dy_j)_p(v) \;=\; (dy_j)_{F(p)}\bigl(dF_p(v)\bigr). \end{align*} By definition of the differential of a smooth function, $(dy_j)_{F(p)}$ acts on a tangent vector $w \in T_{F(p)}N$ by $w[y_j]$. By definition of the pushforward, $dF_p(v)[y_j] = v[y_j \circ F] = v[F_j] = (dF_j)_p(v)$. Hence $F^* dy_j = dF_j$. This identity is the bridge from "pullback" to "[exterior derivative](/theorems/1525) of a coordinate function" that we will exploit in Step 4.[/guided]

[step:Establish the wedge-product identity by unwinding the pointwise definitions]Fix $p \in M$ and tangent vectors $v_1, \dots, v_{p+q} \in T_pM$. Let $S_{p+q}$ denote the symmetric group of all bijections $\sigma : \{1, \dots, p+q\} \to \{1, \dots, p+q\}$, and let $\mathrm{sgn}: S_{p+q} \to \{-1, 1\}$ denote the [sign homomorphism](/theorems/778), with value $1$ on even permutations and $-1$ on odd permutations. We use the convention \begin{align*} (\alpha \wedge \beta)(w_1, \dots, w_{p+q}) \;=\; \frac{1}{p!\, q!} \sum_{\sigma \in S_{p+q}} \mathrm{sgn}(\sigma)\, \alpha(w_{\sigma(1)}, \dots, w_{\sigma(p)})\, \beta(w_{\sigma(p+1)}, \dots, w_{\sigma(p+q)}) \end{align*} for the wedge product of an alternating $p$-tensor $\alpha$ and an alternating $q$-tensor $\beta$ on a [vector space](/page/Vector%20Space). If $p = 0$ or $q = 0$, the same convention is read with $0! = 1$ and the unique empty argument, so wedge product with a $0$-tensor is ordinary multiplication by that function. Applying the definition of pullback to $\alpha \wedge \beta \in \Omega^{p+q}(N)$, \begin{align*} \bigl(F^*(\alpha \wedge \beta)\bigr)_p(v_1, \dots, v_{p+q}) &= (\alpha \wedge \beta)_{F(p)}\bigl(dF_p(v_1), \dots, dF_p(v_{p+q})\bigr) \\ &= \frac{1}{p!\, q!} \sum_{\sigma \in S_{p+q}} \mathrm{sgn}(\sigma)\, \alpha_{F(p)}\bigl(dF_p(v_{\sigma(1)}), \dots, dF_p(v_{\sigma(p)})\bigr) \\ &\qquad\qquad\qquad\qquad \times \beta_{F(p)}\bigl(dF_p(v_{\sigma(p+1)}), \dots, dF_p(v_{\sigma(p+q)})\bigr). \end{align*} Each factor in the sum is, by the definition of pullback applied to $\alpha$ and to $\beta$ separately, equal to $(F^*\alpha)_p(v_{\sigma(1)}, \dots, v_{\sigma(p)})$ and $(F^*\beta)_p(v_{\sigma(p+1)}, \dots, v_{\sigma(p+q)})$ respectively. Therefore \begin{align*} \bigl(F^*(\alpha \wedge \beta)\bigr)_p(v_1, \dots, v_{p+q}) \;=\; \bigl((F^*\alpha) \wedge (F^*\beta)\bigr)_p(v_1, \dots, v_{p+q}). \end{align*} Since $p \in M$ and the vectors $v_1, \dots, v_{p+q}$ were arbitrary, the identity $F^*(\alpha \wedge \beta) = F^*\alpha \wedge F^*\beta$ holds in $\Omega^{p+q}(M)$.[/step]

[guided]The wedge product identity has no analytic content — it is purely a pointwise algebraic statement, and the proof amounts to unwinding two definitions in the correct order. We fix a point $p \in M$ and a list of $p+q$ tangent vectors at $p$, and evaluate both sides. The left-hand side $F^*(\alpha \wedge \beta)$ is, by definition of pullback, \begin{align*} \bigl(F^*(\alpha \wedge \beta)\bigr)_p(v_1, \dots, v_{p+q}) \;=\; (\alpha \wedge \beta)_{F(p)}\bigl(dF_p(v_1), \dots, dF_p(v_{p+q})\bigr). \end{align*} Let $S_{p+q}$ denote the symmetric group of all bijections $\sigma : \{1, \dots, p+q\} \to \{1, \dots, p+q\}$, and let $\mathrm{sgn}: S_{p+q} \to \{-1, 1\}$ denote the [sign homomorphism](/theorems/778). If $p = 0$ or $q = 0$, the wedge convention uses $0! = 1$ and the unique empty argument, giving ordinary multiplication by the corresponding $0$-form. We now apply the definition of the wedge product *at the point $F(p)$*, evaluated on the pushed-forward vectors $dF_p(v_i)$: \begin{align*} &(\alpha \wedge \beta)_{F(p)}\bigl(dF_p(v_1), \dots, dF_p(v_{p+q})\bigr) \\ &\qquad = \frac{1}{p!\, q!} \sum_{\sigma \in S_{p+q}} \mathrm{sgn}(\sigma)\, \alpha_{F(p)}\bigl(dF_p(v_{\sigma(1)}), \dots, dF_p(v_{\sigma(p)})\bigr) \\ &\qquad\qquad\qquad\qquad\qquad \times \beta_{F(p)}\bigl(dF_p(v_{\sigma(p+1)}), \dots, dF_p(v_{\sigma(p+q)})\bigr). \end{align*} The crucial observation is that within each summand, $\alpha_{F(p)}$ is evaluated on pushforwards of $v_{\sigma(1)}, \dots, v_{\sigma(p)}$, which is *precisely* the definition of $(F^*\alpha)_p$ applied to $v_{\sigma(1)}, \dots, v_{\sigma(p)}$ — and similarly for $\beta$. Substituting, \begin{align*} &= \frac{1}{p!\, q!} \sum_{\sigma \in S_{p+q}} \mathrm{sgn}(\sigma)\, (F^*\alpha)_p(v_{\sigma(1)}, \dots, v_{\sigma(p)})\, (F^*\beta)_p(v_{\sigma(p+1)}, \dots, v_{\sigma(p+q)}) \\ &= \bigl((F^*\alpha) \wedge (F^*\beta)\bigr)_p(v_1, \dots, v_{p+q}). \end{align*} The reason this works is that the wedge product is a universal algebraic construction on each fibre $\Lambda^\bullet T_{F(p)}^* N$, and the pullback acts fibrewise by precomposition with the [linear map](/page/Linear%20Map) $dF_p$, which commutes with every multilinear operation. Linearity of $dF_p$ is the only ingredient — no smoothness or regularity of $\alpha, \beta$ enters beyond what is needed to make $\alpha_{F(p)}$ and $\beta_{F(p)}$ well-defined alternating tensors.[/guided]

[step:Verify $d(F^*f) = F^*(df)$ for smooth functions via the chain rule]Let $f \in C^\infty(N)$, so $F^*f = f \circ F \in C^\infty(M)$. Fix matched charts $(U, \varphi)$ on $M$ and $(V, \psi)$ on $N$ with $F(U) \subseteq V$, as constructed in Step 1, with coordinates $(x_1, \dots, x_m)$ and $(y_1, \dots, y_n)$ and component functions $F_j = y_j \circ F$. In the chart $(V, \psi)$, \begin{align*} df \;=\; \sum_{j=1}^n \frac{\partial f}{\partial y_j}\, dy_j \qquad \text{on } V, \end{align*} and pulling back using the wedge identity from Step 2 in the case of a $0$-form multiplying a $1$-form, \begin{align*} F^*((\partial_{y_j} f) \, dy_j) = F^*(\partial_{y_j} f) \cdot F^* dy_j, \end{align*} together with the identity $F^* dy_j = dF_j$ from Step 1, we obtain \begin{align*} F^*(df) \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \, dF_j \qquad \text{on } U. \end{align*} On the other hand, in the chart $(U, \varphi)$, \begin{align*} d(F^*f) \;=\; d(f \circ F) \;=\; \sum_{i=1}^m \partial_{x_i}(f \circ F)\, dx_i. \end{align*} By the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) applied to the chart representative $\psi \circ F \circ \varphi^{-1}$ of $F$ (which is a smooth map between open subsets of $\mathbb{R}^m$ and $\mathbb{R}^n$) and to the chart representative of $f$, \begin{align*} \partial_{x_i}(f \circ F) \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot \partial_{x_i} F_j, \end{align*} and thus \begin{align*} d(F^*f) \;=\; \sum_{i=1}^m \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot \partial_{x_i} F_j \, dx_i \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \, dF_j, \end{align*} where in the last equality we used $dF_j = \sum_{i=1}^m \partial_{x_i} F_j\, dx_i$ on $U$. Comparing with the expression for $F^*(df)$ above gives $d(F^*f) = F^*(df)$ on $U$. As $U$ was an arbitrary chart domain on $M$, the identity holds on all of $M$.[/step]

[guided]For $0$-forms, the pullback identity $d(F^*f) = F^*(df)$ is precisely the chain rule, dressed in the language of differential forms. Let us see exactly how. Pick matched charts on $M$ and $N$ as in Step 1. In the chart $(V, \psi)$, the canonical local expression of $df$ as a $1$-form is \begin{align*} df \;=\; \sum_{j=1}^n \frac{\partial f}{\partial y_j}\, dy_j. \end{align*} Pulling back this expression term-by-term: by the wedge identity from Step 2 (which for $0$-form-times-$1$-form is simply the assertion that $F^*(g\omega) = (F^*g)(F^*\omega)$ for a smooth function $g$ and a $1$-form $\omega$), \begin{align*} F^*(df) \;=\; \sum_{j=1}^n F^*\!\left(\frac{\partial f}{\partial y_j}\right) \cdot F^*dy_j \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot dF_j, \end{align*} where we used $F^* g = g \circ F$ for $0$-forms and $F^* dy_j = dF_j$ from Step 1. Now compute the other side. The composition $f \circ F : U \to \mathbb{R}$ is smooth, so its differential is \begin{align*} d(F^*f) \;=\; d(f \circ F) \;=\; \sum_{i=1}^m \partial_{x_i}(f \circ F)\, dx_i. \end{align*} To match the two expressions, we must evaluate $\partial_{x_i}(f \circ F)$. We invoke the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323). The hypotheses are that we have smooth maps between open subsets of Euclidean space; this is satisfied because $\psi \circ F \circ \varphi^{-1} : \varphi(U) \to \psi(V)$ and $f \circ \psi^{-1} : \psi(V) \to \mathbb{R}$ are smooth by definition of smoothness on manifolds (charts make $F$ and $f$ Euclidean-smooth). The chain rule then gives, with $F_j = y_j \circ F$, \begin{align*} \partial_{x_i}(f \circ F) \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot \partial_{x_i} F_j. \end{align*} Substituting back, \begin{align*} d(F^*f) \;=\; \sum_{i=1}^m \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot \partial_{x_i} F_j \, dx_i \;=\; \sum_{j=1}^n \bigl((\partial_{y_j} f) \circ F\bigr) \cdot \sum_{i=1}^m \partial_{x_i} F_j\, dx_i, \end{align*} where we have exchanged the order of summation (a finite sum, so this is unconditional). The inner sum is exactly the local expression of $dF_j \in \Omega^1(U)$: \begin{align*} dF_j \;=\; \sum_{i=1}^m \partial_{x_i} F_j\, dx_i. \end{align*} Hence $d(F^*f) = \sum_j ((\partial_{y_j} f) \circ F)\, dF_j$, which is precisely the expression we found for $F^*(df)$. The identity holds on $U$; since arbitrary points of $M$ lie in such chart domains, it holds globally.[/guided]

[step:Extend the exterior derivative identity to general $p$-forms via local expansion]Let $\alpha \in \Omega^p(N)$ with $p \ge 1$. We verify $d(F^*\alpha) = F^*(d\alpha)$ on the domain $U$ of an arbitrary chart $(U, \varphi)$ of $M$ matched to a chart $(V, \psi)$ of $N$ with $F(U) \subseteq V$, as in Step 1. In the chart $(V, \psi)$ with coordinates $(y_1, \dots, y_n)$, the form $\alpha$ admits the canonical local expression \begin{align*} \alpha \;=\; \sum_{I} a_I \, dy_{i_1} \wedge \cdots \wedge dy_{i_p} \qquad \text{on } V, \end{align*} where the sum runs over strictly increasing multi-indices $I = (i_1 < i_2 < \cdots < i_p)$ with $1 \le i_k \le n$, and $a_I \in C^\infty(V)$. Define for each such $I$ the smooth form $dy_I := dy_{i_1} \wedge \cdots \wedge dy_{i_p}$. By the iterated wedge identity from Step 2 (applied $p-1$ times) together with Step 1, \begin{align*} F^*(dy_I) \;=\; F^*(dy_{i_1}) \wedge \cdots \wedge F^*(dy_{i_p}) \;=\; dF_{i_1} \wedge \cdots \wedge dF_{i_p}, \end{align*} and another application of Step 2 yields \begin{align*} F^*\alpha \;=\; \sum_I (a_I \circ F)\, dF_{i_1} \wedge \cdots \wedge dF_{i_p} \qquad \text{on } U. \tag{$\star$} \end{align*} Next we apply the [exterior derivative](/theorems/1525) to $(\star)$. We use the standard properties of $d$ on $\Omega^\bullet(U)$: 1. **Linearity:** $d$ is $\mathbb{R}$-linear. 2. **Leibniz rule:** $d(\omega \wedge \eta) = d\omega \wedge \eta + (-1)^{\deg \omega}\, \omega \wedge d\eta$. 3. **$d \circ d = 0$:** in particular, $d(dF_{i_k}) = 0$ for each $k$. Applying $d$ to each summand of $(\star)$ and using the Leibniz rule $p$ times, \begin{align*} d\bigl((a_I \circ F)\, dF_{i_1} \wedge \cdots \wedge dF_{i_p}\bigr) \;=\; d(a_I \circ F) \wedge dF_{i_1} \wedge \cdots \wedge dF_{i_p}, \end{align*} since every Leibniz term containing some $d(dF_{i_k})$ vanishes by $d \circ d = 0$. Step 3 applied to the function $a_I$ gives $d(a_I \circ F) = d(F^* a_I) = F^*(da_I)$. Hence, by linearity of $d$, \begin{align*} d(F^*\alpha) \;=\; \sum_I F^*(da_I) \wedge dF_{i_1} \wedge \cdots \wedge dF_{i_p} \;=\; \sum_I F^*(da_I) \wedge F^*(dy_{i_1}) \wedge \cdots \wedge F^*(dy_{i_p}), \end{align*} using $F^* dy_{i_k} = dF_{i_k}$ once more. On the other hand, applying $d$ to the local expression of $\alpha$ on $V$ and using the same three properties of $d$ on $\Omega^\bullet(V)$, \begin{align*} d\alpha \;=\; \sum_I da_I \wedge dy_{i_1} \wedge \cdots \wedge dy_{i_p} \qquad \text{on } V, \end{align*} and applying $F^*$ via the iterated wedge identity from Step 2, \begin{align*} F^*(d\alpha) \;=\; \sum_I F^*(da_I) \wedge F^*(dy_{i_1}) \wedge \cdots \wedge F^*(dy_{i_p}) \qquad \text{on } U. \end{align*} The right-hand sides of the expressions for $d(F^*\alpha)$ and $F^*(d\alpha)$ on $U$ coincide, so $d(F^*\alpha) = F^*(d\alpha)$ on $U$. Since chart domains cover $M$ and $U$ was arbitrary, the identity holds on all of $M$. Combined with Step 2, this completes the proof of both identities.[/step]

[guided]We now extend the function-case identity from Step 3 to arbitrary $p$-forms. The plan is to use the local coordinate expression of $\alpha$ — which expresses $\alpha$ as a finite combination of products of $0$-forms and exact $1$-forms $dy_j$ — and then propagate the identity through the Leibniz rule and the wedge identity, using $d^2 = 0$ to kill the awkward terms. **Local expansion of $\alpha$.** In the chart $(V, \psi)$ on $N$ with coordinates $(y_1, \dots, y_n)$, every $p$-form on $V$ has a unique expression \begin{align*} \alpha \;=\; \sum_I a_I\, dy_I, \qquad dy_I := dy_{i_1} \wedge \cdots \wedge dy_{i_p}, \end{align*} indexed by strictly increasing multi-indices $I = (i_1 < \cdots < i_p)$. The coefficients $a_I$ are smooth on $V$. **Pull back the local expansion.** By the wedge identity from Step 2 (used $p - 1$ times), \begin{align*} F^*(dy_I) \;=\; F^*(dy_{i_1}) \wedge \cdots \wedge F^*(dy_{i_p}) \;=\; dF_{i_1} \wedge \cdots \wedge dF_{i_p}, \end{align*} where the second equality is $F^* dy_j = dF_j$ from Step 1. Applying Step 2 once more (now to the product of the $0$-form $a_I$ with the $p$-form $dy_I$), \begin{align*} F^*\alpha \;=\; \sum_I (a_I \circ F)\, dF_{i_1} \wedge \cdots \wedge dF_{i_p}. \end{align*} This local formula for $F^*\alpha$ is the workhorse: notice that it is built out of pulled-back functions $a_I \circ F$ and *exact* $1$-forms $dF_{i_k}$. **Differentiate $F^*\alpha$.** Apply $d$ to each summand, using the Leibniz rule \begin{align*} d(\omega \wedge \eta) \;=\; d\omega \wedge \eta \,+\, (-1)^{\deg \omega} \omega \wedge d\eta \end{align*} iteratively across the $p+1$ factors $(a_I \circ F), dF_{i_1}, \dots, dF_{i_p}$. Every Leibniz term except the one where $d$ falls on $(a_I \circ F)$ contains a factor of $d(dF_{i_k}) = 0$ — this is where $d \circ d = 0$ is used. So \begin{align*} d\bigl((a_I \circ F)\, dF_{i_1} \wedge \cdots \wedge dF_{i_p}\bigr) \;=\; d(a_I \circ F) \wedge dF_{i_1} \wedge \cdots \wedge dF_{i_p}. \end{align*} By Step 3 applied to the function $a_I$, $d(a_I \circ F) = d(F^* a_I) = F^*(da_I)$. Hence \begin{align*} d(F^*\alpha) \;=\; \sum_I F^*(da_I) \wedge dF_{i_1} \wedge \cdots \wedge dF_{i_p}. \end{align*} **Compute $F^*(d\alpha)$ on the other side.** On $V$, the same Leibniz-and-$d^2 = 0$ argument applied to $\alpha = \sum_I a_I\, dy_I$ gives \begin{align*} d\alpha \;=\; \sum_I da_I \wedge dy_{i_1} \wedge \cdots \wedge dy_{i_p}. \end{align*} The forms $dy_{i_k}$ are exact (they are $d$ of coordinate functions), so $d(dy_{i_k}) = 0$, exactly as for $dF_{i_k}$ above. Pulling back via the wedge identity from Step 2, \begin{align*} F^*(d\alpha) \;=\; \sum_I F^*(da_I) \wedge F^*(dy_{i_1}) \wedge \cdots \wedge F^*(dy_{i_p}) \;=\; \sum_I F^*(da_I) \wedge dF_{i_1} \wedge \cdots \wedge dF_{i_p}. \end{align*} **Compare.** The expressions for $d(F^*\alpha)$ and $F^*(d\alpha)$ on $U$ are identical term by term. Hence the two smooth $(p+1)$-forms agree on $U$. Since the chart $(U, \varphi)$ was arbitrary and such charts cover $M$, the identity $d(F^*\alpha) = F^*(d\alpha)$ holds on all of $M$. **Why this works.** Two structural facts conspire. First, every form on $N$ is locally a finite combination of products of $0$-forms and exact $1$-forms $dy_j$. Second, both $d$ and $F^*$ are determined by their actions on $0$-forms (chain rule = Step 3) together with the Leibniz rule, the wedge identity, and $d^2 = 0$. So once the identity is checked on $0$-forms — which is the chain rule — it propagates to all forms by purely algebraic manipulation.[/guided]