Principal bundle over an associated bundle Let $(P,M,G)$ be a smooth principal bundle $\pi:P\longrightarrow M$ with structure group $G$ and let $H$ be a closed subgroup of $G$. I know that it is possible to construct the associated bundle
$$E=P\times_G (G/H)$$
with standard fiber $G/H$. I read (Kobayashi-Nomizu, Foundations of Differential Geometry, vol.1, Chap. I, Proposition 5.5) that $E$ can be identified with $P/H$ and that the projection
$$\pi_H:P\longrightarrow P/H$$
defines a principal bundle $(P,P/H,H)$ with structure group $H$. My question is: let $\pi_E:E\longrightarrow M$ the bundle projection of the associated bundle; is it true that $\pi=\pi_E\circ\pi_H$ under the identification $E=P/H$? I think that this is true (and maybe it is trivial), but I can't find any proof, if there is one.
 A: This is true.  The bulk of the proof is simply unraveling what you mean by "Under the identification $E = P/H$."
I'll write $g\ast p$ for the $G$ action on $P$.  I'll use the notation $[p,gH]_G$ to refer to the $G$ orbit through $(p,gH)\in P\times G/H$.  And I'll use $[p]_H$ to denote the $H$ orbit through $p\in P$, and similarly for $[p]_G$ (and I'm thinking of $M$ as being identified by $P/G$).  Lastly, I'll use $\rho:P/H\rightarrow P/G$ to denote the map $\rho([p]_H) = [p]_G$.
Let $f: P\times_G (G/H)\rightarrow P/H$ be defined by $f([p,gH]_G) = [g^{-1}\ast p]_H$ and let $f^{-1}:P/H\rightarrow P\times_G (G/H)$ be defined by $f^{-1}([p]_H) = [p,eH]_G$.
Proposition:  The maps $f$ and $f^{-1}$ are well defined and really are inverses of each other.  Further, $\pi_E =  \rho \circ f$
The map $[p,gH]_G\rightarrow [p]_H$ is well defined since $$f([g'\ast p, g' gH]_G)= [(g'g)^{-1} g'\ast p]_H = [g^{-1} g'^{-1} g' \ast p]_H = [g^{-1} \ast p]_H = f( [p,gH]_G)$$ and since $$f([p, gh H]_G) = [(gh)^{-1} \ast p]_H = [h^{-1} \ast(g^{-1} \ast p)]_H = [g^{-1} \ast p]_H = f([p,gH]_G).$$
To see that $f^{-1}$ is well defined, note that $$f^{-1}([h\ast p]_H) = [h\ast p, eH]_G = [ h^{-1}\ast h\ast p, h^{-1} H]_G = [p, eH]_G = f^{-1}([p]_H).$$
Lastly, to see that they are inverses, simply note that $$f(f^{-1}([p]_H)) = f([p,eH]_G) = [p]_H$$ and $$f^{-1}(f([p,gH]_G)) = f^{-1}([g^{-1}\ast p]_H) = [g^{-1}\ast p, eH]_G = [g\ast g^{-1} \ast p, gH]_G = [p,gH]_G.$$
Lastly, $\pi_E([p,gH]_G) = [p]_G$, while $\rho(f([p,gH]_G)) = \rho([g^{-1}\ast p]_H) = [g^{-1}\ast p]_G = [p]_G.$ $\square$
Armed with this proposition, the equality you seek is really $$\pi =\pi_E\circ f^{-1} \circ \pi_H$$ which follows easily:  $\pi(p) = [p]_G$, while $$\pi_E(f^{-1}(\pi_H(p)) = \pi_E(f^{-1}([p]_H)) = \pi_E([p,eH]_G) = [p]_G.$$
