[proofplan] We construct the smooth structure on $\operatorname{Fr}(E)$ directly from vector bundle trivializations of $E$. A local vector bundle chart identifies a frame $\nu:\mathbb R^r\to E_p$ with the matrix of the composite $\mathbb R^r\xrightarrow{\nu}E_p\to\mathbb R^r$, giving a local model $q^{-1}(U)\cong U\times GL_r(\mathbb R)$. On overlaps these local models differ by left multiplication by the vector bundle transition function, so the charts are smoothly compatible and determine a unique smooth structure with these frame coordinates as charts. In these coordinates the projection $q$ is the first projection and the action $\nu\cdot A=\nu\circ A$ is right multiplication in the $GL_r(\mathbb R)$ factor, which proves the principal bundle axioms. [/proofplan]

[step:Use vector bundle charts to model frames by invertible matrices]Let $(U,\Phi)$ be a vector bundle chart for $E$, so $U\subset M$ is open and $\Phi:E|_U\to U\times \mathbb R^r$ is a smooth vector bundle isomorphism over $U$. Let $\operatorname{pr}_1:U\times\mathbb R^r\to U$ and $\operatorname{pr}_2:U\times\mathbb R^r\to\mathbb R^r$ denote the first and second coordinate projections, respectively. For each $p\in U$, define the fibrewise linear isomorphism \begin{align*} \Phi_p:E_p\to \mathbb R^r,\quad e\mapsto \operatorname{pr}_2(\Phi(e)). \end{align*} Define \begin{align*} \Psi_U:q^{-1}(U)\to U\times GL_r(\mathbb R),\quad \nu\mapsto (q(\nu),\Phi_{q(\nu)}\circ \nu). \end{align*} This is well-defined because if $\nu:\mathbb R^r\to E_p$ is a frame and $p=q(\nu)$, then $\Phi_p\circ\nu:\mathbb R^r\to\mathbb R^r$ is an invertible real [linear map](/page/Linear%20Map). The inverse map is \begin{align*} \Theta_U:U\times GL_r(\mathbb R)\to q^{-1}(U),\quad \Theta_U(p,A)=\Phi_p^{-1}\circ A, \end{align*} where $\Phi_p^{-1}:\mathbb R^r\to E_p$ is the inverse fibre isomorphism. For $\nu:\mathbb R^r\to E_p$ one has \begin{align*} \Theta_U(\Psi_U(\nu))=\Phi_p^{-1}\circ \Phi_p\circ \nu=\nu. \end{align*} For $(p,A)\in U\times GL_r(\mathbb R)$ one has \begin{align*} \Psi_U(\Theta_U(p,A))=(p,\Phi_p\circ\Phi_p^{-1}\circ A)=(p,A). \end{align*} Thus $\Psi_U$ is a bijection with inverse $\Theta_U$.[/step]

