The key observation is to recall that trivialisations of vector bundles are fibrewise linear, and so you can prove an analogous result to result 2 for certain mappings of the form $A \circ u.$

Given the above setup, suppose $\psi_j : E|_{U_i} \rightarrow U_i \times \mathbb R^s$ is another choice of trivialisation for each $i.$ Then the composition, $$ \varphi_i \circ \psi_i^{-1} : U_i \times \mathbb R^s \longrightarrow U_i \times \mathbb R^s $$ maps $(x,v) \mapsto (x,A_i(x)v),$ where $A_i : U_i \rightarrow \mathrm{GL}(s,\mathbb R).$ By shrinking $U_i$ slightly if necessary and identifying $\mathrm{GL}(s,\mathbb R) \subset \mathbb R^{s^2},$ we can assume that $A_i \circ h_i^{-1}, A_i^{-1} \circ h_i^{-1}$ are bounded in $C^k(\mathbb R^n, \mathbb R^{s^2}).$

We want to show there is $C>0$ such that, $$ \lVert (\mu_j \circ h_j^{-1})(\varphi_j \circ u \circ h_j^{-1})\rVert_k^2 \leq C \lVert (\mu_j \circ h_j^{-1})(\psi_j \circ u \circ h_j^{-1})\rVert_k^2. $$ For this we write, \begin{align*} \lVert (\mu_j \circ h_j^{-1})(\varphi_j \circ u \circ h_j^{-1})\rVert_k^2 &= \lVert (\mu_j \circ h_j^{-1})(\varphi_j \circ \psi_j^{-1} \circ \psi_j \circ u \circ h_j^{-1}) \rVert_k^2 \\ &= \lVert(\mu_j \circ h_j^{-1}) (\mathrm{id},A_j \circ h_j^{-1})(\psi_j \circ u \circ h_j^{-1}) \rVert_k^2 \\ &\leq C \left(1+\lVert A_j \circ h_j^{-1} \rVert_{C^k(\mathbb R^n,\mathbb R^{s^2})}\right) \lVert(\mu_j \circ h_j^{-1})(\psi_j \circ u \circ h_j^{-1}) \rVert_k^2 \end{align*} The last line requires checking; the idea is to expand out each $\nabla^m\left( (\mathrm{id},A_j \circ h_j^{-1}) \psi \circ u \circ h_j^{-1}\right)$ and prove the estimate pointwise. Interchanging $\varphi_j$ and $\psi_j$ establishes the equivalence.

From here you've done most of the work. The rest is mostly a matter of notation and putting everything together.


If you are familiar with pseudodifferential operators, you may want to look at Proposition 7.3 in Shubin's book Pseudodifferential Operators and Spectral Theory.

Shubin defines two different Sobolev norms $\Vert \cdot \Vert_s$ and $\Vert \cdot \Vert_s'$, where the first is the same as yours (depending on the choice of charts, frames and partitions of unity) and the second depends on the choice of certain pseudodifferential operators.

He then proves for each norm independently that it is complete on the Sobolev space $H^s$ and uses the open mapping theorem to conclude that they are equivalent. In particular the induced topology is the same in each case and thus it does not depend on either choice.