[proofplan] We construct the two assignments explicitly. Starting from a smooth fibre metric, we show that the frames orthonormal for that metric form a smooth principal $O(n)$-subbundle by writing them in a local frame and using the smooth positive-definite matrix of the metric. Starting from an $O(n)$-reduction, we define the metric by transporting the Euclidean [inner product](/page/Inner%20Product) along any reduced frame, check that this is independent of the chosen frame, and prove smoothness using local sections of the principal $O(n)$-bundle. Finally, we verify that the two constructions undo each other fibrewise. [/proofplan]

[step:Fix the frame bundle conventions and the orthogonal action] Let $\langle \cdot,\cdot\rangle_0: \mathbb{R}^n \times \mathbb{R}^n \to \mathbb{R}$ denote the standard Euclidean inner product. The frame bundle $\operatorname{Fr}(E)$ is the smooth principal $GL_n(\mathbb{R})$-bundle whose fibre over $x \in M$ is \begin{align*} \operatorname{Fr}(E)_x = \{u: \mathbb{R}^n \to E_x : u \text{ is a linear isomorphism}\}. \end{align*} The right action of $GL_n(\mathbb{R})$ is the smooth map \begin{align*} \operatorname{Fr}(E) \times GL_n(\mathbb{R}) \to \operatorname{Fr}(E), \quad (u,A) \mapsto u \cdot A := u \circ A. \end{align*} The orthogonal group is \begin{align*} O(n) := \{A \in GL_n(\mathbb{R}) : \langle Aa, Ab\rangle_0 = \langle a,b\rangle_0 \text{ for all } a,b \in \mathbb{R}^n\}. \end{align*} Thus a principal $O(n)$-subbundle $Q \subset \operatorname{Fr}(E)$ means a smooth submanifold $Q$ over $M$ such that each fibre $Q_x := Q \cap \operatorname{Fr}(E)_x$ is preserved freely and transitively by the restricted right action of $O(n)$. [/step]

[step:Construct the orthonormal frame reduction from a fibre metric]Let $g$ be a smooth fibre metric on $E$. Define \begin{align*} \operatorname{Fr}_g(E) := \{u \in \operatorname{Fr}(E) : g_{\pi(u)}(u(a),u(b)) = \langle a,b\rangle_0 \text{ for all } a,b \in \mathbb{R}^n\}. \end{align*} For $A \in O(n)$ and $u \in \operatorname{Fr}_g(E)$, we have \begin{align*} g_{\pi(u)}((u \cdot A)(a),(u \cdot A)(b)) = g_{\pi(u)}(u(Aa),u(Ab)) = \langle Aa,Ab\rangle_0 = \langle a,b\rangle_0. \end{align*} Hence $\operatorname{Fr}_g(E)$ is stable under the right action of $O(n)$. We next prove that it is a smooth principal $O(n)$-subbundle. Let $U \subset M$ be an [open set](/page/Open%20Set) over which $E$ admits a smooth local frame $e_1,\dots,e_n$, where each \begin{align*} e_i: U \to E \end{align*} is a smooth section and $e_1(x),\dots,e_n(x)$ is a basis of $E_x$ for every $x \in U$. Define the smooth matrix-valued map \begin{align*} G: U \to \operatorname{Sym}^+_n(\mathbb{R}) \end{align*} by \begin{align*} G(x)_{ij} := g_x(e_i(x),e_j(x)), \end{align*} where $\operatorname{Sym}^+_n(\mathbb{R})$ denotes the open subset of symmetric positive-definite matrices in the [vector space](/page/Vector%20Space) of real symmetric $n \times n$ matrices. Let $S: \operatorname{Sym}^+_n(\mathbb{R}) \to \operatorname{Sym}^+_n(\mathbb{R})$ be the map assigning to a positive-definite matrix $B$ its unique positive-definite square root $S(B)$ satisfying $S(B)^2 = B$. The map $S$ is smooth on $\operatorname{Sym}^+_n(\mathbb{R})$: the scalar function $t \mapsto \sqrt{t}$ is smooth on the open set $(0,\infty)$, every matrix in $\operatorname{Sym}^+_n(\mathbb{R})$ is symmetric with spectrum contained in $(0,\infty)$, and the smooth functional calculus for symmetric matrices applies to smooth functions on an open neighbourhood of the spectrum. Define \begin{align*} R: U \to GL_n(\mathbb{R}) \end{align*} by $R(x) := S(G(x))^{-1}$. For $A \in O(n)$, define the frame \begin{align*} u_{x,A}: \mathbb{R}^n \to E_x \end{align*} by \begin{align*} u_{x,A}(a) := \sum_{i=1}^n e_i(x)\,(R(x)A a)_i. \end{align*} For $a,b \in \mathbb{R}^n$, matrix multiplication gives \begin{align*} g_x(u_{x,A}(a),u_{x,A}(b)) = a^\top A^\top R(x)^\top G(x)R(x)A b. \end{align*} Since $R(x)^\top G(x)R(x)=I_n$ and $A^\top A=I_n$, this equals $a^\top b=\langle a,b\rangle_0$. Therefore $u_{x,A} \in \operatorname{Fr}_g(E)_x$. Conversely, if $u \in \operatorname{Fr}_g(E)_x$, write $u(a)=\sum_{i=1}^n e_i(x)(B a)_i$ for a unique $B \in GL_n(\mathbb{R})$. The orthonormality condition says $B^\top G(x)B=I_n$. Hence $S(G(x))B \in O(n)$, and therefore $B=R(x)A$ for the orthogonal matrix $A:=S(G(x))B$. Thus every $g$-orthonormal frame over $U$ is uniquely of the form $u_{x,A}$ with $A \in O(n)$. The map \begin{align*} U \times O(n) \to \operatorname{Fr}_g(E)|_U, \quad (x,A) \mapsto u_{x,A} \end{align*} is a smooth bijection with smooth inverse obtained by expressing a frame in the local frame $e_1,\dots,e_n$ and multiplying by $S(G(x))$. It is $O(n)$-equivariant for the right action. Hence $\operatorname{Fr}_g(E)$ is a smooth principal $O(n)$-subbundle of $\operatorname{Fr}(E)$.[/step]

