[proofplan] We prove the frame property directly from the definition of the pullback bundle. First we record the canonical fibre identification: the fibre of $f^*E$ over $x$ is naturally the [vector space](/page/Vector%20Space) $E_{f(x)}$, represented by pairs $(x,e)$ with $e\in E_{f(x)}$. Under this identification, the pulled-back sections evaluate to the original frame vectors at $f(x)$, so they form a basis in each fibre. Smoothness is checked in the local trivialization determined by the original frame, where the pulled-back sections become the constant coordinate sections. [/proofplan]

[step:Identify the fibres of the pullback bundle over $f^{-1}(V)$] Let $U:=f^{-1}(V)\subset M$. Since $f:M\to N$ is continuous and $V\subset N$ is open, $U$ is open in $M$. Let $\pi$ denote the bundle projection from $E$ to $N$. By the definition of the pullback bundle, $f^*E$ is the submanifold of $M\times E$ consisting of all pairs $(x,e)$ such that $\pi(e)=f(x)$. Let $\pi_f$ denote the projection map from $f^*E$ to $M$ defined by $\pi_f(x,e)=x$. For each $x\in U$, the fibre of $f^*E$ over $x$ satisfies \begin{align*} (f^*E)_x=\pi_f^{-1}(\{x\})=\{(x,e):e\in E_{f(x)}\}. \end{align*} Define the fibre identification \begin{align*} \iota_x:E_{f(x)}\to (f^*E)_x \end{align*} by the rule $\iota_x(e)=(x,e)$ for $e\in E_{f(x)}$. This map is a linear isomorphism, with inverse $(x,e)\mapsto e$. [/step]

[step:Verify that the pulled-back sections form a basis in every fibre] Fix $x\in U$. Since $(s_1,\dots,s_r)$ is a local frame over $V$ and $f(x)\in V$, the tuple \begin{align*} (s_1(f(x)),\dots,s_r(f(x))) \end{align*} is a basis of $E_{f(x)}$. Applying the linear isomorphism $\iota_x:E_{f(x)}\to (f^*E)_x$ gives the tuple \begin{align*} (\iota_x(s_1(f(x))),\dots,\iota_x(s_r(f(x)))). \end{align*} By the definition of $f^*s_i$, this tuple is exactly \begin{align*} ((f^*s_1)(x),\dots,(f^*s_r)(x)). \end{align*} Therefore $(f^*s_1(x),\dots,f^*s_r(x))$ is a basis of $(f^*E)_x$ for every $x\in U$. [/step]

[step:Check smoothness in the frame trivialization]Let $(e_1,\dots,e_r)$ denote the standard basis of $\mathbb{R}^r$. The original frame determines a vector bundle trivialization \begin{align*} \Phi:E|_V\to V\times\mathbb{R}^r \end{align*} by the rule that, for $y\in V$ and coefficients $a_1,\dots,a_r\in\mathbb{R}$, \begin{align*} \Phi\left(\sum_{j=1}^r a_j s_j(y)\right)=(y,(a_1,\dots,a_r)). \end{align*} We verify smoothness locally. Fix $y_0\in V$, and choose an [open set](/page/Open%20Set) $W\subset V$ containing $y_0$ and a smooth bundle trivialization $\Theta:E|_W\to W\times\mathbb{R}^r$. For each $j\in\{1,\dots,r\}$, define the coordinate map $b_j:W\to\mathbb{R}^r$ by requiring $\Theta(s_j(y))=(y,b_j(y))$. Since $s_j$ and $\Theta$ are smooth, each $b_j$ is smooth. Define $A:W\to\mathbb{R}^{r\times r}$ to be the matrix whose $j$th column is $b_j(y)$. Since $(s_1(y),\dots,s_r(y))$ is a basis of $E_y$, the matrix $A(y)$ is invertible for every $y\in W$. In the trivialization $\Theta$, if $\Theta(e)=(y,c)$, then the coefficient vector $a$ satisfying $e=\sum_{j=1}^r a_j s_j(y)$ is $a=A(y)^{-1}c$. Matrix inversion is smooth on $GL_r(\mathbb{R})$, so the local formula $(y,c)\mapsto (y,A(y)^{-1}c)$ proves that $\Phi$ is smooth near $y_0$. Since $y_0$ was arbitrary, $\Phi$ is smooth on $E|_V$, and its inverse $(y,a)\mapsto \sum_{j=1}^r a_j s_j(y)$ is smooth because fibrewise addition and scalar multiplication are smooth. The associated pullback trivialization is the smooth map $\Psi:(f^*E)|_U\to U\times\mathbb{R}^r$ defined by $\Psi(x,e)=(x,a)$, where $a=(a_1,\dots,a_r)\in\mathbb{R}^r$ is the unique vector satisfying \begin{align*} \Phi(e)=(f(x),a). \end{align*} Equivalently, $\Psi$ is obtained from the smooth map $(x,e)\mapsto (x,\operatorname{pr}_2(\Phi(e)))$, where $\operatorname{pr}_2:V\times\mathbb{R}^r\to\mathbb{R}^r$ is the second projection. By the local characterization of smooth vector bundle sections, a section is smooth if and only if its coordinate representative in every smooth local trivialization is smooth. Thus it is enough to compute each pulled-back section in the smooth trivialization $\Psi$. For each $i\in\{1,\dots,r\}$ and each $x\in U$, we have \begin{align*} \Phi(s_i(f(x)))=(f(x),e_i), \end{align*} and hence \begin{align*} \Psi((f^*s_i)(x))=\Psi(x,s_i(f(x)))=(x,e_i). \end{align*} Thus, in the pullback trivialization $\Psi$, the section $f^*s_i$ is represented by the smooth map $U\to U\times\mathbb{R}^r$ given by $x\mapsto (x,e_i)$. Therefore each $f^*s_i:U\to f^*E$ is a smooth section.[/step]

