[proofplan] A trivialisation converts each fiber $E_x$ into $\mathbb{R}^r$, so pulling back the standard basis of $\mathbb{R}^r$ gives $r$ smooth sections forming a basis in every fiber. Conversely, a frame gives fiber coordinates: a vector in $E_x$ is uniquely a linear combination of the frame vectors at $x$. The only point needing verification is smoothness of this coordinate construction and of its inverse; this is checked in an arbitrary local bundle chart by writing the frame as an invertible smooth matrix. [/proofplan]

[step:Handle the rank-zero convention] If $r=0$, then every fiber $E_x$ is the zero [vector space](/page/Vector%20Space). The product $U \times \mathbb{R}^0$ is canonically identified with $U$, and the unique ordered frame is the empty tuple. The constructions below use the empty standard basis of $\mathbb{R}^0$, the empty sum equal to the zero vector in each fiber, and the unique $0 \times 0$ matrix whose determinant is $1$; with these conventions the same argument applies verbatim. [/step]

[step:Pull back the standard basis through a trivialisation] Let $\operatorname{pr}_1: U \times \mathbb{R}^r \to U$ denote the first projection map, $\operatorname{pr}_1(x,a)=x$. Let $\tau: E|_U \to U \times \mathbb{R}^r$ be a local trivialisation, meaning that $\tau$ is a smooth diffeomorphism, $\operatorname{pr}_1 \circ \tau = \pi|_{E|_U}$, and for each $x \in U$ the restricted map $\tau_x: E_x \to \{x\} \times \mathbb{R}^r$ is linear after identifying $\{x\} \times \mathbb{R}^r$ with $\mathbb{R}^r$. Let $\varepsilon_i \in \mathbb{R}^r$ denote the $i$th standard basis vector for $1 \le i \le r$. Define, for each $i$, the map $s_i: U \to E|_U$ by $s_i(x) = \tau^{-1}(x,\varepsilon_i)$. The map $x \mapsto (x,\varepsilon_i)$ from $U$ to $U \times \mathbb{R}^r$ is smooth, and $\tau^{-1}$ is smooth, so $s_i$ is smooth. Also, \begin{align*} \pi(s_i(x)) = \operatorname{pr}_1(\tau(s_i(x))) = \operatorname{pr}_1(x,\varepsilon_i) = x, \end{align*} so $s_i$ is a section of $\pi|_{E|_U}: E|_U \to U$. For each $x \in U$, the fiber map $\tau_x: E_x \to \mathbb{R}^r$ is a linear isomorphism and sends $s_i(x)$ to $\varepsilon_i$. Since $(\varepsilon_1,\dots,\varepsilon_r)$ is a basis of $\mathbb{R}^r$, the ordered tuple $(s_1(x),\dots,s_r(x))$ is a basis of $E_x$. Thus $(s_1,\dots,s_r)$ is an ordered smooth local frame over $U$. [/step]

[step:Build a fiberwise linear map from an ordered frame] Conversely, let $(s_1,\dots,s_r)$ be an ordered smooth local frame over $U$. Define the map $\Psi: U \times \mathbb{R}^r \to E|_U$ by \begin{align*} \Psi(x,a_1,\dots,a_r) = \sum_{i=1}^r a_i s_i(x). \end{align*} The sum is taken in the vector space fiber $E_x$, because each $s_i(x)$ lies in $E_x$. For each $x \in U$, define the restricted [linear map](/page/Linear%20Map) $\Psi_x: \mathbb{R}^r \to E_x$ by \begin{align*} \Psi_x(a_1,\dots,a_r) = \sum_{i=1}^r a_i s_i(x). \end{align*} Since $(s_1(x),\dots,s_r(x))$ is a basis of $E_x$, the map $\Psi_x$ is a linear isomorphism. Moreover, \begin{align*} \pi(\Psi(x,a_1,\dots,a_r)) = x, \end{align*} so $\Psi$ is a map over $U$. [/step]