[guided]We want to prove more than set-theoretic existence: the orthonormal frames must vary smoothly with the base point. The right way to see this is to use an arbitrary smooth local frame and then correct it by a smooth positive-definite matrix. Let $U \subset M$ be an open set over which $E$ has a smooth local frame $e_1,\dots,e_n$. This means that each $e_i: U \to E$ is a smooth section and that $e_1(x),\dots,e_n(x)$ is a basis of $E_x$ for every $x \in U$. The metric $g$ is smooth, so the matrix of its fibrewise inner product in this frame is the smooth map \begin{align*} G: U \to \operatorname{Sym}^+_n(\mathbb{R}) \end{align*} defined by \begin{align*} G(x)_{ij} := g_x(e_i(x),e_j(x)). \end{align*} The target is $\operatorname{Sym}^+_n(\mathbb{R})$ because each $g_x$ is a positive-definite symmetric [bilinear form](/page/Bilinear%20Form). The problem is now a finite-dimensional linear algebra problem depending smoothly on $x$: given the positive-definite matrix $G(x)$, find all matrices $B \in GL_n(\mathbb{R})$ such that the frame with columns $e_i(x)B_{ij}$ is orthonormal. That condition is exactly \begin{align*} B^\top G(x)B = I_n. \end{align*} Let $S: \operatorname{Sym}^+_n(\mathbb{R}) \to \operatorname{Sym}^+_n(\mathbb{R})$ denote the positive-definite square-root map, so $S(B)^2=B$ for every positive-definite matrix $B$. We use smooth functional calculus for symmetric matrices. Its hypotheses are satisfied here because $t \mapsto \sqrt{t}$ is smooth on the open set $(0,\infty)$ and every matrix in $\operatorname{Sym}^+_n(\mathbb{R})$ is symmetric with spectrum contained in $(0,\infty)$. Therefore $S$ depends smoothly on the positive-definite matrix. Define \begin{align*} R: U \to GL_n(\mathbb{R}) \end{align*} by $R(x):=S(G(x))^{-1}$. Since $S(G(x))$ is symmetric and positive-definite, $R(x)^\top G(x)R(x)=I_n$. Now take $A \in O(n)$ and define \begin{align*} u_{x,A}: \mathbb{R}^n \to E_x \end{align*} by \begin{align*} u_{x,A}(a) := \sum_{i=1}^n e_i(x)\,(R(x)A a)_i. \end{align*} This is a linear isomorphism because $R(x)A \in GL_n(\mathbb{R})$. For $a,b \in \mathbb{R}^n$, the matrix formula for the metric in the frame $e_1,\dots,e_n$ gives \begin{align*} g_x(u_{x,A}(a),u_{x,A}(b)) = a^\top A^\top R(x)^\top G(x)R(x)A b. \end{align*} Using $R(x)^\top G(x)R(x)=I_n$ and $A^\top A=I_n$, this becomes \begin{align*} g_x(u_{x,A}(a),u_{x,A}(b)) = a^\top b = \langle a,b\rangle_0. \end{align*} Thus $u_{x,A}$ is a $g$-orthonormal frame. Conversely, suppose $u \in \operatorname{Fr}_g(E)_x$. Since $e_1(x),\dots,e_n(x)$ is a basis of $E_x$, there is a unique matrix $B \in GL_n(\mathbb{R})$ such that \begin{align*} u(a)=\sum_{i=1}^n e_i(x)(Ba)_i. \end{align*} The assumption that $u$ is $g$-orthonormal says $B^\top G(x)B=I_n$. Multiplying this identity by $S(G(x))$ on the left and right shows that $S(G(x))B$ is orthogonal. If we define $A:=S(G(x))B$, then $A \in O(n)$ and $B=R(x)A$. Therefore every orthonormal frame over $U$ has the form $u_{x,A}$ for a unique $A \in O(n)$. This gives a local trivialization \begin{align*} U \times O(n) \to \operatorname{Fr}_g(E)|_U, \quad (x,A) \mapsto u_{x,A}. \end{align*} The map is smooth because $e_i$, $G$, the square-root map $S$, matrix inversion, and matrix multiplication are smooth on their domains. Its inverse is smooth because it is obtained by writing the frame in the smooth local frame $e_1,\dots,e_n$ to get $B$, then forming $A=S(G(x))B$. The right action of $O(n)$ corresponds to multiplication in the second factor, so this local model proves that $\operatorname{Fr}_g(E)$ is a smooth principal $O(n)$-subbundle of $\operatorname{Fr}(E)$.[/guided]

