[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$.[/step]

[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: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]