[proofplan] We prove the vector-field transformation by testing both sides on an arbitrary smooth function and applying the Euclidean chain rule to the transition map $\varphi \circ \psi^{-1}$. The coframe transformation is then proved by evaluating both sides on the coordinate basis vectors $\partial_{x_k}$ and using the defining duality relation $dx_i(\partial_{x_k})=\delta_{ik}$. The two formulas are compatible because the Jacobian matrices of the two transition maps are inverse matrices. [/proofplan] [step:Express the coordinate vector fields as derivations on smooth functions] Let $p \in U$ and let $f:U \to \mathbb{R}$ be a smooth function. By definition of the coordinate vector fields, \begin{align*} (\partial_{y_j})_p(f) &= \partial_{r_j}(f \circ \psi^{-1})(\psi(p)),\\ (\partial_{x_i})_p(f) &= \partial_{s_i}(f \circ \varphi^{-1})(\varphi(p)). \end{align*} Define the transition map \begin{align*} \chi:\psi(U) &\to \varphi(U)\\ r &\mapsto \varphi(\psi^{-1}(r)). \end{align*} Then $\chi_i=x_i\circ \psi^{-1}$ for each component $\chi_i:\psi(U)\to\mathbb{R}$, and \begin{align*} f \circ \psi^{-1} &= (f \circ \varphi^{-1}) \circ \chi. \end{align*} [/step] [step:Apply the Euclidean chain rule to obtain the frame transformation] Let \begin{align*} g:\varphi(U) &\to \mathbb{R}\\ s &\mapsto f(\varphi^{-1}(s)). \end{align*} Then $g=f\circ\varphi^{-1}$ and $f\circ\psi^{-1}=g\circ\chi$. Since $g$ and $\chi$ are smooth maps between open subsets of Euclidean space, the ordinary Euclidean chain rule applies (citing a result not yet in the wiki: Chain Rule for Smooth Maps Between Euclidean Open Sets). At $r=\psi(p)$, \begin{align*} (\partial_{y_j})_p(f) &= \partial_{r_j}(g\circ\chi)(r)\\ &= \sum_{i=1}^n \partial_{s_i}g(\chi(r))\,\partial_{r_j}\chi_i(r)\\ &= \sum_{i=1}^n \partial_{s_i}(f\circ\varphi^{-1})(\varphi(p))\,\partial_{r_j}(x_i\circ\psi^{-1})(\psi(p))\\ &= \sum_{i=1}^n \frac{\partial x_i}{\partial y_j}(p)\,(\partial_{x_i})_p(f). \end{align*} Because this identity holds for every smooth function $f:U\to\mathbb{R}$, the tangent vectors agree: \begin{align*} (\partial_{y_j})_p &= \sum_{i=1}^n \frac{\partial x_i}{\partial y_j}(p)\,(\partial_{x_i})_p. \end{align*} Since $p \in U$ was arbitrary, this proves \begin{align*} \partial_{y_j} &= \sum_{i=1}^n \frac{\partial x_i}{\partial y_j}\,\partial_{x_i} \end{align*} as vector fields on $U$. [guided] We want to compare two tangent vectors, so we compare their actions as derivations on arbitrary smooth functions. Let $f:U\to\mathbb{R}$ be smooth and define \begin{align*} g:\varphi(U) &\to \mathbb{R}\\ s &\mapsto f(\varphi^{-1}(s)). \end{align*} Thus $g=f\circ\varphi^{-1}$ is the coordinate expression of $f$ in the $x$-coordinates. The transition map from $y$-coordinates to $x$-coordinates is \begin{align*} \chi:\psi(U) &\to \varphi(U)\\ r &\mapsto \varphi(\psi^{-1}(r)). \end{align*} Its $i$-th component is \begin{align*} \chi_i(r) &= x_i(\psi^{-1}(r)), \end{align*} so $\chi_i=x_i\circ\psi^{-1}$. The coordinate expression of $f$ in $y$-coordinates is therefore \begin{align*} f\circ\psi^{-1} &= (f\circ\varphi^{-1})\circ(\varphi\circ\psi^{-1})\\ &= g\circ\chi. \end{align*} Now apply the ordinary Euclidean chain rule to the smooth maps $g:\varphi(U)\to\mathbb{R}$ and $\chi:\psi(U)\to\varphi(U)$ (citing a result not yet in the wiki: Chain Rule for Smooth Maps Between Euclidean Open Sets). At $r=\psi(p)$, the derivative in the $r_j$ direction is \begin{align*} (\partial_{y_j})_p(f) &= \partial_{r_j}(f\circ\psi^{-1})(r)\\ &= \partial_{r_j}(g\circ\chi)(r)\\ &= \sum_{i=1}^n \partial_{s_i}g(\chi(r))\,\partial_{r_j}\chi_i(r). \end{align*} Substituting back the meanings of $g$, $\chi$, and $\chi_i$ gives \begin{align*} (\partial_{y_j})_p(f) &= \sum_{i=1}^n \partial_{s_i}(f\circ\varphi^{-1})(\varphi(p))\, \partial_{r_j}(x_i\circ\psi^{-1})(\psi(p))\\ &= \sum_{i=1}^n \frac{\partial x_i}{\partial y_j}(p)\, (\partial_{x_i})_p(f). \end{align*} This equality holds for every smooth function $f:U\to\mathbb{R}$. Tangent vectors are equal exactly when they act equally on all smooth functions, so \begin{align*} (\partial_{y_j})_p &= \sum_{i=1}^n \frac{\partial x_i}{\partial y_j}(p)\,(\partial_{x_i})_p. \end{align*} Because $p$ was arbitrary, the equality holds as an identity of vector fields on $U$. [/guided] [/step] [step:Evaluate both sides on the $x$-coordinate frame to obtain the coframe transformation] Fix $p \in U$ and $1 \leq k \leq n$. The one-form $(dy_j)_p:T_pM\to\mathbb{R}$ acts on $(\partial_{x_k})_p$ by differentiating the coordinate function $y_j:U\to\mathbb{R}$: \begin{align*} (dy_j)_p((\partial_{x_k})_p) &= (\partial_{x_k})_p(y_j)\\ &= \partial_{s_k}(y_j\circ\varphi^{-1})(\varphi(p))\\ &= \frac{\partial y_j}{\partial x_k}(p). \end{align*} On the other hand, using the duality relation \begin{align*} (dx_i)_p((\partial_{x_k})_p)&=\delta_{ik}, \end{align*} we get \begin{align*} \left(\sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p\right)((\partial_{x_k})_p) &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p((\partial_{x_k})_p)\\ &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,\delta_{ik}\\ &= \frac{\partial y_j}{\partial x_k}(p). \end{align*} Thus $(dy_j)_p$ and $\sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)(dx_i)_p$ agree on every vector in the basis $((\partial_{x_1})_p,\dots,(\partial_{x_n})_p)$ of $T_pM$. Hence \begin{align*} (dy_j)_p &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p. \end{align*} Since $p \in U$ was arbitrary, this proves \begin{align*} dy_j &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}\,dx_i \end{align*} as one-forms on $U$. [guided] To prove equality of one-forms at a point $p$, it is enough to evaluate them on a basis of $T_pM$. We use the basis supplied by the $x$-coordinate chart: \begin{align*} ((\partial_{x_1})_p,\dots,(\partial_{x_n})_p). \end{align*} Fix $1\leq k\leq n$. By the definition of the differential of a smooth function and the definition of the coordinate vector field $(\partial_{x_k})_p$, \begin{align*} (dy_j)_p((\partial_{x_k})_p) &= (\partial_{x_k})_p(y_j)\\ &= \partial_{s_k}(y_j\circ\varphi^{-1})(\varphi(p))\\ &= \frac{\partial y_j}{\partial x_k}(p). \end{align*} Now evaluate the proposed right-hand side on the same basis vector. The one-forms $(dx_1)_p,\dots,(dx_n)_p$ are dual to the basis vectors $(\partial_{x_1})_p,\dots,(\partial_{x_n})_p$, meaning \begin{align*} (dx_i)_p((\partial_{x_k})_p) &= \delta_{ik}. \end{align*} Therefore \begin{align*} \left(\sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p\right)((\partial_{x_k})_p) &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p((\partial_{x_k})_p)\\ &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,\delta_{ik}\\ &= \frac{\partial y_j}{\partial x_k}(p). \end{align*} Both one-forms have the same value on each basis vector $(\partial_{x_k})_p$. Since a linear functional on $T_pM$ is determined by its values on a basis, the two one-forms are equal at $p$: \begin{align*} (dy_j)_p &= \sum_{i=1}^n \frac{\partial y_j}{\partial x_i}(p)\,(dx_i)_p. \end{align*} Because $p$ was arbitrary, this is an identity of one-forms on all of $U$. [/guided] [/step] [step:Identify the inverse-dual relation between the two transformation laws] At each $p \in U$, define matrices $A(p),B(p)\in\mathbb{R}^{n\times n}$ by \begin{align*} A(p)_{ij} &= \frac{\partial x_i}{\partial y_j}(p),& B(p)_{ji} &= \frac{\partial y_j}{\partial x_i}(p). \end{align*} The maps $\chi=\varphi\circ\psi^{-1}:\psi(U)\to\varphi(U)$ and $\chi^{-1}=\psi\circ\varphi^{-1}:\varphi(U)\to\psi(U)$ are inverse smooth maps. Applying the Euclidean chain rule to $\chi\circ\chi^{-1}=\operatorname{id}_{\varphi(U)}$ and $\chi^{-1}\circ\chi=\operatorname{id}_{\psi(U)}$ gives \begin{align*} A(p)B(p)&=I_n, & B(p)A(p)&=I_n. \end{align*} Thus the coordinate frame transforms by the Jacobian of the change from $y$-coordinates to $x$-coordinates, while the coframe transforms by the inverse transpose rule encoded by the [dual basis](/theorems/414) calculation above. This completes the proof of both displayed transformation laws. [/step]