[step:Recover all frames by extending the structure group] For each $x \in M$, every frame $u \in \operatorname{Fr}(E)_x$ can be written as $u=q\cdot A$ with $q \in \operatorname{Fr}_g(E)_x$ and $A \in GL_n(\mathbb{R})$. Indeed, choose any $q \in \operatorname{Fr}_g(E)_x$, and set $A:=q^{-1}\circ u$, viewed as an element of $GL_n(\mathbb{R})$. Then $u=q\circ A=q\cdot A$. Thus the canonical associated bundle map \begin{align*} \operatorname{Fr}_g(E)\times_{O(n)} GL_n(\mathbb{R}) \to \operatorname{Fr}(E), \quad [q,A] \mapsto q\cdot A \end{align*} is fibrewise surjective. It is also fibrewise injective because $q\cdot A=q'\cdot A'$ implies $q'=q\cdot H$ for a unique $H\in O(n)$ and then $A'=H^{-1}A$, which is precisely the [equivalence relation](/page/Equivalence%20Relation) defining the associated bundle. The map is smooth because it is induced by the smooth right action of $GL_n(\mathbb{R})$ on $\operatorname{Fr}(E)$, and in the local trivializations constructed above it is the standard smooth map on $U \times GL_n(\mathbb{R})$. Its inverse is smooth in the same local coordinates, where a frame is expressed relative to a reduced frame and the resulting transition function is a smooth $GL_n(\mathbb{R})$-valued map. Hence the canonical associated bundle map is a smooth principal $GL_n(\mathbb{R})$-bundle isomorphism, so extending the structure group of $\operatorname{Fr}_g(E)$ from $O(n)$ to $GL_n(\mathbb{R})$ recovers $\operatorname{Fr}(E)$. [/step]

