Checking whether a map between the fibre of an associated bundle $(P_F:=(P\times F)/\sim_G,\pi_F,M)$ and F is well-defined This is related to a previous post of mine: How do I prove that the typical fibre of the associated bundle $(P_F:=(P\times F)/\sim_G,\pi_F,M)$ is $F$? so I apologise (and please let me know) if I'm breaking any rules of the site.
To tackle this problem, I've tried a different route by first defining a map
$$\begin{alignat*}{2}
j:A_x&\longrightarrow F \\
[(p,f)]&\longmapsto j([(p,f)]):=f
\end{alignat*}$$
where $x\in M$ and $A_x:=\{[(p,f)]\in P_F \mid \pi_F([(p,f)])=x\}$, with $\pi_F$ the projection for the associated bundle. The equivalence relation is defined $[(p',f')]\sim_G [(p,f)] :\iff \exists g\in G: p'=p\triangleleft g:f'=g^{-1}\triangleright f$.
I want to show that this is well-defined (and ultimately a bijection, but I haven't got there yet), i.e $j([(p',f')])=j([(p,f)])$. My attempt so far is this: $$j([(p',f')]) = j([(p\triangleleft g,g^{-1}\triangleright f)]) = g^{-1}\triangleright f=j([(p,g^{-1}\triangleright f)])$$
but I'm not sure where to go next. I'm not entirely confident that the map is indeed well defined and that I'm not trying to prove something true that is simply false, any help would be much appreciated.
 A: Let me change your notation slightly so I can wrap my head around it. Let $P \xrightarrow{\pi} M$ be a principal $G$ bundle and $F$ a left $G$ space. If $p \in P$ denote the right action of $G$ on $P$ by $p \cdot g$ and if $f \in F$ the left action of $G$ on $F$ by $g \cdot f$. Then $P_F = (P \times_G F)$ where we have $[p,f] = [p \cdot g, g^{-1} \cdot f]$. If $m \in M$, we wish to identify the fiber $(P_F)_m$ with $F$ by a homeomorphism.
First consider the product $P \times F$ and fix a basepoint $b \in P$ such that $\pi(b) = m$, then consider $F_b = \lbrace b \rbrace \times F$. Then for any point $p$ in $P$ such that $\pi(p) = m$, there exists a unique $g \in G$ such that $p = b \cdot g$. So if $(p,f) \in P \times F$ and $p = b \cdot g$, then define a map $(P \times_G F)_m \to F_b$ by $[p,f] \mapsto (b,gf)$. This is well defined because $[p,f] = [bg,f] = [b,gf]$ and $[ph,h^{-1}f] = [bgh,h^{-1}f] = [b,ghh^{-1}f] = [b,gf] \mapsto (b,gf)$.
I claim this map is a homeomorphism by providing an inverse $F_b \to (P \times_G F)_m$ given by $(b,f) \mapsto [b,f]$. Then $(b,f) \mapsto [b,f] \mapsto (b,f)$ is the identity and $[p,f] = [bg,f] \mapsto (b,gf) \mapsto [b,gf] = [p,f]$ is also the identity.
Now it is clear that $F_b = \lbrace b \rbrace \times F$ is homeomorphic to $F$.
A: 
$\textbf{Set Up Notation:}$ Let $\pi: P\to M$ be a smooth surjective map and $ G$ be a Lie group
with a smooth action map $\mu: P\times G\to P$. We say, $\pi: P\to  M$
a principal $ G$-bundle if following conditions hold :


$(i)$
$\text{Stab}(p):=\{g\in  G|p\cdot g=p\}=e$, identity element of $ G$,
for all $p\in  P$,


$(ii)$ There is an open covering $\{U_\alpha\}$ of
$ M$ and a collection of diffeomorphisms
$\big\{\varphi_\alpha:\pi^{-1}(U_\alpha)\to U_\alpha\times  G\big\}$
such that the composition
$\pi^{-1}(U_\alpha)\xrightarrow{\varphi_\alpha}U_\alpha\times
 G\xrightarrow{\text{projection}}U_\alpha$ is same as
$\pi\big|{\pi^{-1}(U_\alpha)}\to U_\alpha$ i.e. for each $\alpha$ we
have a smooth $\Xi_\alpha:\pi^{-1}(U_\alpha)\to  G$ with
$\varphi_\alpha=\big(\pi\big|_{\pi^{-1}(U_\alpha)},\Xi_\alpha\big)$,


$(iii)$ for each $\alpha$ action map $\mu$ sends
$\pi^{-1}(U_\alpha)\times  G$ to $\pi^{-1}(U_\alpha)$ and
$\varphi_\alpha$ satisfies $\varphi_\alpha(p\cdot
 g)=\big(\pi(p),\Xi_\alpha(p)\cdot g\big)$ for each $p\in
 \pi^{-1}(U_\alpha).$

Condition $(iii)$ gives $\pi^{-1}\big(\pi(p)\big)=\{p\cdot g|g\in G\}=\text{Orbit}(p)$ for all $p\in P$.
$\textbf{Vector Bundle from a  Principal Bundle :}$ Let $\pi: P\to M$ be a principal $ G$-bundle and $\tau: G\to \text{GL}(V)$ be a smooth group homomorphism, i.e. a representation, where $V$ is a finite dimensional vector space. Consider $$E=P\times_\tau V:=\frac{ P\times V}{(p,v)\sim \big(p\cdot g, \tau(g^{-1})(v)\big)}$$ and the natural map $\widehat\pi: E\to  M$ defined by $\widehat\pi:[p,v]\mapsto \pi(p)$, but  $\big[p\cdot g,\tau(g^{-1})(v)\big]\xrightarrow{\widehat \pi}\pi(p\cdot g)=\pi(p)$, so $\widehat\pi$ is well-defined.
Choose a chart $\varphi_\alpha:\pi^{-1}(U_\alpha)\to U_\alpha\times  G$ as in the definition of principal $ G$-bundle. Note that a typical fibre of $\widehat\pi$ is $\widehat\pi^{-1}(m)=\big\{[p,v]\big|v\in V\big\}$, where $\pi(p)=m$, hence the fibre $\widehat\pi^{-1}(m)$ is isomorphic to $V$ as $\text{Stab}(p)=e\in G$.
$\textbf{Some Extra Facts:---}$Here I show with above construction we have a vector bundle, called Associated bundle. Consider $\Phi_\alpha:\pi^{-1}(U_\alpha)\times_\tau V\longrightarrow U_\alpha\times V$ given by $[p,v]\mapsto\big(\pi(p),\tau\big(\Xi_\alpha(p)\big)v\big)$, where $\varphi_\alpha=\big(\pi\big|_{\pi^{-1}(U_\alpha)},\Xi_\alpha\big)$ and $\Phi_\alpha$ is well-defined due to $ (iii)$. Note also that $\Psi_\alpha:U_\alpha\times V\longrightarrow \pi^{-1}(U_\alpha)\times_\tau V$ given by $(m,v)\mapsto\big[p,\tau\big(\Xi_\alpha(p)^{-1}\big)v\big]$, where $p$ is any element in $\pi^{-1}(m)$, is the inverse of $\Phi_\alpha$.
Next, choose another chart $\varphi_\beta:\pi^{-1}(U_\beta)\to U_\beta\times  G$ as in the definition of principal $ G$-bundle with $U_\alpha\cap U_\beta\not=\emptyset$. Then, $\Phi_\alpha\Psi_\beta:\big(U_\alpha\cap U_\beta\big)\times V\to \big(U_\alpha\cap U_\beta\big)\times V$ is given by $(m,v)\longmapsto\big(m,\tau\big(\Xi_\alpha(p)\cdot\Xi_\beta(p)^{-1}\big)v\big)$, where $p$ is any element in $\pi^{-1}(m)$.
Now we show that, $\Phi_\alpha\Psi_\beta$ is smooth. So choose $m_0\in U_\alpha\cap U_\beta$ Since $\pi: P\to M$ is a surjective submersion, we have another open nbd $\widetilde U_{\alpha\beta}$ of $m_0$ contained in $U_\alpha\cap U_\beta$ and a smooth map $s_{\alpha\beta}:\widetilde U_{\alpha\beta}\to \pi^{-1}\big(\widetilde U_{\alpha\beta}\big)$ with $\pi\circ s_{\alpha\beta}=\text{Id}_{\widetilde U_{\alpha\beta}}$. Then, $$\Phi_\alpha\Psi_\beta(m,v)=\bigg(m,\tau\bigg(\Xi_\alpha\big(s(m)\big)\cdot\Xi_\beta\big(s(m)\big)^{-1}\bigg)v\bigg)$$ for all $m\in \widetilde U_{\alpha\beta}$, so we are done as $\tau$ is a smooth map. So by vector bundle chart lemma, $\widehat\pi: E=P\times_\tau V\to M$ is a vector bundle, whose typical fibre is $V$.
A: Here's an attempt at an alternative proof I've tried, though I'm somewhat uncomfortable about it, particularly the surjectivity part.
Define a map $$\begin{alignat*}{2}
i:F&\longrightarrow A_x \\
f&\longmapsto i(f):=[(p,f)]
\end{alignat*}$$
where $p$ is in the fiber over $x\in M$, in the total space of the corresponding principal bundle $(P,\pi,M)$. Well-definedness does not need to be checked because the domain of the map is not a quotient space, only the target is.
Injectivity: Let $i(f)=i(a)$. $i(f)=i(a)\iff [(p,f)]=[(p,a)]\implies\exists g\in G: p=p\triangleleft g : a=g^{-1}\triangleright f$. Since the group action is free, $p=p\triangleleft g \implies g=e \implies a=f$, so $i$ is injective.
Surjectivity Let $[(p,f)]$ be some arbitrary element in $A_x$ we want to hit. We can hit this element simply by applying the map to $f$, ie $i(f)=[(p,f)]$, so the map is surjective because we have found an element in the domain that hits this arbitrary element.
Therefore, $i$ is bijective, so $F$ is isomorphic to the fiber of the associated bundle.
The surjectivity part feels wrong - am I allowed to just pluck the $p$ out of thin air like that? Do I need to somehow choose a particular $p$ from the $f$ I am applying the map to?
