[proofplan] A vector bundle isomorphism to the product bundle transports the standard basis of $\mathbb{R}^k$ to $k$ smooth global sections of $E$, and fibrewise linearity makes those sections a basis in every fibre. Conversely, a global frame gives a fibrewise [linear map](/page/Linear%20Map) from $M \times \mathbb{R}^k$ to $E$ by taking linear combinations of the frame vectors. The only point requiring verification is smoothness of this map and of its inverse; this is checked in local bundle trivializations, where the frame becomes a smooth invertible matrix-valued function. [/proofplan]

[step:Pull back the standard basis along a bundle trivialization] Assume first that there is a smooth vector bundle isomorphism \begin{align*} \Psi:E \to M \times \mathbb{R}^k \end{align*} over $M$, meaning $\operatorname{pr}_1 \circ \Psi=\pi$ and each fibre map \begin{align*} \Psi_x:E_x \to \{x\}\times \mathbb{R}^k \end{align*} is a linear isomorphism. Let $u_1,\dots,u_k \in \mathbb{R}^k$ denote the standard basis. For each $i \in \{1,\dots,k\}$, define a map \begin{align*} e_i:M \to E, \qquad e_i(x):=\Psi^{-1}(x,u_i). \end{align*} Since the map $x \mapsto (x,u_i)$ is a smooth section of the product bundle and $\Psi^{-1}:M\times \mathbb{R}^k \to E$ is smooth, each $e_i$ is a smooth section of $E$. For every $x \in M$, the vectors $(x,u_1),\dots,(x,u_k)$ form a basis of the fibre $\{x\}\times \mathbb{R}^k$. Since $\Psi_x:E_x \to \{x\}\times\mathbb{R}^k$ is a linear isomorphism, their inverse images $e_1(x),\dots,e_k(x)$ form a basis of $E_x$. Thus $e_1,\dots,e_k$ are a global frame. [/step]

[step:Use a global frame to define a fibrewise linear map from the product bundle] Conversely, suppose that $e_1,\dots,e_k:M \to E$ are smooth global sections such that $e_1(x),\dots,e_k(x)$ form a basis of $E_x$ for every $x \in M$. Define a map \begin{align*} \Phi:M \times \mathbb{R}^k \to E, \qquad \Phi(x,a):=\sum_{i=1}^k a_i e_i(x), \end{align*} where $a=(a_1,\dots,a_k) \in \mathbb{R}^k$ and the sum is taken in the [vector space](/page/Vector%20Space) $E_x$. The map $\Phi$ lies over $M$, because $\pi(e_i(x))=x$ for each section $e_i$, hence \begin{align*} \pi(\Phi(x,a))=x=\operatorname{pr}_1(x,a). \end{align*} For each fixed $x \in M$, the fibre map \begin{align*} \Phi_x:\mathbb{R}^k \to E_x, \qquad \Phi_x(a):=\sum_{i=1}^k a_i e_i(x) \end{align*} is linear. Since $e_1(x),\dots,e_k(x)$ is a basis of $E_x$, the map $\Phi_x$ is a linear isomorphism. [/step]

[step:Check smoothness and construct the smooth inverse in local trivializations]It remains to prove that $\Phi$ is a smooth diffeomorphism of total spaces with smooth fibrewise-linear inverse. Let $p \in M$. Choose an open neighbourhood $U \subset M$ of $p$ and a smooth bundle trivialization \begin{align*} \tau:\pi^{-1}(U) \to U \times \mathbb{R}^k \end{align*} over $U$. Let $\operatorname{pr}_2:U\times\mathbb{R}^k\to\mathbb{R}^k$ denote the second projection. For each $i \in \{1,\dots,k\}$, define the smooth coordinate vector map \begin{align*} v_i:U \to \mathbb{R}^k, \qquad v_i(x):=\operatorname{pr}_2(\tau(e_i(x))). \end{align*} Define the matrix-valued map \begin{align*} A:U &\to \mathbb{R}^{k\times k} \end{align*} by taking $v_i(x)$ as the $i$-th column of $A(x)$. Since each $v_i$ is smooth, every entry of $A$ is smooth. In the trivialization $\tau$, the map $\Phi$ is represented by \begin{align*} U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,a) \mapsto (x,A(x)a). \end{align*} This map is smooth because its coordinate functions are finite sums of products of smooth functions. For every $x \in U$, the vectors $e_1(x),\dots,e_k(x)$ form a basis of $E_x$, so their coordinate vectors $v_1(x),\dots,v_k(x)$ form a basis of $\mathbb{R}^k$. Hence $A(x) \in GL(k,\mathbb{R})$. The local inverse is represented in the same trivialization by \begin{align*} U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,b) \mapsto (x,A(x)^{-1}b). \end{align*} The entries of $A(x)^{-1}$ are given by the cofactor formula divided by $\det A(x)$. Since the entries of $A$ are smooth and $\det A(x)\neq 0$ for all $x \in U$, the entries of $A^{-1}$ are smooth on $U$. Therefore the local inverse is smooth.[/step]