[step:Construct a fibre metric from an orthogonal reduction] Let $Q \subset \operatorname{Fr}(E)$ be a smooth principal $O(n)$-subbundle. For $x \in M$, choose $u \in Q_x$. Define the bilinear form $g^Q_x:E_x\times E_x\to\mathbb R$ as follows. For $v,w \in E_x$, define $a:=u^{-1}(v)$ and $b:=u^{-1}(w)$ in $\mathbb{R}^n$, and set \begin{align*} g^Q_x(v,w) := \langle a,b\rangle_0. \end{align*} This defines a symmetric positive-definite bilinear form on $E_x$ because $u: \mathbb{R}^n \to E_x$ is a linear isomorphism and $\langle \cdot,\cdot\rangle_0$ is a symmetric positive-definite bilinear form. The definition is independent of the chosen frame in $Q_x$. If $u,u' \in Q_x$, then the principal $O(n)$-action on $Q_x$ is transitive, so there is a unique $A \in O(n)$ such that $u'=u\cdot A=u\circ A$. For $v,w \in E_x$, define $a:=u^{-1}(v)$ and $b:=u^{-1}(w)$. Then $(u')^{-1}(v)=A^{-1}a$ and $(u')^{-1}(w)=A^{-1}b$. Since $A^{-1}\in O(n)$, orthogonality gives \begin{align*} \langle A^{-1}a,A^{-1}b\rangle_0=\langle a,b\rangle_0. \end{align*} Thus $g^Q_x(v,w)$ is independent of $u$. It remains to prove smoothness. Let $U \subset M$ be an open set admitting a smooth local section \begin{align*} s: U \to Q. \end{align*} Such sections exist after replacing $U$ by a principal-bundle trivialising neighbourhood, because local triviality of the smooth principal bundle $Q \to M$ identifies $Q|_U$ with $U \times O(n)$ and the constant identity element of $O(n)$ gives a smooth section. For each $x \in U$, the frame $s(x):\mathbb{R}^n \to E_x$ gives smooth local sections \begin{align*} e_i: U \to E \end{align*} by $e_i(x):=s(x)(\varepsilon_i)$, where $\varepsilon_1,\dots,\varepsilon_n$ is the standard basis of $\mathbb{R}^n$. By construction, \begin{align*} g^Q_x(e_i(x),e_j(x))=\langle \varepsilon_i,\varepsilon_j\rangle_0=\delta_{ij}. \end{align*} Therefore the matrix of $g^Q$ in the smooth local frame $e_1,\dots,e_n$ is the constant identity matrix. Hence $g^Q$ is a smooth fibre metric on $E$. [/step]

[step:Verify that the two constructions are inverse] Let $g$ be a smooth fibre metric. Construct $Q=\operatorname{Fr}_g(E)$ and then construct $g^Q$. For $x \in M$ and $v,w \in E_x$, choose $u \in \operatorname{Fr}_g(E)_x$. Let $a:=u^{-1}(v)$ and $b:=u^{-1}(w)$. Since $u$ is a $g$-isometry, \begin{align*} g^Q_x(v,w)=\langle a,b\rangle_0=g_x(u(a),u(b))=g_x(v,w). \end{align*} Thus $g^Q=g$. Conversely, let $Q \subset \operatorname{Fr}(E)$ be a smooth principal $O(n)$-subbundle, construct $g^Q$, and then form $\operatorname{Fr}_{g^Q}(E)$. If $u \in Q_x$, then by definition of $g^Q_x$ the map $u:(\mathbb{R}^n,\langle\cdot,\cdot\rangle_0)\to(E_x,g^Q_x)$ is an isometry, so $Q \subset \operatorname{Fr}_{g^Q}(E)$. For the reverse inclusion, let $u \in \operatorname{Fr}_{g^Q}(E)_x$ and choose $q \in Q_x$. Since $q$ is also a $g^Q_x$-orthonormal frame, the [linear map](/page/Linear%20Map) $A:=q^{-1}\circ u$ preserves $\langle\cdot,\cdot\rangle_0$, hence $A\in O(n)$. Therefore $u=q\cdot A\in Q_x$ because $Q_x$ is stable under the right action of $O(n)$. Hence $\operatorname{Fr}_{g^Q}(E)=Q$. The assignments $g \mapsto \operatorname{Fr}_g(E)$ and $Q \mapsto g^Q$ are therefore mutually inverse, giving the claimed natural bijection between smooth fibre metrics on $E$ and $O(n)$-reductions of $\operatorname{Fr}(E)$. [/step]