[proofplan] We first check that the formula for $\Phi_F$ is independent of the chosen representative in the associated bundle quotient. The equivariance of the principal bundle morphism is exactly the condition needed to carry the defining relation on $P\times F$ to the defining relation on $Q\times F$. We then verify that the associated bundle projection is respected. Finally, smoothness is checked in associated bundle charts built from local principal sections, where the map becomes an explicit smooth map involving $f$, the left action of $G$ on $F$, and a smooth transition function determined by $\Phi$. [/proofplan]

[step:Use equivariance to prove that the formula is independent of representatives]Let $\sim_P$ be the [equivalence relation](/page/Equivalence%20Relation) on $P\times F$ defining $P\times_G F$, so that \begin{align*} (p g,u)\sim_P(p,g\cdot u) \end{align*} for every $p\in P$, $g\in G$, and $u\in F$. Equivalently, \begin{align*} [p g,g^{-1}\cdot u]=[p,u]. \end{align*} Let $p\in P$, $u\in F$, and $g\in G$. Since $\Phi$ is $G$-equivariant, \begin{align*} \Phi(p g)=\Phi(p)g. \end{align*} Therefore, in $Q\times_G F$, \begin{align*} [\Phi(p g),g^{-1}\cdot u]=[\Phi(p)g,g^{-1}\cdot u]=[\Phi(p),u]. \end{align*} Thus equivalent representatives in $P\times F$ have the same image in $Q\times_G F$, and the rule \begin{align*} [p,u]\mapsto[\Phi(p),u] \end{align*} defines a well-defined map $\Phi_F:P\times_G F\to Q\times_G F$.[/step]

[guided]The only possible obstruction to defining $\Phi_F$ is that an element of $P\times_G F$ has many representatives. We must prove that replacing $(p,u)$ by an equivalent pair does not change the proposed output. The associated bundle $P\times_G F$ is formed from the right action of $G$ on $P$ and the left action of $G$ on $F$. Its defining relation is \begin{align*} (p g,u)\sim_P(p,g\cdot u) \end{align*} for $p\in P$, $g\in G$, and $u\in F$. The same relation may be written in the form \begin{align*} [p g,g^{-1}\cdot u]=[p,u]. \end{align*} Now use the defining property of a principal bundle morphism: $\Phi$ is equivariant for the right $G$-actions, so \begin{align*} \Phi(p g)=\Phi(p)g. \end{align*} Hence the two representatives $(p,u)$ and $(p g,g^{-1}\cdot u)$ are sent to \begin{align*} (\Phi(p),u) \end{align*} and \begin{align*} (\Phi(p g),g^{-1}\cdot u)=(\Phi(p)g,g^{-1}\cdot u). \end{align*} But these two pairs are equivalent in $Q\times_G F$, again by the defining associated bundle relation. Therefore \begin{align*} [\Phi(p g),g^{-1}\cdot u]=[\Phi(p)g,g^{-1}\cdot u]=[\Phi(p),u]. \end{align*} This proves that the value of $\Phi_F([p,u])$ depends only on the class $[p,u]$, not on the chosen representative.[/guided]

[step:Check that the induced map covers $f$] Let $\rho_P:P\times_G F\to M$ and $\rho_Q:Q\times_G F\to N$ be the associated bundle projections, defined by \begin{align*} \rho_P([p,u])=\pi_P(p) \end{align*} and \begin{align*} \rho_Q([q,u])=\pi_Q(q). \end{align*} For $[p,u]\in P\times_G F$, the fact that $\Phi$ covers $f$ gives \begin{align*} \rho_Q(\Phi_F([p,u]))=\rho_Q([\Phi(p),u])=\pi_Q(\Phi(p))=f(\pi_P(p))=f(\rho_P([p,u])). \end{align*} Thus \begin{align*} \rho_Q\circ \Phi_F=f\circ \rho_P, \end{align*} so $\Phi_F$ is a bundle map covering $f$. [/step]

[step:Write the map in associated bundle charts and prove smoothness] Let $x_0\in M$. Choose an open neighbourhood $U\subset M$ of $x_0$ and a smooth local section \begin{align*} s:U\to P \end{align*} of $\pi_P$. Choose an open neighbourhood $V\subset N$ of $f(x_0)$ with $f(U)\subset V$ and a smooth local section \begin{align*} t:V\to Q \end{align*} of $\pi_Q$. Define \begin{align*} \gamma:U\to G \end{align*} to be the unique smooth map satisfying \begin{align*} \Phi(s(x))=t(f(x))\gamma(x) \end{align*} for every $x\in U$. The uniqueness follows from the freeness and transitivity of the right $G$-action on each fiber of $Q$, and smoothness follows by reading $\gamma$ as the $G$-coordinate of $\Phi\circ s$ in the principal trivialization determined by $t$. The associated bundle chart determined by $s$ is \begin{align*} \Psi_s:\rho_P^{-1}(U)\to U\times F,\quad [s(x)a,u]\mapsto (x,a\cdot u), \end{align*} where $x\in U$, $a\in G$, and $u\in F$. The associated bundle chart determined by $t$ is \begin{align*} \Psi_t:\rho_Q^{-1}(V)\to V\times F,\quad [t(y)b,u]\mapsto (y,b\cdot u), \end{align*} where $y\in V$, $b\in G$, and $u\in F$. For $x\in U$, $a\in G$, and $u\in F$, \begin{align*} \Phi(s(x)a)=\Phi(s(x))a=t(f(x))\gamma(x)a. \end{align*} Therefore \begin{align*} (\Psi_t\circ \Phi_F\circ \Psi_s^{-1})(x,a\cdot u)=(f(x),\gamma(x)a\cdot u). \end{align*} Equivalently, for $v=a\cdot u\in F$, \begin{align*} (\Psi_t\circ \Phi_F\circ \Psi_s^{-1})(x,v)=(f(x),\gamma(x)\cdot v). \end{align*} The map $(x,v)\mapsto (f(x),\gamma(x)\cdot v)$ is smooth because $f$ is smooth, $\gamma$ is smooth, and the left action map $G\times F\to F$ is smooth. Since smoothness of a map between smooth bundles is local in charts, $\Phi_F$ is smooth near every point of $P\times_G F$. [/step]

[step:Conclude functoriality of the associated bundle construction] The preceding steps show that $\Phi_F$ is well-defined, smooth, and satisfies \begin{align*} \rho_Q\circ \Phi_F=f\circ \rho_P. \end{align*} Hence $\Phi_F:P\times_G F\to Q\times_G F$ is a smooth bundle map covering $f$, as claimed. [/step]