Subject to my question a few days ago, I am trying to show that for an embeddable vector bundle $E \hookrightarrow M \times \mathbb{R}^n$, the direct sum with its orthogonal complement is trivial, i.e. that $E \oplus E^\bot \cong M \times \mathbb{R}^n$.
I've used the map $f$ defined fibrewise as $f|_x (v,u) = v+u$. I can show that this is a fibrewise-isomorphism, but I cannot show that it is smooth, and thus cannot show that $f$ is a bundle isomorphism.
I know that from my linked question that I can appeal to the locality of smoothness. We want to show that for any point $(v,u)$ in the bundle, there is a chart $(U, \Psi)$ at $(v,u)$ and a chart $(V,\Phi)$ at $v+u$ such that the coordinate expression of $f$, i.e. $\Phi \circ f \circ \Psi^{-1}$ is a smooth map between Euclidean spaces.
I think the best way to try and express $f$ in local coordinates is to use local trivialisations - let $(v,u) \in E \oplus E^\bot$, and use a local trivialisation $(U , \Psi)$ around the point $x\in M$ such that $(v,u) \in E_x \oplus E_x^\bot$. Our chart on the trivial bundle can just be the open set $U \times \mathbb{R}^n$ with the identity map. Suppose that $\Psi(v,u) = (x,r)$, where $r \in \mathbb{R}^n$. If we decompose the map $\Psi^{-1}$ into $\Psi^{-1} = (\Psi_1^{-1},\Psi_2^{-1})$, the local expression of $f$ becomes $f \circ \Psi^{-1}: U \times \mathbb{R}^n \rightarrow U \times \mathbb{R}^n$ given by $(x,r) \mapsto (x, \Psi_1^{-1}(r) + \Psi_2^{-1}(r))$.
To show that this is smooth I think that I can wave my hands and say that $\Psi^{-1}$ is smooth iff both it's components $\Psi_1^{-1}$ and $\Psi_2^{-1}$ are smooth. Then we can use the fact that $\Psi$ is a diffeomorphism to conclude that its components are smooth and, since addition of smooth maps is also smooth, that the map $f \circ \Psi^{-1}$ is also smooth.
Is this correct reasoning? It seems ok but I am unconfident in this type of proof.