[proofplan] We prove smoothness locally. Around an arbitrary point, choose a smooth frame of $E$ adapted to the subbundle $F$, then apply the fibrewise Gram-Schmidt construction with respect to the smooth metric $g$. The resulting orthonormal frame is smooth, its first $r$ vectors still span $F$, and its remaining vectors form a smooth local frame for $F^\perp$. The direct sum decomposition is then the corresponding finite-dimensional [orthogonal decomposition](/theorems/436) in each fibre. [/proofplan]

[step:Choose a local frame adapted to the subbundle $F$] Fix $p_0\in M$. Since $F\subset E$ is a smooth vector subbundle of rank $r$, there is an open neighbourhood $U\subset M$ of $p_0$ and smooth sections \begin{align*} s_i:U&\to E|_U \end{align*} for $1\le i\le k$ such that, for every $p\in U$, the list $(s_1(p),\dots,s_k(p))$ is a basis of $E_p$ and the list $(s_1(p),\dots,s_r(p))$ is a basis of $F_p$. For $1\le i,j\le k$, define the smooth coefficient function $g_{ij}:U\to \mathbb{R}$ by sending $p\in U$ to $g_p(s_i(p),s_j(p))$. The smoothness of $g_{ij}$ follows from the smoothness of the fibre metric $g$ and of the sections $s_i,s_j$. [/step]

[step:Apply fibrewise Gram-Schmidt without losing smoothness]We recursively define smooth sections \begin{align*} u_j:U&\to E|_U, & e_j:U&\to E|_U \end{align*} for $1\le j\le k$. Set $u_1:=s_1$ and \begin{align*} e_1(p):=\frac{u_1(p)}{\sqrt{g_p(u_1(p),u_1(p))}}. \end{align*} For $2\le j\le k$, after $e_1,\dots,e_{j-1}$ have been defined, set \begin{align*} u_j(p):=s_j(p)-\sum_{\ell=1}^{j-1}g_p(s_j(p),e_\ell(p))e_\ell(p), \end{align*} and then \begin{align*} e_j(p):=\frac{u_j(p)}{\sqrt{g_p(u_j(p),u_j(p))}}. \end{align*} We prove by induction on $j$ that these formulas define smooth sections and that, for every $p\in U$, the list $(e_1(p),\dots,e_j(p))$ is an [orthonormal basis](/page/Orthonormal%20Basis) of $\operatorname{span}\{s_1(p),\dots,s_j(p)\}$. For $j=1$, the section $u_1=s_1$ is nowhere zero because $s_1(p)$ is part of a basis of $E_p$. Hence $p\mapsto g_p(u_1(p),u_1(p))$ is a positive smooth function, so division by its square root preserves smoothness. The normalized vector $e_1(p)$ has $g_p(e_1(p),e_1(p))=1$ and spans the same line as $s_1(p)$. Assume the statement holds up to $j-1$. The section $u_j$ is smooth because it is obtained from smooth sections by addition, scalar multiplication by the smooth functions $p\mapsto g_p(s_j(p),e_\ell(p))$, and finite summation. For each $p\in U$, the vector $u_j(p)$ is the vector obtained from $s_j(p)$ by subtracting its [orthogonal projection](/theorems/437) onto $\operatorname{span}\{e_1(p),\dots,e_{j-1}(p)\}=\operatorname{span}\{s_1(p),\dots,s_{j-1}(p)\}$. Since $(s_1(p),\dots,s_j(p))$ is linearly independent, $s_j(p)$ is not in that span, so $u_j(p)\ne 0$. Therefore $p\mapsto g_p(u_j(p),u_j(p))$ is a positive smooth function, and $e_j$ is smooth. The construction gives $g_p(e_j(p),e_\ell(p))=0$ for $\ell<j$ and $g_p(e_j(p),e_j(p))=1$, so $(e_1(p),\dots,e_j(p))$ is orthonormal and spans the same subspace as $(s_1(p),\dots,s_j(p))$. In particular, for every $p\in U$, the list $(e_1(p),\dots,e_k(p))$ is an orthonormal basis of $E_p$, and the list $(e_1(p),\dots,e_r(p))$ is an orthonormal basis of $F_p$.[/step]