[guided]The only point needing verification beyond the fibrewise basis statement is smoothness. We use the local characterization built into the definition of a smooth vector bundle section: a section is smooth precisely when, after composing with a smooth local trivialization, its base-and-fibre coordinate representative is a smooth map. Thus we use the trivialization supplied by the original frame. Let $(e_1,\dots,e_r)$ be the standard basis of $\mathbb{R}^r$. Because $(s_1,\dots,s_r)$ is a smooth local frame for $E$ over $V$, every vector $e\in E_y$ with $y\in V$ can be written uniquely as \begin{align*} e=\sum_{j=1}^r a_j s_j(y) \end{align*} for coefficients $a_1,\dots,a_r\in\mathbb{R}$. This defines the frame trivialization $\Phi:E|_V\to V\times\mathbb{R}^r$ by \begin{align*} \Phi\left(\sum_{j=1}^r a_j s_j(y)\right)=(y,(a_1,\dots,a_r)). \end{align*} Why is this a smooth trivialization? We check it in an arbitrary local trivialization. Fix $y_0\in V$, choose an open set $W\subset V$ containing $y_0$, and choose a smooth bundle trivialization $\Theta:E|_W\to W\times\mathbb{R}^r$. For each $j\in\{1,\dots,r\}$, define $b_j:W\to\mathbb{R}^r$ by $\Theta(s_j(y))=(y,b_j(y))$. These maps are smooth because they are the fibre-coordinate functions of the smooth sections $s_j$ in the smooth trivialization $\Theta$. Now define $A:W\to\mathbb{R}^{r\times r}$ by taking the $j$th column of $A(y)$ to be $b_j(y)$. The frame hypothesis says that $(s_1(y),\dots,s_r(y))$ is a basis of $E_y$, so the coordinate vectors $(b_1(y),\dots,b_r(y))$ form a basis of $\mathbb{R}^r$. Hence $A(y)\in GL_r(\mathbb{R})$ for every $y\in W$. If $\Theta(e)=(y,c)$ and $e=\sum_{j=1}^r a_j s_j(y)$, then $c=A(y)a$, so $a=A(y)^{-1}c$. Therefore, in the trivialization $\Theta$, the map $\Phi$ has the local expression $(y,c)\mapsto (y,A(y)^{-1}c)$. Since matrix inversion is smooth on $GL_r(\mathbb{R})$, this local expression is smooth. The inverse formula $(y,a)\mapsto \sum_{j=1}^r a_j s_j(y)$ is smooth because it is built from the smooth sections $s_j$ using the smooth fibrewise addition and scalar multiplication maps of the vector bundle. Now set $U:=f^{-1}(V)$. The pullback trivialization associated to $\Phi$ is $\Psi:(f^*E)|_U\to U\times\mathbb{R}^r$, defined by $\Psi(x,e)=(x,a)$, where $a=(a_1,\dots,a_r)$ is determined by \begin{align*} \Phi(e)=(f(x),a). \end{align*} This map is smooth because it is the coordinate chart used in the pullback smooth structure; explicitly, it keeps the base coordinate $x$ and records the fibre coordinate of $e\in E_{f(x)}$ in the original trivialization over $V$. For the pulled-back section $f^*s_i$, we compute its coordinate expression. Since $s_i(f(x))$ is the $i$th frame vector at $f(x)$, its coordinates in the frame $(s_1,\dots,s_r)$ are $e_i$. Therefore \begin{align*} \Phi(s_i(f(x)))=(f(x),e_i), \end{align*} and hence \begin{align*} \Psi((f^*s_i)(x))=\Psi(x,s_i(f(x)))=(x,e_i). \end{align*} The representing map $U\to U\times\mathbb{R}^r$ is given by $x\mapsto (x,e_i)$, which is smooth because it is the product of the identity map on $U$ and the constant map with value $e_i$. Thus each pulled-back section $f^*s_i$ is smooth.[/guided]

[step:Conclude that the pulled-back sections form a local frame] We have shown that each map \begin{align*} f^*s_i:U\to f^*E \end{align*} is a smooth section of $f^*E$ over $U=f^{-1}(V)$, and that for every $x\in U$ the tuple \begin{align*} ((f^*s_1)(x),\dots,(f^*s_r)(x)) \end{align*} is a basis of the fibre $(f^*E)_x$. Therefore $(f^*s_1,\dots,f^*s_r)$ is a smooth local frame for $f^*E$ over $f^{-1}(V)$. [/step]