[proofplan]
We construct the two functors explicitly and then build natural isomorphisms in both directions. For a vector bundle $E$, evaluation of a frame on a vector descends to an isomorphism $\operatorname{Fr}(E)\times_{GL_r(\mathbb{R})}\mathbb{R}^r \cong E$. Conversely, for a principal bundle $P$, each point $u \in P_p$ gives a frame of the associated vector bundle by $v \mapsto [u,v]$, and these frames identify $P$ with the frame bundle of the associated bundle. The final step verifies that these identifications commute with isomorphisms, giving an equivalence of categories rather than only a bijection on objects.
[/proofplan]
[step:Define the frame and associated bundle functors]
Let $G := GL_r(\mathbb{R})$. For a smooth rank-$r$ real vector bundle $\pi_E:E \to M$, define the smooth principal right $G$-bundle $\operatorname{Fr}(E) \to M$ by
\begin{align*}
\operatorname{Fr}(E)_p=\{\nu:\mathbb{R}^r \to E_p \mid \nu \text{ is a linear isomorphism}\}.
\end{align*}
The right action is
\begin{align*}
\operatorname{Fr}(E)_p \times G \to \operatorname{Fr}(E)_p,\qquad (\nu,g)\mapsto \nu \cdot g := \nu \circ g.
\end{align*}
This action is free and transitive on each fiber, since any two frames $\nu,\mu:\mathbb{R}^r \to E_p$ satisfy $\mu=\nu\circ(\nu^{-1}\circ\mu)$ with $\nu^{-1}\circ\mu \in G$.
If $F:E \to E'$ is a vector bundle isomorphism over $\operatorname{id}_M$, define
\begin{align*}
\operatorname{Fr}(F):\operatorname{Fr}(E) \to \operatorname{Fr}(E'),\qquad \nu \mapsto F_{\pi_E(\nu)}\circ \nu.
\end{align*}
This is smooth in local bundle charts, covers $\operatorname{id}_M$, and is $G$-equivariant because
\begin{align*}
\operatorname{Fr}(F)(\nu \cdot g)=F_{\pi_E(\nu)}\circ \nu \circ g=\operatorname{Fr}(F)(\nu)\cdot g.
\end{align*}
Thus $E \mapsto \operatorname{Fr}(E)$ defines a functor
\begin{align*}
\operatorname{Fr}: \mathrm{Vect}_r(M) \to \mathrm{Prin}_G(M).
\end{align*}
Conversely, for a smooth principal right $G$-bundle $\pi_P:P \to M$, define
\begin{align*}
A(P):=P\times_G \mathbb{R}^r.
\end{align*}
Here $P\times_G\mathbb{R}^r$ is the quotient of $P\times \mathbb{R}^r$ by the [equivalence relation](/page/Equivalence%20Relation)
\begin{align*}
(u\cdot g,v)\sim (u,g v)
\end{align*}
for $u\in P$, $g\in G$, and $v\in\mathbb{R}^r$. Write $[u,v]$ for the equivalence class of $(u,v)$. The projection is
\begin{align*}
A(P) \to M,\qquad [u,v]\mapsto \pi_P(u).
\end{align*}
Local principal trivializations identify this quotient with $U\times\mathbb{R}^r$, so $A(P)\to M$ is a smooth real rank-$r$ vector bundle.
If $\Psi:P \to Q$ is a principal bundle isomorphism over $\operatorname{id}_M$, define
\begin{align*}
A(\Psi):A(P) \to A(Q),\qquad [u,v]\mapsto [\Psi(u),v].
\end{align*}
This is well-defined because $\Psi(u\cdot g)=\Psi(u)\cdot g$, so
\begin{align*}
[\Psi(u\cdot g),v]=[\Psi(u)\cdot g,v]=[\Psi(u),gv].
\end{align*}
It is a smooth vector bundle isomorphism in local principal charts. Therefore $P\mapsto A(P)$ defines a functor
\begin{align*}
A:\mathrm{Prin}_G(M)\to \mathrm{Vect}_r(M).
\end{align*}
[/step]
[step:Identify the vector bundle recovered from its frame bundle]
Let $\pi_E:E\to M$ be a smooth real rank-$r$ vector bundle. Define
\begin{align*}
\varepsilon_E:\operatorname{Fr}(E)\times_G\mathbb{R}^r \to E,\qquad [\nu,v]\mapsto \nu(v).
\end{align*}
This map is well-defined: if $(\nu\cdot g,v)\sim(\nu,gv)$, then
\begin{align*}
(\nu\cdot g)(v)=(\nu\circ g)(v)=\nu(gv).
\end{align*}
Thus equivalent representatives have the same image.
For each $p\in M$, the fiber map
\begin{align*}
(\varepsilon_E)_p:\operatorname{Fr}(E)_p\times_G\mathbb{R}^r \to E_p
\end{align*}
is linear. It is surjective because, given $e\in E_p$, choosing any frame $\nu:\mathbb{R}^r\to E_p$ gives $e=\nu(v)$ for $v:=\nu^{-1}(e)$. It is injective because if $\nu(v)=\mu(w)$ for frames $\nu,\mu\in\operatorname{Fr}(E)_p$, then with $g:=\nu^{-1}\circ\mu\in G$ we have $\mu=\nu\cdot g$ and $gv=w$, so
\begin{align*}
[\mu,w]=[\nu\cdot g,w]=[\nu,gw]=[\nu,v].
\end{align*}
Hence $\varepsilon_E$ is a fiberwise linear bijection.
In a local vector bundle trivialization over an [open set](/page/Open%20Set) $U\subset M$, a frame $\nu\in\operatorname{Fr}(E)_p$ is represented by a matrix $a\in G$ and a vector $v\in\mathbb{R}^r$ is sent to $av\in\mathbb{R}^r$. Thus $\varepsilon_E$ is smooth and has smooth inverse locally. Therefore $\varepsilon_E$ is a smooth vector bundle isomorphism over $M$.
[guided]
The goal is to compare $E$ with the vector bundle obtained by first taking frames and then forming the associated bundle. A point of $\operatorname{Fr}(E)\times_G\mathbb{R}^r$ is represented by a frame $\nu:\mathbb{R}^r\to E_p$ and a vector $v\in\mathbb{R}^r$. The only natural candidate map is evaluation:
\begin{align*}
\varepsilon_E:\operatorname{Fr}(E)\times_G\mathbb{R}^r \to E,\qquad [\nu,v]\mapsto \nu(v).
\end{align*}
The first issue is well-definedness. In the associated bundle, the relation is
\begin{align*}
(\nu\cdot g,v)\sim(\nu,gv)
\end{align*}
for $g\in G$. Since the frame action is $\nu\cdot g=\nu\circ g$, evaluating the two representatives gives
\begin{align*}
(\nu\cdot g)(v)=(\nu\circ g)(v)=\nu(gv).
\end{align*}
So the two representatives determine the same vector in $E_p$, and $\varepsilon_E$ is well-defined.
Now fix $p\in M$. We prove that the fiber map is a linear isomorphism. It is linear because scalar multiplication and addition in the associated bundle are induced from the [vector space](/page/Vector%20Space) operations in $\mathbb{R}^r$, and each frame $\nu:\mathbb{R}^r\to E_p$ is linear. For surjectivity, take $e\in E_p$. Choose a frame $\nu:\mathbb{R}^r\to E_p$ and define $v:=\nu^{-1}(e)$. Then $\varepsilon_E([\nu,v])=\nu(v)=e$.
For injectivity, suppose $\varepsilon_E([\nu,v])=\varepsilon_E([\mu,w])$. This means $\nu(v)=\mu(w)$ in $E_p$. Define
\begin{align*}
g:=\nu^{-1}\circ\mu:\mathbb{R}^r\to\mathbb{R}^r.
\end{align*}
Because $\nu$ and $\mu$ are linear isomorphisms, $g\in G$, and $\mu=\nu\circ g=\nu\cdot g$. From $\nu(v)=\mu(w)=\nu(gw)$ and injectivity of $\nu$, we get $v=gw$. Therefore
\begin{align*}
[\mu,w]=[\nu\cdot g,w]=[\nu,gw]=[\nu,v].
\end{align*}
So the fiber map is injective.
Finally, the fiberwise linear bijection is smooth with smooth inverse because this can be checked in local trivializations. On an open set $U\subset M$ over which $E$ is trivial, frames are represented by matrices $a\in G$, vectors in the associated copy of $\mathbb{R}^r$ are represented by $v\in\mathbb{R}^r$, and the map is simply matrix multiplication $a v$. Matrix multiplication is smooth, and the inverse is obtained by choosing the standard local frame in the trivialization. Hence $\varepsilon_E$ is a smooth vector bundle isomorphism over $M$.
[/guided]
[/step]
[step:Identify a principal bundle with the frame bundle of its associated vector bundle]
Let $\pi_P:P\to M$ be a smooth principal right $G$-bundle and let
\begin{align*}
A(P):=P\times_G\mathbb{R}^r.
\end{align*}
For each $u\in P$, with $p:=\pi_P(u)$, define
\begin{align*}
\theta_u:\mathbb{R}^r \to A(P)_p,\qquad v\mapsto [u,v].
\end{align*}
The map $\theta_u$ is linear by the vector space structure on the associated fiber. It is injective because $[u,v]=[u,w]$ implies $v=w$. It is surjective because every element of $A(P)_p$ has the form $[u',v']$ with $u'\in P_p$, and since the principal action is transitive on $P_p$, there is $g\in G$ such that $u'=u\cdot g$, hence
\begin{align*}
[u',v']=[u\cdot g,v']=[u,gv'].
\end{align*}
Thus $\theta_u$ is a frame of $A(P)_p$.
Define
\begin{align*}
\eta_P:P\to \operatorname{Fr}(A(P)),\qquad u\mapsto \theta_u.
\end{align*}
This map covers $\operatorname{id}_M$. It is $G$-equivariant because for $g\in G$ and $v\in\mathbb{R}^r$,
\begin{align*}
\theta_{u\cdot g}(v)=[u\cdot g,v]=[u,gv]=\theta_u(gv)=(\theta_u\circ g)(v)=(\theta_u\cdot g)(v).
\end{align*}
Therefore $\eta_P(u\cdot g)=\eta_P(u)\cdot g$.
The map $\eta_P$ is bijective on each fiber. Indeed, if $\theta_u=\theta_{u'}$, then $u'=u\cdot g$ for a unique $g\in G$, and
\begin{align*}
\theta_{u'}(v)=\theta_{u\cdot g}(v)=\theta_u(gv).
\end{align*}
Equality $\theta_{u'}=\theta_u$ implies $gv=v$ for all $v\in\mathbb{R}^r$, so $g=I_r$ and $u'=u$. Conversely, any frame of $A(P)_p$ is obtained from some $\theta_u$ because, in a principal local trivialization, frames of the associated bundle are exactly the standard frame multiplied on the right by an element of $G$, and the fiber $P_p$ is exactly the corresponding $G$-torsor. Hence $\eta_P$ is a smooth principal bundle isomorphism over $M$.
[/step]
[step:Verify naturality of the two identifications]
Let $F:E\to E'$ be a vector bundle isomorphism over $\operatorname{id}_M$. For every frame $\nu\in\operatorname{Fr}(E)$ and vector $v\in\mathbb{R}^r$,
\begin{align*}
\varepsilon_{E'}([\operatorname{Fr}(F)(\nu),v])=(F_{\pi_E(\nu)}\circ\nu)(v)=F(\nu(v))=F(\varepsilon_E([\nu,v])).
\end{align*}
Thus the family $\varepsilon_E:A(\operatorname{Fr}(E))\to E$ is natural in $E$.
Let $\Psi:P\to Q$ be a principal bundle isomorphism over $\operatorname{id}_M$. For $u\in P$, define $\theta_u:\mathbb{R}^r\to A(P)_{\pi_P(u)}$ by $\theta_u(v)=[u,v]$, and define $\theta_{\Psi(u)}:\mathbb{R}^r\to A(Q)_{\pi_Q(\Psi(u))}$ by $\theta_{\Psi(u)}(v)=[\Psi(u),v]$. Then
\begin{align*}
\operatorname{Fr}(A(\Psi))(\theta_u)(v)=A(\Psi)([u,v])=[\Psi(u),v]=\theta_{\Psi(u)}(v).
\end{align*}
Hence
\begin{align*}
\operatorname{Fr}(A(\Psi))(\eta_P(u))=\eta_Q(\Psi(u)).
\end{align*}
Thus the family $\eta_P:P\to\operatorname{Fr}(A(P))$ is natural in $P$.
[/step]
[step:Conclude that the two functors are quasi-inverse equivalences]
The functors
\begin{align*}
\operatorname{Fr}: \mathrm{Vect}_r(M)\to \mathrm{Prin}_G(M)
\end{align*}
and
\begin{align*}
A:\mathrm{Prin}_G(M)\to \mathrm{Vect}_r(M)
\end{align*}
satisfy
\begin{align*}
A\circ\operatorname{Fr}\cong \operatorname{Id}_{\mathrm{Vect}_r(M)}
\end{align*}
by the natural vector bundle isomorphisms $\varepsilon_E$, and
\begin{align*}
\operatorname{Fr}\circ A\cong \operatorname{Id}_{\mathrm{Prin}_G(M)}
\end{align*}
by the natural principal bundle isomorphisms $\eta_P$. Therefore $\operatorname{Fr}$ is an equivalence of categories, with quasi-inverse $P\mapsto P\times_G\mathbb{R}^r$. This proves the theorem.
[/step]
