[proofplan] The proof is a direct comparison of the two frame-change formulas for local frames. At a point $x\in f^{-1}(V_i\cap V_j)$, both pulled-back frames live in the fibre of the pullback vector bundle, namely $(f^*E)_x=\{x\}\times E_{f(x)}$, so their relation is exactly the original relation between the frames of $E$ at the point $f(x)\in V_i\cap V_j$. Substituting $y=f(x)$ into the transition function formula for $E$ gives the matrix entries of the pullback transition function, and smoothness follows because the pullback transition function is the composition $g_{ij}\circ f$ on the relevant [open set](/page/Open%20Set). [/proofplan]

[step:Write the pulled-back frame relation in the fibre over $x$]Fix indices $i,j\in I$. Let $x\in f^{-1}(V_i\cap V_j)$, so $f(x)\in V_i\cap V_j$. For each $a\in\{1,\dots,r\}$, the definition of the pulled-back local frame gives \begin{align*} \tilde e_{j,a}(x)=(x,e_{j,a}(f(x))). \end{align*} Using the defining transition function formula for the original frames at the point $f(x)$ gives the following equality in $E_{f(x)}$: \begin{align*} e_{j,a}(f(x))=\sum_{b=1}^r e_{i,b}(f(x))\,(g_{ij}(f(x)))_{ba}. \end{align*} Therefore, using the [vector space](/page/Vector%20Space) structure on the fibre $(f^*E)_x=\{x\}\times E_{f(x)}$, we first have \begin{align*} \tilde e_{j,a}(x)=(x,e_{j,a}(f(x))). \end{align*} Substituting the transition formula for $e_{j,a}(f(x))$ gives that $\tilde e_{j,a}(x)$ is the pair whose first component is $x$ and whose second component is \begin{align*} \sum_{b=1}^r e_{i,b}(f(x))\,(g_{ij}(f(x)))_{ba}. \end{align*} Linearity of the fibre operations in the second component gives \begin{align*} \tilde e_{j,a}(x)=\sum_{b=1}^r (x,e_{i,b}(f(x)))\,(g_{ij}(f(x)))_{ba}. \end{align*} By the definition of the pulled-back frame vectors, this is \begin{align*} \tilde e_{j,a}(x)=\sum_{b=1}^r \tilde e_{i,b}(x)\,(g_{ij}(f(x)))_{ba}. \end{align*}[/step]

[guided]Fix $i,j\in I$ and choose a point $x\in f^{-1}(V_i\cap V_j)$. The condition $x\in f^{-1}(V_i\cap V_j)$ means exactly that $f(x)\in V_i\cap V_j$, so the original transition formula for the frames of $E$ may be evaluated at the point $f(x)$. For each frame index $a\in\{1,\dots,r\}$, the pulled-back frame vector is defined by \begin{align*} \tilde e_{j,a}(x)=(x,e_{j,a}(f(x)))\in (f^*E)_x. \end{align*} The original transition function $g_{ij}:V_i\cap V_j\to GL(r,\mathbb R)$ is defined by the following identity for every $y\in V_i\cap V_j$: \begin{align*} e_{j,a}(y)=\sum_{b=1}^r e_{i,b}(y)\,(g_{ij}(y))_{ba}. \end{align*} We now substitute $y=f(x)$, which is allowed because $f(x)\in V_i\cap V_j$. This gives \begin{align*} e_{j,a}(f(x))=\sum_{b=1}^r e_{i,b}(f(x))\,(g_{ij}(f(x)))_{ba}. \end{align*} The fibre of the pullback vector bundle over $x$ is the vector space \begin{align*} (f^*E)_x=\{x\}\times E_{f(x)}. \end{align*} Its vector space operations are inherited from the fibre $E_{f(x)}$ in the second component. Hence the preceding equality in $E_{f(x)}$ becomes an equality in $(f^*E)_x$. First, \begin{align*} \tilde e_{j,a}(x)=(x,e_{j,a}(f(x))). \end{align*} Substituting the frame-change formula in the second component gives that $\tilde e_{j,a}(x)$ is the pair whose first component is $x$ and whose second component is \begin{align*} \sum_{b=1}^r e_{i,b}(f(x))\,(g_{ij}(f(x)))_{ba}. \end{align*} Because scalar multiplication and addition in $(f^*E)_x$ are inherited from $E_{f(x)}$ in the second component, the preceding expression equals \begin{align*} \tilde e_{j,a}(x)=\sum_{b=1}^r (x,e_{i,b}(f(x)))\,(g_{ij}(f(x)))_{ba}. \end{align*} Using again the definition $(x,e_{i,b}(f(x)))=\tilde e_{i,b}(x)$ for each $b\in\{1,\dots,r\}$, we obtain \begin{align*} \tilde e_{j,a}(x)=\sum_{b=1}^r \tilde e_{i,b}(x)\,(g_{ij}(f(x)))_{ba}. \end{align*} This is exactly the change-of-frame relation for the pulled-back frames, with the same matrix as the original transition matrix evaluated at $f(x)$.[/guided]

[step:Identify the transition function between the pulled-back frames] By definition, the transition function $\tilde g_{ij}$ is the unique map from $f^{-1}(V_i\cap V_j)$ to $GL(r,\mathbb R)$ whose matrix entries satisfy \begin{align*} \tilde e_{j,a}(x)=\sum_{b=1}^r \tilde e_{i,b}(x)\,(\tilde g_{ij}(x))_{ba} \end{align*} for all $x\in f^{-1}(V_i\cap V_j)$ and all $a\in\{1,\dots,r\}$. Comparing this defining identity with the identity proved above gives \begin{align*} (\tilde g_{ij}(x))_{ba}=(g_{ij}(f(x)))_{ba} \end{align*} for all $a,b\in\{1,\dots,r\}$. Hence \begin{align*} \tilde g_{ij}(x)=g_{ij}(f(x)). \end{align*} Since $x\in f^{-1}(V_i\cap V_j)$ was arbitrary, $\tilde g_{ij}=g_{ij}\circ f$ on $f^{-1}(V_i\cap V_j)$. [/step]

[step:Verify that the pulled-back transition function is smooth] The set $f^{-1}(V_i\cap V_j)$ is open in $M$ because $V_i\cap V_j$ is open in $N$ and $f:M\to N$ is smooth, hence continuous. The restriction $f|_{f^{-1}(V_i\cap V_j)}$ is a smooth map from $f^{-1}(V_i\cap V_j)$ to $V_i\cap V_j$, and $g_{ij}:V_i\cap V_j\to GL(r,\mathbb R)$ is smooth by the definition of the transition functions of the smooth vector bundle $E$. Therefore the composition \begin{align*} g_{ij}\circ f|_{f^{-1}(V_i\cap V_j)}:f^{-1}(V_i\cap V_j)\to GL(r,\mathbb R) \end{align*} is smooth. This composition is precisely $\tilde g_{ij}$, so the pulled-back transition functions are smooth and are given by \begin{align*} \tilde g_{ij}=g_{ij}\circ f. \end{align*} This proves the theorem. [/step]