[proofplan]
We compare the two coordinate expressions by pulling the $\varphi$-coordinate expression through the transition map from $\psi$-coordinates to $\varphi$-coordinates. The transformation law for a top-degree form produces exactly the determinant of the transition Jacobian. Since the charts are positively oriented, this determinant is positive, so the determinant in the form transformation matches the absolute Jacobian factor in the Euclidean change-of-variables formula.
[/proofplan]
[step:Define the transition map between the two coordinate domains]
Let
\begin{align*}
W_\varphi &:= \varphi(U \cap V) \subseteq \mathbb{R}^n,\\
W_\psi &:= \psi(U \cap V) \subseteq \mathbb{R}^n.
\end{align*}
Define the transition map
\begin{align*}
F: W_\psi &\to W_\varphi\\
y &\mapsto \varphi(\psi^{-1}(y)).
\end{align*}
Since $\varphi$ and $\psi$ are smooth coordinate charts, $F$ is a smooth diffeomorphism with inverse
\begin{align*}
F^{-1}: W_\varphi &\to W_\psi\\
x &\mapsto \psi(\varphi^{-1}(x)).
\end{align*}
For each $y \in W_\psi$, let $JF_y \in \mathbb{R}^{n \times n}$ denote the Jacobian matrix of $F$ at $y$, that is, the matrix representation of the total derivative $DF_y: \mathbb{R}^n \to \mathbb{R}^n$ in the standard bases. Because both charts are positively oriented, the transition map is orientation-preserving, so
\begin{align*}
\det JF_y > 0
\end{align*}
for every $y \in W_\psi$.
[/step]
[step:Declare the coordinate coefficient functions of the top-degree form]
Since $\alpha \in \Omega_c^n(U \cap V)$, its pullbacks to the coordinate domains are compactly supported smooth top-degree forms. Define the coefficient functions $f: W_\varphi \to \mathbb{R}$ and $g: W_\psi \to \mathbb{R}$ by
\begin{align*}
(\varphi^{-1})^*\alpha &= f\, dx_1 \wedge \cdots \wedge dx_n,\\
(\psi^{-1})^*\alpha &= g\, dy_1 \wedge \cdots \wedge dy_n.
\end{align*}
Both $f$ and $g$ are smooth with compact support in their respective coordinate domains.
[/step]
[step:Compute the coefficient of the form in the second coordinate system]
Write the components of $F$ as smooth functions
\begin{align*}
F_i: W_\psi &\to \mathbb{R}, \qquad i \in \{1,\dots,n\},
\end{align*}
so that $F(y) = (F_1(y),\dots,F_n(y))$. Since
\begin{align*}
\psi^{-1} = \varphi^{-1} \circ F,
\end{align*}
we have
\begin{align*}
(\psi^{-1})^*\alpha
=
F^*((\varphi^{-1})^*\alpha).
\end{align*}
Using the $\varphi$-coordinate expression of $\alpha$,
\begin{align*}
F^*((\varphi^{-1})^*\alpha)
&=
F^*(f\, dx_1 \wedge \cdots \wedge dx_n)\\
&=
(f \circ F)\, dF_1 \wedge \cdots \wedge dF_n.
\end{align*}
By multilinearity and alternation of the wedge product,
\begin{align*}
dF_1 \wedge \cdots \wedge dF_n
=
\det JF_y\, dy_1 \wedge \cdots \wedge dy_n.
\end{align*}
Therefore
\begin{align*}
(\psi^{-1})^*\alpha
=
(f \circ F)\det JF_y\, dy_1 \wedge \cdots \wedge dy_n.
\end{align*}
By uniqueness of the coefficient of the basis form $dy_1 \wedge \cdots \wedge dy_n$, we obtain
\begin{align*}
g(y) = f(F(y))\det JF_y
\end{align*}
for every $y \in W_\psi$.
[guided]
The goal of this step is to identify the function $g$ appearing in the $\psi$-coordinate expression in terms of the function $f$ appearing in the $\varphi$-coordinate expression. The coordinate change from $\psi$-coordinates to $\varphi$-coordinates is the map
\begin{align*}
F: W_\psi &\to W_\varphi\\
y &\mapsto \varphi(\psi^{-1}(y)).
\end{align*}
The identity $\psi^{-1} = \varphi^{-1} \circ F$ gives
\begin{align*}
(\psi^{-1})^*\alpha
=
F^*((\varphi^{-1})^*\alpha).
\end{align*}
Now substitute the known $\varphi$-coordinate expression:
\begin{align*}
F^*((\varphi^{-1})^*\alpha)
&=
F^*(f\, dx_1 \wedge \cdots \wedge dx_n)\\
&=
(f \circ F)\, F^*(dx_1) \wedge \cdots \wedge F^*(dx_n).
\end{align*}
If $F_i: W_\psi \to \mathbb{R}$ denotes the $i$th component of $F$, then $F^*(dx_i) = dF_i$. Hence
\begin{align*}
F^*((\varphi^{-1})^*\alpha)
=
(f \circ F)\, dF_1 \wedge \cdots \wedge dF_n.
\end{align*}
The determinant appears because the wedge product records oriented volume distortion. Writing
\begin{align*}
dF_i = \sum_{j=1}^n \frac{\partial F_i}{\partial y_j}\, dy_j,
\end{align*}
and expanding the wedge product, all terms with repeated $dy_j$ vanish by alternation, and the surviving terms are exactly the determinant expansion:
\begin{align*}
dF_1 \wedge \cdots \wedge dF_n
=
\det JF_y\, dy_1 \wedge \cdots \wedge dy_n.
\end{align*}
Therefore
\begin{align*}
(\psi^{-1})^*\alpha
=
(f \circ F)\det JF_y\, dy_1 \wedge \cdots \wedge dy_n.
\end{align*}
Since the $\psi$-coordinate expression is also
\begin{align*}
(\psi^{-1})^*\alpha
=
g\, dy_1 \wedge \cdots \wedge dy_n,
\end{align*}
the coefficient functions must agree:
\begin{align*}
g(y) = f(F(y))\det JF_y
\end{align*}
for every $y \in W_\psi$.
[/guided]
[/step]
[step:Apply Euclidean change of variables with the positive Jacobian determinant]
The function $f: W_\varphi \to \mathbb{R}$ is smooth with compact support, because $\alpha$ has compact support in $U \cap V$. Thus $f$ is Lebesgue integrable on $W_\varphi$. Since $F: W_\psi \to W_\varphi$ is a smooth diffeomorphism, the Euclidean change-of-variables formula applies to $F$ and $f$ (citing a result not yet in the wiki: Euclidean Change of Variables Theorem). It gives
\begin{align*}
\int_{W_\varphi} f(x)\, d\mathcal{L}^n(x)
=
\int_{W_\psi} f(F(y))\, |\det JF_y|\, d\mathcal{L}^n(y).
\end{align*}
Because the charts are positively oriented, $\det JF_y > 0$ for every $y \in W_\psi$, so $|\det JF_y| = \det JF_y$. Using the coefficient identity from the previous step,
\begin{align*}
f(F(y))\det JF_y = g(y),
\end{align*}
we conclude that
\begin{align*}
\int_{W_\varphi} f(x)\, d\mathcal{L}^n(x)
=
\int_{W_\psi} g(y)\, d\mathcal{L}^n(y).
\end{align*}
This is exactly the equality of the local integrals computed in the two oriented coordinate charts.
[guided]
We now compare the two ordinary Lebesgue integrals. The relevant analytic input is the Euclidean change-of-variables formula for a smooth diffeomorphism (citing a result not yet in the wiki: Euclidean Change of Variables Theorem). Its hypotheses are satisfied here: $F: W_\psi \to W_\varphi$ is a smooth diffeomorphism between open subsets of $\mathbb{R}^n$, and $f: W_\varphi \to \mathbb{R}$ is smooth with compact support, hence Lebesgue integrable on $W_\varphi$.
Applying that formula gives
\begin{align*}
\int_{W_\varphi} f(x)\, d\mathcal{L}^n(x)
=
\int_{W_\psi} f(F(y))\, |\det JF_y|\, d\mathcal{L}^n(y).
\end{align*}
The absolute value is part of the Euclidean change-of-variables theorem because Lebesgue measure is unoriented. The form transformation, however, produced the signed determinant. The orientation hypothesis is precisely what makes these two factors agree: since $(U,\varphi)$ and $(V,\psi)$ are positively oriented charts, the transition map $F = \varphi \circ \psi^{-1}$ satisfies
\begin{align*}
\det JF_y > 0
\end{align*}
for every $y \in W_\psi$. Therefore
\begin{align*}
|\det JF_y| = \det JF_y.
\end{align*}
From the previous step we already proved the coefficient identity
\begin{align*}
g(y) = f(F(y))\det JF_y.
\end{align*}
Substituting this identity into the change-of-variables formula yields
\begin{align*}
\int_{W_\varphi} f(x)\, d\mathcal{L}^n(x)
=
\int_{W_\psi} g(y)\, d\mathcal{L}^n(y).
\end{align*}
Thus the value of the local integral of the compactly supported top-degree form $\alpha$ is independent of whether it is computed in the $\varphi$-coordinates or in the $\psi$-coordinates.
[/guided]
[/step]
