Associated vector bundles are well-defined

Let $s_i:U_i\to P$ be the smooth section defined by a principal trivialization. Every $p\in {\pi }^{-1}(U_i)$ has a unique expression $p=s_i(x)h$. Define ${\mathrm{\Phi }}_i:r^{-1}(U_i)\to U_i\times V,{\mathrm{\Phi }}_i([s_i(x)h,v])=(x,\rho (h)v)\mathrm{.}$ This is independent of representatives: replacing $(s_i(x)h,v)$ by $(s_i(x)hk,\rho (k{)}^{-1}v)$ leaves $\rho (hk)\rho (k{)}^{-1}v=\rho (h)v$. It is bijective, with inverse $(x,w)\mapsto [s_i(x),w]$.

Let $Q:P\times V\to P{\times }_{H}V$ be the quotient map. It is open because the saturation of an open set is the union of its translates under the diagonal action, each a homeomorphism. The composite ${\mathrm{\Phi }}_i\circ Q$ on ${\pi }^{-1}(U_i)\times V$ is, in principal coordinates $(x,h,v)$, $(x,h,v)\mapsto (x,\rho (h)v)$; it is continuous and constant on orbits, while the displayed inverse in step 1.1 is continuous after composing with $Q$. Hence ${\mathrm{\Phi }}_i$ is a homeomorphism.

On $U_i\cap U_j$, define the smooth map $g_{ji}$ by $s_i(x)=s_j(x)g_{ji}(x)$; it is the group coordinate in a principal trivialization. Then ${\mathrm{\Phi }}_j{\mathrm{\Phi }}_i^{-1}(x,w)={\mathrm{\Phi }}_j([s_i(x),w])={\mathrm{\Phi }}_j([s_j(x)g_{ji}(x),w])=(x,\rho (g_{ji}(x))w)\mathrm{.}$ This is smooth with smooth inverse and is fibrewise linear. Consequently the ${\mathrm{\Phi }}_i$ form a smooth rank-$\dim V$ vector-bundle atlas.

The open quotient of the second-countable manifold $P\times V$ is second-countable. It is Hausdorff: points over distinct base points are separated using the Hausdorff base; points over the same base lie in one $r^{-1}(U_i)$ and are separated by the product chart ${\mathrm{\Phi }}_i$. Thus the charts ${\mathrm{\Phi }}_i$ can define a smooth-manifold atlas on the actual quotient space.

Any smooth vector-bundle structure for which all ${\mathrm{\Phi }}_i$ are local trivializations has exactly this atlas, so the identity map between it and the constructed structure is locally the identity in $U_i\times V$ and is a diffeomorphism. This proves uniqueness. The cocycle theorem [F3] gives the same abstract bundle whenever a countable principal cover is supplied, but the direct open-quotient argument above does not assume such a cover or choose a countable refinement. If $V=0$, $H$ is trivial, $M$ is empty, or $\rho$ is ineffective, the same formulas apply. No choice principle is used.