[step:Verify smoothness of the frame map and its inverse in local bundle coordinates]We prove that $\Psi$ is a smooth diffeomorphism by checking in local [vector bundle](/page/Vector%20Bundle) charts. Let $V \subset U$ be an [open set](/page/Open%20Set) over which $E$ is trivial, and let $\theta: E|_V \to V \times \mathbb{R}^r$ be a smooth local bundle chart, fiberwise linear over $V$. For $1 \le i \le r$, define the smooth map $b_i: V \to \mathbb{R}^r$ by the condition $\theta(s_i(x)) = (x,b_i(x))$ for every $x \in V$. This is smooth because $s_i$ and $\theta$ are smooth and because the second projection $V \times \mathbb{R}^r \to \mathbb{R}^r$ is smooth. Define the matrix-valued map $A: V \to \operatorname{Mat}_{r \times r}(\mathbb{R})$ by declaring that the $i$th column of $A(x)$ is $b_i(x)$. Since the entries of each $b_i$ are smooth, the entries of $A$ are smooth. Since $(s_1(x),\dots,s_r(x))$ is a basis of $E_x$ and $\theta|_{E_x}: E_x \to \mathbb{R}^r$ is a linear isomorphism, the vectors $(b_1(x),\dots,b_r(x))$ form a basis of $\mathbb{R}^r$. Hence $\det A(x) \neq 0$ for every $x \in V$. In these coordinates, \begin{align*} (\theta \circ \Psi)(x,a) = (x,A(x)a) \end{align*} for $x \in V$ and $a \in \mathbb{R}^r$. The map $(x,a) \mapsto (x,A(x)a)$ is smooth because its coordinate functions are finite sums of products of smooth functions. Therefore $\Psi$ is smooth over $V$, and since such open sets $V$ cover $U$, $\Psi$ is smooth on $U \times \mathbb{R}^r$. The inverse is also smooth in the same coordinates. If $\theta(e) = (x,v)$ with $x \in V$ and $v \in \mathbb{R}^r$, then \begin{align*} \Psi^{-1}(e) = (x,A(x)^{-1}v). \end{align*} Let $\operatorname{adj}: \operatorname{Mat}_{r \times r}(\mathbb{R}) \to \operatorname{Mat}_{r \times r}(\mathbb{R})$ denote the adjugate matrix map, which sends a square matrix to its classical cofactor-transpose matrix. The entries of $A(x)^{-1}$ are smooth functions of $x$ because \begin{align*} A(x)^{-1} = \frac{1}{\det A(x)}\operatorname{adj}(A(x)), \end{align*} the entries of $\operatorname{adj}(A(x))$ are polynomial expressions in the entries of $A(x)$, and $\det A(x)$ is nowhere zero on $V$. Hence $(x,v) \mapsto (x,A(x)^{-1}v)$ is smooth. Therefore $\Psi^{-1}$ is smooth locally on each $E|_V$, and consequently $\Psi^{-1}$ is smooth globally on $E|_U$.[/step]