[guided]The purpose of a vector bundle chart is to replace each fibre $E_p$ over $U$ by the standard [vector space](/page/Vector%20Space) $\mathbb R^r$ in a smoothly varying way. Let $(U,\Phi)$ be such a chart, where $\Phi:E|_U\to U\times \mathbb R^r$ is a smooth vector bundle isomorphism over $U$. Let $\operatorname{pr}_1:U\times\mathbb R^r\to U$ and $\operatorname{pr}_2:U\times\mathbb R^r\to\mathbb R^r$ denote the first and second coordinate projections, respectively. For each $p\in U$, the chart restricts to a linear isomorphism on the fibre: \begin{align*} \Phi_p:E_p\to \mathbb R^r,\quad \Phi_p(e)=\operatorname{pr}_2(\Phi(e)). \end{align*} A point of $\operatorname{Fr}(E)$ [lying over](/theorems/2876) $p$ is a linear isomorphism $\nu:\mathbb R^r\to E_p$. Once the fibre $E_p$ is identified with $\mathbb R^r$ by $\Phi_p$, the frame $\nu$ becomes the invertible linear map $\Phi_p\circ\nu:\mathbb R^r\to\mathbb R^r$. This gives the local coordinate map \begin{align*} \Psi_U:q^{-1}(U)\to U\times GL_r(\mathbb R),\quad \nu\mapsto (q(\nu),\Phi_{q(\nu)}\circ \nu). \end{align*} The second component lies in $GL_r(\mathbb R)$ because it is the composite of two real linear isomorphisms. Conversely, given a point $p\in U$ and a matrix $A\in GL_r(\mathbb R)$, we recover a frame of $E_p$ by first applying $A:\mathbb R^r\to\mathbb R^r$ and then using the inverse fibre chart $\Phi_p^{-1}:\mathbb R^r\to E_p$. Thus define \begin{align*} \Theta_U:U\times GL_r(\mathbb R)\to q^{-1}(U),\quad \Theta_U(p,A)=\Phi_p^{-1}\circ A. \end{align*} These two constructions undo one another. If $\nu:\mathbb R^r\to E_p$, then \begin{align*} \Theta_U(\Psi_U(\nu))=\Phi_p^{-1}\circ \Phi_p\circ \nu=\nu. \end{align*} If $(p,A)\in U\times GL_r(\mathbb R)$, then \begin{align*} \Psi_U(\Theta_U(p,A))=(p,\Phi_p\circ\Phi_p^{-1}\circ A)=(p,A). \end{align*} So each vector bundle chart gives a bijective local description of $q^{-1}(U)$ as $U\times GL_r(\mathbb R)$.[/guided]

