[proofplan]
We construct the isomorphism by evaluation: a frame $u:\mathbb{R}^r \to E_x$ sends a vector $v \in \mathbb{R}^r$ to the vector $u(v) \in E_x$. The compatibility relation in the associated bundle is exactly designed so that changing the frame representative by the right $GL_r(\mathbb{R})$-action does not change the evaluated vector. After proving well-definedness and fibrewise linear bijectivity, we verify smoothness in a local frame, where the map becomes the identity map on $U \times \mathbb{R}^r$.
[/proofplan]
[step:Define the evaluation map on the associated bundle]
Let $P := \operatorname{Fr}(E)$, and let $\pi_P:P \to M$ denote its bundle projection. The associated bundle $P \times_{GL_r(\mathbb{R})} \mathbb{R}^r$ is the quotient of $P \times \mathbb{R}^r$ by the [equivalence relation](/page/Equivalence%20Relation)
\begin{align*}
(u \cdot A, v) \sim (u, Av)
\end{align*}
for every $u \in P$, $A \in GL_r(\mathbb{R})$, and $v \in \mathbb{R}^r$. Denote the equivalence class of $(u,v)$ by $[u,v]$.
Define the map $\Phi:P \times_{GL_r(\mathbb{R})} \mathbb{R}^r \to E$ by
\begin{align*}
\Phi([u,v]) := u(v).
\end{align*}
Here $u \in P_x$ is a linear isomorphism $u:\mathbb{R}^r \to E_x$, so $u(v) \in E_x$. Therefore $\Phi$ lies over the identity map on $M$: if $[u,v]$ belongs to the fibre over $x$, then $\Phi([u,v]) \in E_x$.
[/step]
[step:Check that evaluation is independent of the chosen representative]
Suppose $(u',v')$ is another representative of the same associated-bundle element. It is enough to check the generating relation. Let $A \in GL_r(\mathbb{R})$, and let $u' = u \cdot A = u \circ A$ and $v'=v$. Then
\begin{align*}
\Phi([u \cdot A,v]) = (u \circ A)(v) = u(Av) = \Phi([u,Av]).
\end{align*}
Since $[u \cdot A,v]=[u,Av]$ by the defining relation of the associated bundle, the formula $\Phi([u,v])=u(v)$ is well-defined.
[guided]
The only possible ambiguity in the formula $\Phi([u,v])=u(v)$ is that an associated-bundle element has many representatives. The quotient relation says that, for every matrix $A \in GL_r(\mathbb{R})$, the pair $(u \cdot A,v)$ represents the same class as $(u,Av)$. With the chosen right action on frames, $u \cdot A$ means $u \circ A$, so evaluation gives
\begin{align*}
\Phi([u \cdot A,v]) = (u \circ A)(v).
\end{align*}
By associativity of composition and the standard action of $GL_r(\mathbb{R})$ on $\mathbb{R}^r$, this equals
\begin{align*}
u(Av).
\end{align*}
But this is exactly the value of the other representative:
\begin{align*}
\Phi([u,Av]) = u(Av).
\end{align*}
Thus the two representatives forced to be equal in the quotient have the same image in $E$. Since the quotient equivalence relation is generated by these elementary changes of representative, the evaluation formula defines a genuine map on the associated bundle.
[/guided]
[/step]
[step:Prove fibrewise linear bijectivity]
Fix $x \in M$. Let $\Phi_x:(P_x \times_{GL_r(\mathbb{R})} \mathbb{R}^r) \to E_x$ denote the restriction of $\Phi$ to the fibre over $x$. It is linear because, for any fixed frame $u \in P_x$ and any $v,w \in \mathbb{R}^r$ and $a,b \in \mathbb{R}$,
\begin{align*}
\Phi_x([u,av+bw]) = u(av+bw) = a u(v)+b u(w) = a\Phi_x([u,v])+b\Phi_x([u,w]).
\end{align*}
The map $\Phi_x$ is surjective: if $e \in E_x$, choose any frame $u \in P_x$. Since $u:\mathbb{R}^r \to E_x$ is an isomorphism, there exists $v \in \mathbb{R}^r$ such that $u(v)=e$, and then $\Phi_x([u,v])=e$.
The map $\Phi_x$ is injective: suppose $\Phi_x([u,v])=\Phi_x([w,z])$ for frames $u,w \in P_x$ and vectors $v,z \in \mathbb{R}^r$. Define the [linear map](/page/Linear%20Map) $A:\mathbb{R}^r \to \mathbb{R}^r$ by
\begin{align*}
A := u^{-1} \circ w.
\end{align*}
Then $A \in GL_r(\mathbb{R})$ and $w=u \circ A=u \cdot A$. The equality $u(v)=w(z)=u(Az)$ implies $v=Az$ because $u$ is injective. Hence
\begin{align*}
[w,z]=[u \cdot A,z]=[u,Az]=[u,v].
\end{align*}
Therefore $\Phi_x$ is a linear isomorphism for every $x \in M$.
[/step]
[step:Verify smoothness in a local frame]
Let $U \subset M$ be an [open set](/page/Open%20Set) over which $E$ admits a smooth local frame $s_1,\dots,s_r:U \to E$. Define the frame-valued smooth map $s:U \to P|_U$ by declaring $s(x):\mathbb{R}^r \to E_x$ to be
\begin{align*}
s(x)(a_1,\dots,a_r)=\sum_{i=1}^r a_i s_i(x).
\end{align*}
This local frame gives a vector bundle trivialization $\tau_E:E|_U \to U \times \mathbb{R}^r$ defined by
\begin{align*}
\tau_E\left(\sum_{i=1}^r a_i s_i(x)\right)=(x,(a_1,\dots,a_r)).
\end{align*}
It also gives a local trivialization $\tau_A:(P \times_{GL_r(\mathbb{R})} \mathbb{R}^r)|_U \to U \times \mathbb{R}^r$ of the associated bundle defined by
\begin{align*}
\tau_A([s(x),a])=(x,a).
\end{align*}
For $a=(a_1,\dots,a_r)\in \mathbb{R}^r$, we have
\begin{align*}
(\tau_E \circ \Phi \circ \tau_A^{-1})(x,a) = (x,a).
\end{align*}
Thus, in local trivializations, $\Phi$ is the identity map on $U \times \mathbb{R}^r$. Hence $\Phi$ is smooth. Since the same coordinate calculation shows that the local representative of $\Phi^{-1}$ is also the identity map on $U \times \mathbb{R}^r$, the inverse map is smooth as well.
[/step]
[step:Conclude natural vector bundle isomorphism]
The map $\Phi$ covers $\operatorname{id}_M$, is linear on every fibre, is a fibrewise bijection, and is smooth with smooth inverse. Therefore $\Phi$ is a smooth vector bundle isomorphism over $M$:
\begin{align*}
\operatorname{Fr}(E) \times_{GL_r(\mathbb{R})} \mathbb{R}^r \cong E.
\end{align*}
The construction uses only evaluation of a frame on a vector and is therefore natural in the vector bundle $E$.
[/step]