[guided]The main issue is not bijectivity on each fiber; the frame already gives that. The point is to prove that the fiber coordinates vary smoothly with the base point. We do this by translating the statement into an ordinary matrix calculation in a local bundle chart. Choose an open set $V \subset U$ on which the vector bundle is trivial, and choose a smooth local bundle chart $\theta: E|_V \to V \times \mathbb{R}^r$. This chart is fiberwise linear: for each $x \in V$, the restricted map $\theta|_{E_x}: E_x \to \{x\} \times \mathbb{R}^r$ is a linear isomorphism after identifying $\{x\} \times \mathbb{R}^r$ with $\mathbb{R}^r$. Each frame section $s_i: U \to E|_U$ restricts to a smooth section over $V$. Because $\theta(s_i(x))$ lies over $x$, there is a unique vector $b_i(x) \in \mathbb{R}^r$ such that \begin{align*} \theta(s_i(x)) = (x,b_i(x)). \end{align*} This defines a map $b_i: V \to \mathbb{R}^r$. The map $b_i$ is smooth because it is obtained by composing the smooth section $s_i$, the smooth chart $\theta$, and the smooth projection map $\operatorname{pr}_2:V\times\mathbb{R}^r\to\mathbb{R}^r$, $\operatorname{pr}_2(x,v)=v$. Now assemble these coordinate vectors into a matrix. Define $A: V \to \operatorname{Mat}_{r \times r}(\mathbb{R})$ by taking the $i$th column of $A(x)$ to be $b_i(x)$. Since each entry of each $b_i$ is smooth, each entry of $A$ is smooth. For a fixed $x \in V$, the vectors $(s_1(x),\dots,s_r(x))$ are a basis of $E_x$. Applying the linear isomorphism $\theta|_{E_x}$ sends this basis to $(b_1(x),\dots,b_r(x))$, so these vectors form a basis of $\mathbb{R}^r$. Thus $A(x)$ is invertible, equivalently $\det A(x) \neq 0$, for every $x \in V$. In the chart $\theta$, the map $\Psi$ has the concrete form \begin{align*} (\theta \circ \Psi)(x,a) = (x,A(x)a). \end{align*} Indeed, if $a=(a_1,\dots,a_r)$, then fiberwise linearity of $\theta$ gives \begin{align*} \theta\left(\sum_{i=1}^r a_i s_i(x)\right) = \left(x,\sum_{i=1}^r a_i b_i(x)\right) = (x,A(x)a). \end{align*} The coordinate functions of $(x,a) \mapsto (x,A(x)a)$ are finite sums of products of smooth functions, so this map is smooth. Hence $\Psi$ is smooth on $V \times \mathbb{R}^r$. Since the trivialising sets $V$ cover $U$, smoothness holds globally. For the inverse, take $e \in E|_V$ and write $\theta(e)=(x,v)$ with $x \in V$ and $v \in \mathbb{R}^r$. The unique coefficients $a \in \mathbb{R}^r$ satisfying \begin{align*} e = \sum_{i=1}^r a_i s_i(x) \end{align*} are exactly the solution of the linear system $A(x)a=v$. Since $A(x)$ is invertible, this solution is $a=A(x)^{-1}v$, so \begin{align*} \Psi^{-1}(e) = (x,A(x)^{-1}v). \end{align*} The inverse matrix depends smoothly on $x$: by the adjugate formula, \begin{align*} A(x)^{-1} = \frac{1}{\det A(x)}\operatorname{adj}(A(x)). \end{align*} The adjugate entries are polynomial expressions in the entries of $A(x)$, and division by $\det A(x)$ is smooth because $\det A(x)$ is nowhere zero on $V$. Therefore $(x,v) \mapsto (x,A(x)^{-1}v)$ is smooth. This proves that $\Psi^{-1}$ is smooth locally in every bundle chart, and hence smooth globally.[/guided]

[step:Convert the frame map into a local trivialisation] Since $\Psi: U \times \mathbb{R}^r \to E|_U$ is a smooth diffeomorphism over $U$ and each restricted map $\Psi_x: \mathbb{R}^r \to E_x$ is a linear isomorphism, its inverse $\tau := \Psi^{-1}: E|_U \to U \times \mathbb{R}^r$ is a local trivialisation of $E$ over $U$. This constructs a local trivialisation from the ordered local frame $(s_1,\dots,s_r)$. [/step]

[step:Check that the two constructions are inverse] Starting with a trivialisation $\tau: E|_U \to U \times \mathbb{R}^r$, the associated frame is defined by $s_i(x)=\tau^{-1}(x,\varepsilon_i)$. The frame map constructed from these sections is \begin{align*} \Psi(x,a_1,\dots,a_r) = \sum_{i=1}^r a_i \tau^{-1}(x,\varepsilon_i). \end{align*} Because $\tau^{-1}$ is fiberwise linear on $\{x\} \times \mathbb{R}^r$, this equals \begin{align*} \Psi(x,a_1,\dots,a_r) = \tau^{-1}(x,a_1,\dots,a_r). \end{align*} Therefore the recovered trivialisation $\Psi^{-1}$ is exactly $\tau$. Starting with an ordered frame $(s_1,\dots,s_r)$, the constructed trivialisation is $\tau=\Psi^{-1}$. The frame recovered from $\tau$ is \begin{align*} \tilde{s}_i(x) = \tau^{-1}(x,\varepsilon_i) = \Psi(x,\varepsilon_i) = s_i(x), \end{align*} because $\Psi(x,\varepsilon_i)$ selects the $i$th vector of the frame. Hence the two constructions are mutually inverse. This proves the claimed natural bijection between local trivialisations and ordered smooth local frames over $U$. [/step]