[proofplan]
We construct the correspondence in both directions. Starting from an equivariant map $\varphi:P \to F$, we define a section by choosing any point in the fibre of $P$ over $x \in M$ and prove that equivariance makes the definition independent of this choice. Starting from a section $s:M \to P \times_G F$, we recover a unique value $\varphi_s(p) \in F$ by writing $s(\pi(p))$ with first coordinate $p$. Local trivializations then show that both constructions preserve smoothness, and the two assignments are inverse to one another.
[/proofplan]
[step:Construct a section from an equivariant map]
Let $\varphi:P \to F$ be a smooth map satisfying
\begin{align*}
\varphi(pg)=g^{-1}\cdot \varphi(p)
\end{align*}
for all $p \in P$ and $g \in G$.
Define a map
\begin{align*}
s_\varphi:M &\to P \times_G F
\end{align*}
as follows. For $x \in M$, choose any $p \in \pi^{-1}(\{x\})$ and set
\begin{align*}
s_\varphi(x):=[p,\varphi(p)].
\end{align*}
This definition is independent of the choice of $p$. Indeed, if $p' \in \pi^{-1}(\{x\})$, then the principal bundle action is free and transitive on the fibre $\pi^{-1}(\{x\})$, so there is a unique $g \in G$ such that $p'=pg$. Using the equivariance of $\varphi$ and the defining [equivalence relation](/page/Equivalence%20Relation) for $P \times_G F$, we get
\begin{align*}
[p',\varphi(p')]=[pg,\varphi(pg)]=[pg,g^{-1}\cdot \varphi(p)]=[p,\varphi(p)].
\end{align*}
Thus $s_\varphi$ is a well-defined map.
Let $\pi_{P \times_G F}:P \times_G F \to M$ denote the associated bundle projection, defined by $\pi_{P \times_G F}([p,f])=\pi(p)$. It is a section of $P \times_G F \to M$ because this bundle projection sends $[p,f]$ to $\pi(p)$. Hence, for $x=\pi(p)$,
\begin{align*}
\pi_{P \times_G F}(s_\varphi(x))=\pi_{P \times_G F}([p,\varphi(p)])=\pi(p)=x.
\end{align*}
[guided]
We begin with a smooth equivariant map $\varphi:P \to F$. The intended section must assign to each point $x \in M$ an element of the associated fibre over $x$. Since points in that fibre are represented by pairs $(p,f)$ with $p \in \pi^{-1}(\{x\})$, the only possible definition is
\begin{align*}
s_\varphi(x):=[p,\varphi(p)]
\end{align*}
for some $p \in \pi^{-1}(\{x\})$.
The issue is that there is usually no preferred point $p$ in the principal fibre over $x$. We therefore check that the value does not depend on the choice. Let $p,p' \in \pi^{-1}(\{x\})$. Since $\pi:P \to M$ is a principal right $G$-bundle, the right action of $G$ on the fibre $\pi^{-1}(\{x\})$ is free and transitive. Therefore there is a unique $g \in G$ such that
\begin{align*}
p'=pg.
\end{align*}
Using the equivariance condition for $\varphi$, we have
\begin{align*}
\varphi(p')=\varphi(pg)=g^{-1}\cdot \varphi(p).
\end{align*}
Now apply the equivalence relation defining the associated bundle:
\begin{align*}
(p,f)\sim(pg,g^{-1}\cdot f).
\end{align*}
With $f=\varphi(p)$, this gives
\begin{align*}
[p',\varphi(p')]=[pg,g^{-1}\cdot \varphi(p)]=[p,\varphi(p)].
\end{align*}
Thus $s_\varphi(x)$ is independent of the chosen representative $p$.
Finally, $s_\varphi$ is a section because the associated bundle projection sends $[p,f]$ to $\pi(p)$. Therefore, if $x=\pi(p)$, then
\begin{align*}
\pi_{P \times_G F}(s_\varphi(x))=\pi_{P \times_G F}([p,\varphi(p)])=\pi(p)=x.
\end{align*}
[/guided]
[/step]
[step:Verify smoothness of the section locally]
Let $U \subset M$ be an [open set](/page/Open%20Set) in a trivializing cover of the principal bundle $\pi:P \to M$, and choose the corresponding smooth local section
\begin{align*}
\sigma:U \to P.
\end{align*}
Thus $\pi \circ \sigma=\operatorname{id}_U$. Define the associated local trivialization $\Theta_\sigma:U \times F \to (P \times_G F)|_U$ by $\Theta_\sigma(x,f)=[\sigma(x),f]$. Since $P \to M$ is a smooth principal $G$-bundle and $F$ is a smooth left $G$-space, this is the smooth associated-bundle trivialization induced by the smooth local section $\sigma$.
For $x \in U$, the definition of $s_\varphi$ gives
\begin{align*}
s_\varphi(x)=[\sigma(x),\varphi(\sigma(x))]=\Theta_\sigma(x,\varphi(\sigma(x))).
\end{align*}
The map $U \to U \times F$ given by $x \mapsto (x,\varphi(\sigma(x)))$ is smooth because $\sigma$ and $\varphi$ are smooth. Since $\Theta_\sigma$ is a smooth local trivialization, $s_\varphi|_U$ is smooth. Smoothness is local on $M$, so $s_\varphi:M \to P \times_G F$ is smooth.
[/step]
[step:Recover an equivariant map from a section]
Let $s:M \to P \times_G F$ be a smooth section. For $p \in P$, put $x:=\pi(p)$. Since $s(x)$ lies in the associated fibre over $x$, there exists a representative $[q,a]$ with $q \in \pi^{-1}(\{x\})$ and $a \in F$. The principal right $G$-action is transitive on $\pi^{-1}(\{x\})$, so there is a unique $g \in G$ such that $q=pg$. By the associated-bundle equivalence relation, $[q,a]=[pg,a]=[p,g\cdot a]$. Hence there exists at least one $f \in F$, namely $f=g\cdot a$, such that
\begin{align*}
s(x)=[p,f].
\end{align*}
This element $f$ is unique. If $[p,f]=[p,f']$, then by the equivalence relation there exists $g \in G$ such that
\begin{align*}
p=pg
\end{align*}
and
\begin{align*}
f'=g^{-1}\cdot f.
\end{align*}
The right $G$-action on $P$ is free, so $g=e$, where $e \in G$ is the identity element. Hence $f'=f$.
Define
\begin{align*}
\varphi_s:P &\to F
\end{align*}
by declaring $\varphi_s(p)$ to be the unique element of $F$ satisfying
\begin{align*}
s(\pi(p))=[p,\varphi_s(p)].
\end{align*}
For $p \in P$ and $g \in G$, the same section value can be represented using $pg$:
\begin{align*}
s(\pi(pg))=s(\pi(p))=[p,\varphi_s(p)]=[pg,g^{-1}\cdot \varphi_s(p)].
\end{align*}
By uniqueness of the second coordinate relative to the first coordinate $pg$, we obtain
\begin{align*}
\varphi_s(pg)=g^{-1}\cdot \varphi_s(p).
\end{align*}
Thus $\varphi_s$ satisfies the required equivariance condition.
[/step]
[step:Verify smoothness of the recovered map locally]
Let $U \subset M$ be an open set in a trivializing cover of the principal bundle $\pi:P \to M$, and choose the corresponding smooth local section
\begin{align*}
\sigma:U \to P.
\end{align*}
Let $\Psi_\sigma:U \times G \to \pi^{-1}(U)$ be the map $\Psi_\sigma(x,g)=\sigma(x)g$. By the local trivialization theorem for smooth principal bundles, $\Psi_\sigma$ is a smooth principal-bundle trivialization determined by $\sigma$. Let
\begin{align*}
h_\sigma:\pi^{-1}(U) &\to G
\end{align*}
denote the smooth map obtained as the $G$-component of $\Psi_\sigma^{-1}$, so that every $p \in \pi^{-1}(U)$ has the unique representation
\begin{align*}
p=\sigma(\pi(p))h_\sigma(p).
\end{align*}
Using the associated bundle trivialization $\Theta_\sigma:U \times F \to (P \times_G F)|_U$ given by $\Theta_\sigma(x,f)=[\sigma(x),f]$, define the local representative of the section $s$ by
\begin{align*}
a_\sigma:U &\to F
\end{align*}
through the identity
\begin{align*}
s(x)=[\sigma(x),a_\sigma(x)].
\end{align*}
Equivalently, $a_\sigma$ is the $F$-component of the smooth map $\Theta_\sigma^{-1}\circ s|_U:U \to U \times F$, so $a_\sigma$ is smooth.
For $p \in \pi^{-1}(U)$, write $p=\sigma(\pi(p))h_\sigma(p)$. Since
\begin{align*}
s(\pi(p))=[\sigma(\pi(p)),a_\sigma(\pi(p))]=[p,h_\sigma(p)^{-1}\cdot a_\sigma(\pi(p))],
\end{align*}
the defining uniqueness of $\varphi_s(p)$ gives
\begin{align*}
\varphi_s(p)=h_\sigma(p)^{-1}\cdot a_\sigma(\pi(p)).
\end{align*}
The maps $h_\sigma$, $a_\sigma$, and $\pi$ are smooth, inversion in $G$ is smooth, and the action $G \times F \to F$ is smooth. Therefore $\varphi_s|_{\pi^{-1}(U)}$ is smooth. Since the open sets $\pi^{-1}(U)$ cover $P$, the map $\varphi_s:P \to F$ is smooth.
[guided]
The point of this step is to turn the abstract definition of $\varphi_s$ into an explicit formula in a local trivialization. Choose an open set $U \subset M$ from a trivializing cover of the smooth principal bundle $\pi:P \to M$, and choose the corresponding smooth local section
\begin{align*}
\sigma:U \to P.
\end{align*}
This local section identifies the principal bundle over $U$ with $U \times G$ by the smooth map $\Psi_\sigma:U \times G \to \pi^{-1}(U)$ defined by $\Psi_\sigma(x,g)=\sigma(x)g$. The smoothness and invertibility of $\Psi_\sigma$ are exactly the local trivialization property of a smooth principal bundle.
For each $p \in \pi^{-1}(U)$, there is therefore a unique element $h_\sigma(p) \in G$ such that
\begin{align*}
p=\sigma(\pi(p))h_\sigma(p).
\end{align*}
The map
\begin{align*}
h_\sigma:\pi^{-1}(U) &\to G
\end{align*}
is smooth because it is the $G$-component of the inverse trivialization $\Psi_\sigma^{-1}$.
The section $s$ also has a local representative in the associated bundle trivialization. Define $\Theta_\sigma:U \times F \to (P \times_G F)|_U$ by $\Theta_\sigma(x,f)=[\sigma(x),f]$. This is the smooth associated-bundle trivialization induced by the smooth local section $\sigma$. Because $\Theta_\sigma$ is a smooth local trivialization and $s|_U$ is smooth, the $F$-component of $\Theta_\sigma^{-1}\circ s|_U$ is a smooth map
\begin{align*}
a_\sigma:U &\to F
\end{align*}
satisfying
\begin{align*}
s(x)=[\sigma(x),a_\sigma(x)]
\end{align*}
for every $x \in U$.
Now fix $p \in \pi^{-1}(U)$. Write
\begin{align*}
p=\sigma(\pi(p))h_\sigma(p).
\end{align*}
Using the equivalence relation in the associated bundle with $g=h_\sigma(p)$ and $f=a_\sigma(\pi(p))$, we have
\begin{align*}
[\sigma(\pi(p)),a_\sigma(\pi(p))]=[\sigma(\pi(p))h_\sigma(p),h_\sigma(p)^{-1}\cdot a_\sigma(\pi(p))].
\end{align*}
Since $\sigma(\pi(p))h_\sigma(p)=p$, this becomes
\begin{align*}
s(\pi(p))=[p,h_\sigma(p)^{-1}\cdot a_\sigma(\pi(p))].
\end{align*}
By the definition of $\varphi_s(p)$ as the unique second coordinate relative to the first coordinate $p$, we obtain
\begin{align*}
\varphi_s(p)=h_\sigma(p)^{-1}\cdot a_\sigma(\pi(p)).
\end{align*}
This formula proves smoothness. The map $p \mapsto h_\sigma(p)$ is smooth, the map $p \mapsto a_\sigma(\pi(p))$ is smooth as a composition of smooth maps, inversion $g \mapsto g^{-1}$ in the Lie group $G$ is smooth, and the action map $G \times F \to F$, $(g,f) \mapsto g\cdot f$, is smooth by hypothesis. Therefore $\varphi_s$ is smooth on $\pi^{-1}(U)$. Since such sets $\pi^{-1}(U)$ cover $P$, $\varphi_s$ is smooth on all of $P$.
[/guided]
[/step]
[step:Show that the two constructions are inverse]
Let $\varphi:P \to F$ be a smooth map satisfying $\varphi(pg)=g^{-1}\cdot \varphi(p)$. Construct $s_\varphi$ and then recover $\varphi_{s_\varphi}$. For each $p \in P$,
\begin{align*}
s_\varphi(\pi(p))=[p,\varphi(p)].
\end{align*}
By the uniqueness of the second coordinate relative to the fixed first coordinate $p$, the recovered map satisfies
\begin{align*}
\varphi_{s_\varphi}(p)=\varphi(p).
\end{align*}
Hence $\varphi_{s_\varphi}=\varphi$.
Conversely, let $s:M \to P \times_G F$ be a smooth section. Construct $\varphi_s$ and then construct $s_{\varphi_s}$. For $x \in M$, choose any $p \in \pi^{-1}(\{x\})$. By definition of $\varphi_s$,
\begin{align*}
s(x)=s(\pi(p))=[p,\varphi_s(p)].
\end{align*}
Therefore
\begin{align*}
s_{\varphi_s}(x)=[p,\varphi_s(p)]=s(x).
\end{align*}
Thus $s_{\varphi_s}=s$.
The assignments $\varphi \mapsto s_\varphi$ and $s \mapsto \varphi_s$ are therefore mutually inverse bijections between smooth equivariant maps $P \to F$ and smooth sections $M \to P \times_G F$.
[/step]
