Principal g bundle and associated fiber bundle

Let $G$ be a topological group, as in Topological group: multiplication and inversion are continuous, with identity $1$. A right principal $G$-bundle is a continuous map $\pi :P\to B$ with a continuous right action $(p,g)\mapsto pg$, satisfying $p1=p$, $(pg)h=p(gh)$ and $\pi (pg)=\pi (p)$, together with equivariant bundle charts ${\theta }_i:{\pi }^{-1}(U_i)\cong U_i\times G$ over an open cover. Equivariance means ${\theta }_i(pg)=(b,ag)$ whenever ${\theta }_i(p)=(b,a)$. Charts use ordinary products as in Locally trivial fiber bundle. In each fiber the action is free and transitive: right multiplication on $G$ has those properties and the chart identifies the actions. Freeness alone is not the definition.

A left $G$-space is a topological space $F$ with a continuous map $(g,x)\mapsto gx$ such that $1x=x$ and $g(hx)=(gh)x$. Effectiveness of this action is not required. Define $P{\times }_{G}F=(P\times F)\mathrm{/}((pg,x)\sim (p,gx))$ with the ordinary quotient topology, and write $[p,x]$ for its points. Precisely, the relation is the orbit relation of the right action $(p,x)\cdot g=(pg,g^{-1}x)$. Its action law is $((p,x)\cdot g)\cdot h=(pgh,h^{-1}{g}^{-1}x)=(p,x)\cdot (gh)$, and its generating relations are exactly the displayed ones. Thus the equivalence relation and quotient are defined without choosing orbit representatives.

The projection $r([p,x])=\pi (p)$ is well-defined and continuous by For a quotient map $q:X\to Y$, a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$; and a composite of quotient maps is a quotient map, since $(p,x)\mapsto \pi (p)$ is continuous and constant on every orbit. This is the associated fiber-bundle construction; the next proposition proves its local triviality and pullback property. The quotient construction and projection already make sense before that proof.

If $B$ is empty then $P$ is empty. If $F$ is empty the associated space is empty even for nonempty $B$; this is allowed by our bundle convention. For singleton $F$ the construction is the orbit projection of the principal bundle. For the trivial group it is the product with $F$ over the chart-identified base. No AC is used.