[guided]The purpose of this step is to replace the adapted frame $(s_1,\dots,s_k)$ by an adapted orthonormal frame. The point requiring verification is smoothness: Gram-Schmidt is performed separately in each fibre, so we must check that the resulting fibrewise formulas vary smoothly with the base point $p\in U$. We define smooth sections $u_j:U\to E|_U$ and $e_j:U\to E|_U$ recursively. First set $u_1:=s_1$. Since $s_1(p)$ is part of a basis of $E_p$ for every $p\in U$, it is nowhere zero. Because $g_p$ is positive definite on $E_p$, the function $h_1:U\to \mathbb{R}$ defined by $h_1(p):=g_p(u_1(p),u_1(p))$ is smooth and satisfies $h_1(p)>0$ for every $p\in U$. Hence $\sqrt{h_1}$ is a positive smooth function, and we may define \begin{align*} e_1(p):=\frac{u_1(p)}{\sqrt{h_1(p)}}. \end{align*} Then $e_1$ is smooth, $g_p(e_1(p),e_1(p))=1$, and $e_1(p)$ spans the same one-dimensional subspace as $s_1(p)$. Now suppose $e_1,\dots,e_{j-1}$ have been constructed as smooth sections and form, in each fibre $E_p$, an orthonormal basis of $\operatorname{span}\{s_1(p),\dots,s_{j-1}(p)\}$. Define \begin{align*} u_j(p):=s_j(p)-\sum_{\ell=1}^{j-1}g_p(s_j(p),e_\ell(p))e_\ell(p). \end{align*} This is the Gram-Schmidt subtraction step: from $s_j(p)$ we subtract its components in the already constructed orthonormal directions. Each coefficient $a_{j\ell}:U\to \mathbb{R}$ defined by $a_{j\ell}(p):=g_p(s_j(p),e_\ell(p))$ is smooth because $g$ and the sections $s_j,e_\ell$ are smooth. Therefore $u_j$ is a smooth section. We next check that the denominator used to normalize $u_j$ is never zero. If $u_j(p)=0$, then \begin{align*} s_j(p)=\sum_{\ell=1}^{j-1}g_p(s_j(p),e_\ell(p))e_\ell(p), \end{align*} so $s_j(p)$ lies in $\operatorname{span}\{e_1(p),\dots,e_{j-1}(p)\}$. By the induction hypothesis, this equals $\operatorname{span}\{s_1(p),\dots,s_{j-1}(p)\}$, contradicting the [linear independence](/page/Linear%20Independence) of $(s_1(p),\dots,s_j(p))$. Thus $u_j(p)\ne 0$ for every $p\in U$. The function $h_j:U\to \mathbb{R}$ defined by $h_j(p):=g_p(u_j(p),u_j(p))$ is therefore positive and smooth, so \begin{align*} e_j(p):=\frac{u_j(p)}{\sqrt{h_j(p)}} \end{align*} defines a smooth section. Finally, fix $\ell<j$. By the orthonormality of $e_1(p),\dots,e_{j-1}(p)$, the sum \begin{align*} \sum_{m=1}^{j-1}g_p(s_j(p),e_m(p))g_p(e_m(p),e_\ell(p)) \end{align*} has only one nonzero term, namely the term $m=\ell$, and therefore equals $g_p(s_j(p),e_\ell(p))$. Hence $g_p(u_j(p),e_\ell(p))=0$. After normalization, $g_p(e_j(p),e_\ell(p))=0$ for $\ell<j$ and $g_p(e_j(p),e_j(p))=1$. Thus the induction produces a smooth orthonormal frame $(e_1,\dots,e_k)$ of $E|_U$. Since the first $r$ Gram-Schmidt vectors are constructed only from $s_1,\dots,s_r$, the list $(e_1(p),\dots,e_r(p))$ spans the same subspace as $(s_1(p),\dots,s_r(p))$, namely $F_p$.[/guided]

[step:Use the remaining orthonormal vectors as a local frame for $F^\perp$] For $r+1\le j\le k$, the section $e_j:U\to E|_U$ takes values in $F^\perp|_U$. Indeed, if $p\in U$ and $w\in F_p$, then there are unique scalars $b_1,\dots,b_r\in\mathbb{R}$ such that \begin{align*} w=\sum_{i=1}^{r}b_i e_i(p). \end{align*} For $j>r$, orthonormality gives \begin{align*} g_p(e_j(p),w) =\sum_{i=1}^{r}b_i g_p(e_j(p),e_i(p)) =0. \end{align*} Thus $e_j(p)\in F_p^\perp$. Conversely, let $v\in F_p^\perp$. Since $(e_1(p),\dots,e_k(p))$ is a basis of $E_p$, there are unique scalars $a_1,\dots,a_k\in\mathbb{R}$ such that \begin{align*} v=\sum_{j=1}^{k}a_j e_j(p). \end{align*} For each $1\le i\le r$, using $e_i(p)\in F_p$ and $v\in F_p^\perp$ gives \begin{align*} 0=g_p(v,e_i(p)) =\sum_{j=1}^{k}a_j g_p(e_j(p),e_i(p)) =a_i. \end{align*} Hence \begin{align*} v=\sum_{j=r+1}^{k}a_j e_j(p). \end{align*} Therefore $(e_{r+1}(p),\dots,e_k(p))$ is a basis of $F_p^\perp$ for every $p\in U$. Since the sections $e_{r+1},\dots,e_k$ are smooth and form a local frame for $F^\perp|_U$, the subset $F^\perp\subset E$ is a smooth vector subbundle over $U$ of rank $k-r$. Because $p_0\in M$ was arbitrary, these local frames cover $M$, so $F^\perp$ is a smooth vector subbundle of $E$. [/step]

[step:Recover the fibrewise direct sum decomposition] Fix $p\in M$. Choose a neighbourhood $U$ of $p$ and the orthonormal frame constructed above. The basis \begin{align*} (e_1(p),\dots,e_k(p)) \end{align*} splits into a basis $(e_1(p),\dots,e_r(p))$ of $F_p$ and a basis $(e_{r+1}(p),\dots,e_k(p))$ of $F_p^\perp$. Hence every $v\in E_p$ has a unique expression \begin{align*} v=\sum_{i=1}^{r}a_i e_i(p)+\sum_{j=r+1}^{k}a_j e_j(p), \end{align*} with the first summand in $F_p$ and the second summand in $F_p^\perp$. The intersection is zero: if $v\in F_p\cap F_p^\perp$, then $g_p(v,v)=0$ because $v\in F_p^\perp$ and $v\in F_p$; since $g_p$ is positive definite, this implies $v=0$. Therefore \begin{align*} E_p=F_p\oplus F_p^\perp. \end{align*} Since $p\in M$ was arbitrary, the decomposition holds in every fibre. [/step]