[guided]The main issue in the converse direction is not fibrewise bijectivity; the frame hypothesis already gives that. The point is to verify smoothness of both the map and its inverse as maps between manifolds. Fix $p \in M$ and choose an open neighbourhood $U \subset M$ of $p$ together with a smooth bundle trivialization \begin{align*} \tau:\pi^{-1}(U) \to U \times \mathbb{R}^k \end{align*} over $U$. This means that $\tau$ identifies every fibre $E_x$ with $\{x\}\times\mathbb{R}^k$ by a linear isomorphism, smoothly in $x$. Let $\operatorname{pr}_2:U\times\mathbb{R}^k\to\mathbb{R}^k$ denote the second projection. For each frame section $e_i:M \to E$, define its coordinate vector in this trivialization by \begin{align*} v_i:U \to \mathbb{R}^k, \qquad v_i(x):=\operatorname{pr}_2(\tau(e_i(x))). \end{align*} The map $v_i$ is smooth because $e_i$ is smooth, $\tau$ is smooth, and $\operatorname{pr}_2$ is smooth. Now define \begin{align*} A:U &\to \mathbb{R}^{k\times k} \end{align*} by declaring that the $i$-th column of $A(x)$ is $v_i(x)$. Thus $A(x)$ records the frame vectors in the local trivialization. In these coordinates, the map $\Phi$ becomes \begin{align*} U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,a) \mapsto (x,A(x)a). \end{align*} Indeed, if $a=(a_1,\dots,a_k)$, then linearity of the fibre map induced by $\tau$ gives \begin{align*} \tau\left(\sum_{i=1}^k a_i e_i(x)\right) = \left(x,\sum_{i=1}^k a_i v_i(x)\right) = (x,A(x)a). \end{align*} This coordinate expression is smooth because each component is a finite sum of products of smooth functions. We must also show that the inverse is smooth. For each $x \in U$, the vectors $e_1(x),\dots,e_k(x)$ form a basis of $E_x$. Since $\tau$ is fibrewise linear and invertible, the coordinate vectors $v_1(x),\dots,v_k(x)$ form a basis of $\mathbb{R}^k$. Therefore $A(x)$ is an invertible matrix, so $A(x)\in GL(k,\mathbb{R})$. The inverse coordinate map must solve $b=A(x)a$ for $a$, so it is \begin{align*} U \times \mathbb{R}^k \to U \times \mathbb{R}^k, \qquad (x,b) \mapsto (x,A(x)^{-1}b). \end{align*} The entries of $A(x)^{-1}$ are smooth functions of $x$: by the cofactor formula, each entry is a polynomial in the entries of $A(x)$ divided by $\det A(x)$, and $\det A(x)$ never vanishes on $U$. Hence the inverse coordinate map is smooth. Since this argument works around every point $p \in M$, $\Phi$ is a smooth map with smooth inverse globally.[/guided]

[step:Conclude that the frame map is a vector bundle isomorphism] The preceding step shows that $\Phi:M\times\mathbb{R}^k \to E$ is a smooth bijection with smooth inverse. The second step shows that $\Phi$ lies over $M$ and is linear on every fibre. Hence $\Phi$ is a smooth vector bundle isomorphism from the product bundle $\operatorname{pr}_1:M\times\mathbb{R}^k \to M$ onto $\pi:E\to M$. This proves that $E$ is trivial whenever it admits a global frame, and together with the first direction establishes the equivalence. [/step]