[step:Check that the local frame coordinates define a smooth manifold structure]Let $(U,\Phi)$ and $(V,\Phi')$ be vector bundle charts for $E$. For $p\in U\cap V$, define the vector bundle transition map \begin{align*} g_{\Phi'\Phi}:U\cap V\to GL_r(\mathbb R),\quad p\mapsto \Phi'_p\circ \Phi_p^{-1}. \end{align*} This map is smooth by the smoothness condition in the definition of a smooth vector bundle. Indeed, the coordinate expression of $\Phi'\circ\Phi^{-1}$ is a smooth map \begin{align*} F:(U\cap V)\times\mathbb R^r\to (U\cap V)\times\mathbb R^r \end{align*} of the form $F(p,v)=(p,H(p,v))$, where $H:(U\cap V)\times\mathbb R^r\to\mathbb R^r$ is smooth and each map $v\mapsto H(p,v)$ is linear. If $(e_1,\dots,e_r)$ denotes the standard basis of $\mathbb R^r$, then the matrix entries of $g_{\Phi'\Phi}$ are the component functions of the smooth maps $p\mapsto H(p,e_j)$, so $g_{\Phi'\Phi}:U\cap V\to GL_r(\mathbb R)$ is smooth. Define also \begin{align*} g_{\Phi\Phi'}:U\cap V\to GL_r(\mathbb R),\quad p\mapsto \Phi_p\circ (\Phi'_p)^{-1}. \end{align*} Then $g_{\Phi\Phi'}(p)=g_{\Phi'\Phi}(p)^{-1}$ for every $p\in U\cap V$. The overlap map between frame coordinates is \begin{align*} \Psi_V\circ\Psi_U^{-1}:(U\cap V)\times GL_r(\mathbb R)\to (U\cap V)\times GL_r(\mathbb R),\quad (\Psi_V\circ\Psi_U^{-1})(p,A)=(p,g_{\Phi'\Phi}(p)A). \end{align*} Matrix multiplication in $GL_r(\mathbb R)$ is smooth, and $g_{\Phi'\Phi}$ is smooth, so this overlap map is smooth. Its inverse is the smooth map \begin{align*} (p,B)\mapsto (p,g_{\Phi\Phi'}(p)B). \end{align*} Hence the frame coordinate bijections are smoothly compatible. The chart domains $q^{-1}(U_i)$ cover $\operatorname{Fr}(E)$ because the trivializing sets $U_i$ cover $M$, and each chart image is the open submanifold $U_i\times GL_r(\mathbb R)$ of $U_i\times \mathbb R^{r^2}$. By the standard atlas construction criterion in the definition of a smooth manifold, these compatible coordinate bijections define a smooth atlas once the induced topology is Hausdorff and second countable. Because $M$ is a smooth manifold, it is Hausdorff and second countable. Choose a countable vector bundle trivializing cover $(U_i,\Phi_i)_{i\in\mathbb N}$ of $M$, which exists because every vector bundle trivializing cover has a countable subcover on a second-countable manifold. For each $i\in\mathbb N$, let $\mathcal B_i$ be a countable basis for $U_i\times GL_r(\mathbb R)$. The family \begin{align*} \mathcal B:=\{\Psi_{U_i}^{-1}(B):i\in\mathbb N,\ B\in\mathcal B_i\} \end{align*} is countable. It is a basis for the atlas topology: if $W\subset\operatorname{Fr}(E)$ is open in the atlas topology and $\nu\in W$, choose $i$ with $\nu\in q^{-1}(U_i)$; then compatibility of the charts makes $W\cap q^{-1}(U_i)$ open in the $\Psi_{U_i}$-coordinates, so some $B\in\mathcal B_i$ satisfies $\Psi_{U_i}(\nu)\in B$ and $\Psi_{U_i}^{-1}(B)\subset W$. Thus the topology on $\operatorname{Fr}(E)$ is second countable. In this topology, $q$ is continuous because on each chart domain $q^{-1}(U_i)$ it is represented by the continuous projection $\operatorname{pr}_1:U_i\times GL_r(\mathbb R)\to U_i$. It is Hausdorff: if two frames lie over distinct points of $M$, separate their base points by disjoint open subsets of $M$ and use the continuity of $q$ to pull those subsets back to disjoint open neighborhoods in $\operatorname{Fr}(E)$; if they lie over the same point, use one frame chart over that point and separate their distinct coordinates in the [Hausdorff space](/page/Hausdorff%20Space) $U_i\times GL_r(\mathbb R)$. Therefore these compatible charts define a smooth manifold structure on $\operatorname{Fr}(E)$.[/step]

[guided]We must check two things before calling $\operatorname{Fr}(E)$ a smooth manifold: the coordinate changes must be smooth, and the topology defined by the coordinates must satisfy the manifold separation and countability axioms. First consider two vector bundle charts $(U,\Phi)$ and $(V,\Phi')$. For $p\in U\cap V$, define \begin{align*} g_{\Phi'\Phi}:U\cap V\to GL_r(\mathbb R),\quad g_{\Phi'\Phi}(p)=\Phi'_p\circ \Phi_p^{-1}. \end{align*} Why is this a smooth map into matrices? This is part of the compatibility requirement in the definition of a smooth vector bundle, but we spell out the coordinate verification. In the two bundle charts, the transition map is a smooth map \begin{align*} F:(U\cap V)\times\mathbb R^r\to (U\cap V)\times\mathbb R^r \end{align*} with $F(p,v)=(p,H(p,v))$, where $H$ is smooth and, for fixed $p$, the map $v\mapsto H(p,v)$ is linear. If $(e_1,\dots,e_r)$ is the standard basis of $\mathbb R^r$, then the $j$th column of the matrix of $g_{\Phi'\Phi}(p)$ is $H(p,e_j)$. Each map $p\mapsto H(p,e_j)$ is smooth because it is obtained by restricting the smooth map $H$ to the smooth constant section $p\mapsto (p,e_j)$. Thus all matrix entries of $g_{\Phi'\Phi}$ are smooth functions, so $g_{\Phi'\Phi}:U\cap V\to GL_r(\mathbb R)$ is smooth. We also name the reverse transition function explicitly: \begin{align*} g_{\Phi\Phi'}:U\cap V\to GL_r(\mathbb R),\quad g_{\Phi\Phi'}(p)=\Phi_p\circ (\Phi'_p)^{-1}. \end{align*} This satisfies $g_{\Phi\Phi'}(p)=g_{\Phi'\Phi}(p)^{-1}$ for every $p\in U\cap V$. Now compute the frame-coordinate overlap. If $(p,A)\in (U\cap V)\times GL_r(\mathbb R)$ represents the frame $\Phi_p^{-1}\circ A$, then applying the $V$-coordinates gives \begin{align*} (\Psi_V\circ\Psi_U^{-1})(p,A)=(p,\Phi'_p\circ\Phi_p^{-1}\circ A)=(p,g_{\Phi'\Phi}(p)A). \end{align*} This map is smooth because it is built from the smooth transition function $g_{\Phi'\Phi}$ and smooth matrix multiplication in $GL_r(\mathbb R)$. The inverse is \begin{align*} (p,B)\mapsto (p,g_{\Phi\Phi'}(p)B). \end{align*} Hence the frame charts are smoothly compatible. The domains $q^{-1}(U_i)$ cover $\operatorname{Fr}(E)$ because every frame lies over some point of $M$, and the trivializing sets $U_i$ cover $M$. The image of each chart is $U_i\times GL_r(\mathbb R)$, which is open in the model manifold $U_i\times \mathbb R^{r^2}$ because $GL_r(\mathbb R)$ is open in $\mathbb R^{r^2}$. Therefore the standard atlas construction criterion from the definition of a smooth manifold applies once we check Hausdorffness and second countability. It remains to verify the topological hypotheses in the definition of a smooth manifold. Since $M$ is a smooth manifold, it is second countable, and every open cover of $M$ has a countable subcover. Applying this to the cover by vector bundle trivializing neighborhoods, choose a countable trivializing cover $(U_i,\Phi_i)_{i\in\mathbb N}$. For each $i\in\mathbb N$, choose a countable basis $\mathcal B_i$ for the second-countable model space $U_i\times GL_r(\mathbb R)$. The countable family \begin{align*} \mathcal B:=\{\Psi_{U_i}^{-1}(B):i\in\mathbb N,\ B\in\mathcal B_i\} \end{align*} is a basis for the atlas topology. To see this, let $W\subset\operatorname{Fr}(E)$ be open in the atlas topology and let $\nu\in W$. Choose $i$ with $\nu\in q^{-1}(U_i)$. Since the charts are compatible, $W\cap q^{-1}(U_i)$ is open in the $\Psi_{U_i}$-coordinates. Therefore some $B\in\mathcal B_i$ contains $\Psi_{U_i}(\nu)$ and satisfies $\Psi_{U_i}^{-1}(B)\subset W$. Hence $\operatorname{Fr}(E)$ is second countable. Before using base-space separation, note that $q$ is continuous in this topology. On each chart domain $q^{-1}(U_i)$, the coordinate expression of $q$ is the first projection $\operatorname{pr}_1:U_i\times GL_r(\mathbb R)\to U_i$, which is continuous. Therefore the preimage under $q$ of any open subset of $M$ is open in $\operatorname{Fr}(E)$. For Hausdorffness, take two distinct frames. If they lie over distinct points of $M$, separate those base points by disjoint open subsets of $M$ and pull the separating neighborhoods back by the continuous map $q$. If they lie over the same point $p$, choose a trivializing chart $U_i$ containing $p$; the two frames have distinct images in the Hausdorff space $U_i\times GL_r(\mathbb R)$, so they have disjoint coordinate neighborhoods. Thus the atlas defines a Hausdorff, second-countable smooth manifold structure on $\operatorname{Fr}(E)$.[/guided]

[step:Prove uniqueness of the smooth structure determined by the frame coordinates] Suppose $\mathcal A$ and $\mathcal A'$ are two smooth atlases on the same set $\operatorname{Fr}(E)$ such that, for every vector bundle chart $(U,\Phi)$ used above, the corresponding map \begin{align*} \Psi_U:q^{-1}(U)\to U\times GL_r(\mathbb R),\quad \nu\mapsto (q(\nu),\Phi_{q(\nu)}\circ \nu) \end{align*} is a chart in both atlases. Since these frame-coordinate charts cover $\operatorname{Fr}(E)$, the identity map \begin{align*} \operatorname{id}: (\operatorname{Fr}(E),\mathcal A)\to (\operatorname{Fr}(E),\mathcal A') \end{align*} has local coordinate expression $\Psi_U\circ\operatorname{id}\circ\Psi_U^{-1}=\operatorname{id}_{U\times GL_r(\mathbb R)}$ on each such chart. This coordinate expression is smooth, and the same computation applies to the inverse identity map. Thus the two smooth structures are diffeomorphic by the identity map, so the smooth structure determined by the frame-coordinate atlas is unique. [/step]

[step:Show that the projection is locally the product projection]With the smooth structure just defined, each $\Psi_U:q^{-1}(U)\to U\times GL_r(\mathbb R)$ is a smooth chart. In this chart the map $q$ satisfies $\operatorname{pr}_1\circ \Psi_U(\nu)=q(\nu)$ for every $\nu\in q^{-1}(U)$, where $\operatorname{pr}_1:U\times GL_r(\mathbb R)\to U$ is the first projection. Therefore $q|_{q^{-1}(U)}=\operatorname{pr}_1\circ\Psi_U$, so $q$ is smooth and locally trivial with typical fibre $GL_r(\mathbb R)$.[/step]

[guided]The projection $q$ sends a frame to the point of $M$ over which that frame lives. In the coordinate chart $\Psi_U$, a frame $\nu:\mathbb R^r\to E_p$ is represented by the pair $(p,\Phi_p\circ\nu)$. Therefore applying the first projection $\operatorname{pr}_1:U\times GL_r(\mathbb R)\to U$ recovers exactly the base point: \begin{align*} \operatorname{pr}_1\circ \Psi_U(\nu)=q(\nu). \end{align*} Thus, on $q^{-1}(U)$, the map $q$ has coordinate expression $\operatorname{pr}_1$. Since projections from products of smooth manifolds are smooth, $q$ is smooth. The same identity also gives the local product form $q^{-1}(U)\cong U\times GL_r(\mathbb R)$ over $U$, so $q$ is locally trivial with typical fibre $GL_r(\mathbb R)$.[/guided]

[step:Identify the right action in local coordinates and verify the principal bundle axioms]Define the right action \begin{align*} \rho:\operatorname{Fr}(E)\times GL_r(\mathbb R)\to \operatorname{Fr}(E),\quad (\nu,A)\mapsto \nu\circ A. \end{align*} This is well-defined: if $\nu:\mathbb R^r\to E_p$ and $A:\mathbb R^r\to\mathbb R^r$ are real linear isomorphisms, then $\nu\circ A:\mathbb R^r\to E_p$ is again a frame over $p$. It is a right [group action](/page/Group%20Action) because for $A,B\in GL_r(\mathbb R)$, \begin{align*} (\nu\cdot A)\cdot B=(\nu\circ A)\circ B=\nu\circ(AB)=\nu\cdot(AB), \end{align*} and $\nu\cdot I_r=\nu\circ I_r=\nu$, where $I_r$ is the identity element of $GL_r(\mathbb R)$. In the local coordinates $\Psi_U$, the action is \begin{align*} \Psi_U((\nu\cdot A))=(q(\nu),\Phi_{q(\nu)}\circ\nu\circ A). \end{align*} If $\Psi_U(\nu)=(p,B)$, then $p=q(\nu)$ and $B=\Phi_p\circ\nu$, so \begin{align*} \Psi_U(\nu\cdot A)=(p,BA). \end{align*} Thus locally $\rho$ is the smooth map \begin{align*} U\times GL_r(\mathbb R)\times GL_r(\mathbb R)\to U\times GL_r(\mathbb R),\quad (p,B,A)\mapsto (p,BA). \end{align*} Therefore the action is smooth. The local trivializations $\Psi_U$ are $GL_r(\mathbb R)$-equivariant for the right action, since $\Psi_U(\nu\cdot A)=(p,BA)$ whenever $\Psi_U(\nu)=(p,B)$. Thus they are principal-bundle trivializations in the sense of the definition of a principal bundle. It remains to verify freeness and transitivity on each fibre. Fix $p\in M$. If $\nu\in q^{-1}(p)$ and $\nu\cdot A=\nu$, then $\nu\circ A=\nu$. Composing on the left with $\nu^{-1}:E_p\to\mathbb R^r$ gives $A=I_r$, so the action is free. If $\nu,\mu\in q^{-1}(p)$, then \begin{align*} A:=\nu^{-1}\circ\mu:\mathbb R^r\to\mathbb R^r \end{align*} is an element of $GL_r(\mathbb R)$, and \begin{align*} \nu\cdot A=\nu\circ\nu^{-1}\circ\mu=\mu. \end{align*} Thus the action is transitive on $q^{-1}(p)$. Hence $q:\operatorname{Fr}(E)\to M$ is a smooth principal $GL_r(\mathbb R)$-bundle.[/step]

[guided]The principal action must be smooth and must act freely and transitively on each fibre. Smoothness can be checked in the frame coordinates already constructed. Define \begin{align*} \rho:\operatorname{Fr}(E)\times GL_r(\mathbb R)\to \operatorname{Fr}(E),\quad (\nu,A)\mapsto \nu\circ A. \end{align*} If $\nu:\mathbb R^r\to E_p$ and $A:\mathbb R^r\to\mathbb R^r$ are real linear isomorphisms, then $\nu\circ A:\mathbb R^r\to E_p$ is again a frame over $p$, so $\rho$ is well-defined. The action laws follow from associativity of composition. For $A,B\in GL_r(\mathbb R)$, \begin{align*} (\nu\cdot A)\cdot B=(\nu\circ A)\circ B=\nu\circ(AB)=\nu\cdot(AB). \end{align*} Also $\nu\cdot I_r=\nu\circ I_r=\nu$, where $I_r$ is the identity element of $GL_r(\mathbb R)$. To prove smoothness, write the action in a frame chart. If $\Psi_U(\nu)=(p,B)$, then $p=q(\nu)$ and $B=\Phi_p\circ\nu$. Hence \begin{align*} \Psi_U(\nu\cdot A)=(p,\Phi_p\circ\nu\circ A)=(p,BA). \end{align*} Thus, in coordinates, the action is \begin{align*} U\times GL_r(\mathbb R)\times GL_r(\mathbb R)\to U\times GL_r(\mathbb R),\quad (p,B,A)\mapsto (p,BA), \end{align*} which is smooth because matrix multiplication in $GL_r(\mathbb R)$ is smooth. The local maps $\Psi_U$ are also compatible with the right action in the sense required by the definition of a principal bundle. Indeed, if $\Psi_U(\nu)=(p,B)$, then $\Psi_U(\nu\cdot A)=(p,BA)$, so the group acts by right multiplication on the $GL_r(\mathbb R)$ coordinate while leaving the base point fixed. Finally fix $p\in M$. If $\nu\in q^{-1}(p)$ and $\nu\cdot A=\nu$, then $\nu\circ A=\nu$. Composing on the left with the inverse linear map $\nu^{-1}:E_p\to\mathbb R^r$ gives $A=I_r$, so the action is free. If $\nu,\mu\in q^{-1}(p)$, define \begin{align*} A:=\nu^{-1}\circ\mu:\mathbb R^r\to\mathbb R^r. \end{align*} This is an element of $GL_r(\mathbb R)$, and \begin{align*} \nu\cdot A=\nu\circ\nu^{-1}\circ\mu=\mu. \end{align*} So the action is transitive on each fibre. Therefore $q:\operatorname{Fr}(E)\to M$ with this right action satisfies the principal $GL_r(\mathbb R)$-bundle axioms.[/guided]