[proofplan] We use the Slice Theorem for Proper Lie Group Actions rather than the result being proved. Since the action is free, each stabiliser is trivial, so the usual associated-bundle slice model reduces to an equivariant product of a local slice with $G$. Properness and openness of the quotient map give the required Hausdorff and second countable topology on the orbit space, and the slice quotient charts are shown to induce exactly this topology. These product neighbourhoods then make the quotient map locally a product projection and give the principal bundle trivializations. Finally, any other smooth structure making the quotient map a smooth submersion has charts locally compatible with the same slice charts, which gives uniqueness. [/proofplan]

[step:Apply the slice theorem at each point of $P$]Let $B := P/G$ denote the set of right $G$-orbits equipped with the [quotient topology](/page/Quotient%20Topology), and let $q: P \to B$ denote the orbit projection. Let $\rho: P \times G \to P$ be the smooth action map defined by $\rho(p,g) = p \cdot g$. For each $p_0 \in P$, the stabiliser subgroup is \begin{align*} G_{p_0} := \{g \in G : p_0 \cdot g = p_0\}. \end{align*} Freeness gives $G_{p_0} = \{e\}$, where $e \in G$ is the identity element. The action is proper by hypothesis. The Slice Theorem for Proper Lie Group Actions, applied to this proper smooth right action at $p_0$, gives a local model of the form $S_{p_0} \times_{G_{p_0}} G$. Since $G_{p_0}=\{e\}$, the associated-bundle quotient is canonically identified with the product $S_{p_0}\times G$ by the map induced from $(s,g)\mapsto(s,g)$. Thus there are a $G$-invariant open neighbourhood $O_{p_0} \subset P$ of $p_0$, an embedded submanifold $S_{p_0} \subset O_{p_0}$ with $p_0 \in S_{p_0}$, and a diffeomorphism \begin{align*} \Phi_{p_0}: S_{p_0} \times G &\to O_{p_0} \end{align*} specified by $\Phi_{p_0}(s,g) = s \cdot g$. The codomain is $G$-invariant, hence saturated for the orbit [equivalence relation](/page/Equivalence%20Relation), so $U_{p_0} := q(O_{p_0}) \subset B$ is open in the quotient topology and $q^{-1}(U_{p_0}) = O_{p_0}$.[/step]

[guided]We first build the local model before putting a smooth structure on the orbit set. Let $B := P/G$ be the set of right $G$-orbits with the quotient topology, and let $q:P\to B$ be the orbit projection. Let $\rho:P\times G\to P$ denote the smooth right action map, so $\rho(p,g)=p\cdot g$. Fix $p_0\in P$. The stabiliser subgroup at $p_0$ is \begin{align*} G_{p_0}:=\{g\in G:p_0\cdot g=p_0\}. \end{align*} Because the action is free, the only group element fixing $p_0$ is the identity element $e\in G$, so $G_{p_0}=\{e\}$. The action is proper by hypothesis, so the Slice Theorem for Proper Lie Group Actions applies to the smooth proper right action at $p_0$. It gives a $G$-invariant open neighbourhood $O_{p_0}\subset P$, an embedded submanifold $S_{p_0}\subset O_{p_0}$ containing $p_0$, and a local model $S_{p_0}\times_{G_{p_0}}G\to O_{p_0}$. Since $G_{p_0}=\{e\}$, the associated-bundle quotient has no nontrivial stabiliser identification, so it is identified with the ordinary product $S_{p_0}\times G$. Thus the slice theorem gives a diffeomorphism \begin{align*} \Phi_{p_0}:S_{p_0}\times G&\to O_{p_0} \end{align*} specified by $\Phi_{p_0}(s,g)=s\cdot g$. The point of freeness is exactly this simplification: without freeness, the local quotient would remember the stabiliser action on the slice. Here each nearby orbit meets $S_{p_0}$ exactly once inside $O_{p_0}$. Since $O_{p_0}$ is $G$-invariant, it is saturated for the orbit equivalence relation. Therefore $U_{p_0}:=q(O_{p_0})$ is open in the quotient topology and $q^{-1}(U_{p_0})=O_{p_0}$.[/guided]

[step:Verify the quotient topology is a manifold topology]The quotient map $q:P\to B$ is open. Indeed, if $W\subset P$ is open, then \begin{align*} q^{-1}(q(W))=\{p\cdot g:p\in W,\ g\in G\}. \end{align*} For each $g\in G$, the right translation map $R_g:P\to P$ defined by $R_g(p)=p\cdot g$ is a diffeomorphism with inverse $R_{g^{-1}}$. Hence $q^{-1}(q(W))$ is a union of open sets $R_g(W)$, so it is open in $P$, and therefore $q(W)$ is open in the quotient topology. The space $B$ is Hausdorff. Properness of $A:P\times G\to P\times P$ implies that the orbit equivalence relation \begin{align*} E:=A(P\times G)=\{(p,p\cdot g):p\in P,\ g\in G\} \end{align*} is closed in $P\times P$, because $E$ is the image of the proper map $A$ and proper maps between Hausdorff locally compact manifolds are closed. Let $p_1,p_2\in P$ satisfy $q(p_1)\neq q(p_2)$. Then $(p_1,p_2)\notin E$. Since $E$ is closed, the [open set](/page/Open%20Set) $(P\times P)\setminus E$ contains $(p_1,p_2)$; choose open neighbourhoods $W_1\subset P$ of $p_1$ and $W_2\subset P$ of $p_2$ such that $W_1\times W_2\subset (P\times P)\setminus E$. The quotient map is open, so $q(W_1)$ and $q(W_2)$ are open neighbourhoods of $q(p_1)$ and $q(p_2)$ in $B$. If $b\in q(W_1)\cap q(W_2)$, then there are $w_1\in W_1$ and $w_2\in W_2$ with $q(w_1)=q(w_2)$, so $(w_1,w_2)\in E$, contradicting $W_1\times W_2\subset (P\times P)\setminus E$. Hence $q(W_1)$ and $q(W_2)$ are disjoint, and $B$ is Hausdorff. Since $P$ is a smooth manifold, it is second countable. Let $(W_j)_{j\in\mathbb{N}}$ be a countable basis for the topology of $P$. Because $q$ is open and surjective, the countable family $(q(W_j))_{j\in\mathbb{N}}$ is a basis for the quotient topology of $B$. It remains to record that the slice charts induce exactly the quotient topology. For a slice $S:=S_{p_0}$ and $U:=U_{p_0}$, the map $\theta:S\to U$ defined by $\theta(s)=q(s)$ is continuous because it is the restriction of $q$. If $V\subset S$ is open, choose an open set $W\subset P$ with $V=W\cap S$. In the slice neighbourhood $O=\Phi(S\times G)$, the saturation of $V$ is \begin{align*} \Phi(V\times G)\subset O. \end{align*} This set is open in $O$, hence open in $P$, and it is saturated. Therefore $\theta(V)=q(\Phi(V\times G))$ is open in $U$ with the quotient topology. Thus each $\theta:S\to U$ is a homeomorphism, so the topology defined by the slice atlas agrees with the quotient topology.[/step]

[guided]We verify the quotient topology carefully because the smooth atlas must be built on the actual orbit-space topology. First, $q:P\to B$ is open. If $W\subset P$ is open, then \begin{align*} q^{-1}(q(W))=\{p\cdot g:p\in W,\ g\in G\}. \end{align*} For each $g\in G$, define the right translation map $R_g:P\to P$ by $R_g(p)=p\cdot g$. The inverse map is $R_{g^{-1}}$, so $R_g$ is a diffeomorphism and sends open sets to open sets. Hence $q^{-1}(q(W))$ is a union of the open sets $R_g(W)$, and is open in $P$. By the definition of the quotient topology, $q(W)$ is open in $B$. Next we prove Hausdorffness. Properness of $A:P\times G\to P\times P$ implies that the orbit relation \begin{align*} E:=A(P\times G)=\{(p,p\cdot g):p\in P,\ g\in G\} \end{align*} is closed in $P\times P$, since proper maps between Hausdorff locally compact manifolds are closed. Let $p_1,p_2\in P$ represent distinct orbits. Then $(p_1,p_2)\notin E$. Because $E$ is closed, choose open neighbourhoods $W_1\subset P$ of $p_1$ and $W_2\subset P$ of $p_2$ such that $W_1\times W_2\subset (P\times P)\setminus E$. The already-proved openness of $q$ makes $q(W_1)$ and $q(W_2)$ open in $B$. They are disjoint: otherwise a point in their intersection would be represented by some $w_1\in W_1$ and $w_2\in W_2$ in the same orbit, which means $(w_1,w_2)\in E$, contradicting the choice of $W_1$ and $W_2$. Thus distinct points of $B$ have disjoint open neighbourhoods. Since $P$ is a smooth manifold, it has a countable basis $(W_j)_{j\in\mathbb{N}}$. Because $q$ is open and surjective, the countable family $(q(W_j))_{j\in\mathbb{N}}$ is a basis for $B$: every open set in $B$ has open preimage in $P$, and every point in that preimage lies in some basis element $W_j$ whose image is contained in the given open set. Finally, the slice charts give the same topology. For a slice $S:=S_{p_0}$ and $U:=U_{p_0}$, define $\theta:S\to U$ by $\theta(s)=q(s)$. This map is continuous because it is the restriction of $q$. If $V\subset S$ is open, choose an open set $W\subset P$ with $V=W\cap S$. In the slice neighbourhood $O=\Phi(S\times G)$, the saturation of $V$ is \begin{align*} \Phi(V\times G)\subset O. \end{align*} This subset is open in $O$, hence open in $P$, and it is saturated. Therefore $\theta(V)=q(\Phi(V\times G))$ is open in $U$. Thus $\theta:S\to U$ is a homeomorphism, and the slice-atlas topology agrees with the quotient topology.[/guided]

[step:Use slice quotients as smooth charts on $P/G$]For each $p_0 \in P$, define \begin{align*} \theta_{p_0}: S_{p_0} &\to U_{p_0} \end{align*} by $\theta_{p_0}(s) = q(s)$. The map $\theta_{p_0}$ is bijective: surjectivity follows from $O_{p_0} = \Phi_{p_0}(S_{p_0} \times G)$, and injectivity follows because if $q(s_1) = q(s_2)$ for $s_1,s_2 \in S_{p_0}$, then $s_2 = s_1 \cdot g$ for some $g \in G$, and uniqueness in the product representation $\Phi_{p_0}: S_{p_0} \times G \to O_{p_0}$ forces $s_1 = s_2$. Declare the sets $U_{p_0}$ to be coordinate domains with chart maps $\theta_{p_0}^{-1}: U_{p_0} \to S_{p_0}$. These charts are smoothly compatible. Indeed, suppose $U_{p_0}\cap U_{p_1}\neq\varnothing$. The transition map has domain \begin{align*} D_{01}:=\theta_{p_0}^{-1}(U_{p_0}\cap U_{p_1})=S_{p_0}\cap O_{p_1}. \end{align*} The equality holds because $O_{p_1}=q^{-1}(U_{p_1})$ is saturated. Since $O_{p_1}$ is open in $P$, the set $D_{01}$ is open in the embedded submanifold $S_{p_0}$. For $s\in D_{01}$, the transition map is \begin{align*} \theta_{p_1}^{-1}\circ\theta_{p_0}(s)=\pi_{S,1}(\Phi_{p_1}^{-1}(s)), \end{align*} where $\pi_{S,1}:S_{p_1}\times G\to S_{p_1}$ is the projection onto the first factor. This is smooth as a composition of the inclusion $D_{01}\hookrightarrow O_{p_1}$, the smooth inverse $\Phi_{p_1}^{-1}:O_{p_1}\to S_{p_1}\times G$, and the smooth projection $\pi_{S,1}$. The reverse transition is identical with $p_0$ and $p_1$ interchanged. This atlas defines a smooth structure on $B$.[/step]

[guided]We now check the overlap domains rather than only writing the formula for the transition map. Suppose $U_{p_0}\cap U_{p_1}\neq\varnothing$. A point of the first chart is represented by $s\in S_{p_0}$. It lies over the chart overlap exactly when $q(s)\in U_{p_1}$. Since $U_{p_1}=q(O_{p_1})$ and $O_{p_1}=q^{-1}(U_{p_1})$ is saturated, this condition is equivalent to $s\in O_{p_1}$. Hence the transition map is defined on \begin{align*} D_{01}:=\theta_{p_0}^{-1}(U_{p_0}\cap U_{p_1})=S_{p_0}\cap O_{p_1}. \end{align*} Because $O_{p_1}$ is open in $P$, the intersection $S_{p_0}\cap O_{p_1}$ is open in the embedded submanifold $S_{p_0}$. This verifies that the transition map has an open submanifold domain. For $s\in D_{01}$, the slice diffeomorphism at $p_1$ writes $s$ uniquely as $s=s_1\cdot g_1$ with $(s_1,g_1)\in S_{p_1}\times G$. In symbols, $(s_1,g_1)=\Phi_{p_1}^{-1}(s)$. Since $q(s)=q(s_1)$, the corresponding representative in the second slice is $s_1$. Therefore \begin{align*} \theta_{p_1}^{-1}\circ\theta_{p_0}(s)=\pi_{S,1}(\Phi_{p_1}^{-1}(s)), \end{align*} where $\pi_{S,1}:S_{p_1}\times G\to S_{p_1}$ is the projection onto the first factor. This is smooth because it is the composition of the inclusion $D_{01}\hookrightarrow O_{p_1}$, the smooth inverse $\Phi_{p_1}^{-1}$, and the smooth projection $\pi_{S,1}$. Interchanging $p_0$ and $p_1$ gives the smoothness of the inverse transition map, so the slice charts form a smooth atlas.[/guided]

[step:Show the slice product maps are smooth principal trivializations]Fix $p_0 \in P$ and write $S := S_{p_0}$, $O := O_{p_0}$, $U := U_{p_0}$, $\Phi := \Phi_{p_0}$, and $\theta := \theta_{p_0}$. Define \begin{align*} \Theta: U \times G &\to q^{-1}(U) \end{align*} by $\Theta(b,g) = \theta^{-1}(b) \cdot g$. Under the chart identification $U \cong S$ given by $\theta^{-1}$, this map is exactly $\Phi: S \times G \to O$, so $\Theta$ is a diffeomorphism. Its inverse is \begin{align*} \Psi: q^{-1}(U) &\to U \times G \end{align*} specified by $\Psi(p) = (q(p),\pi_G(\Phi^{-1}(p)))$, where $\pi_G: S \times G \to G$ is the projection onto the second factor. This formula proves smoothness of the inverse because $q$ is locally $\theta \circ \pi_S \circ \Phi^{-1}$, where $\pi_S: S \times G \to S$ is the projection onto the first factor. Moreover, for every $b \in U$ and $g,h \in G$, \begin{align*} \Theta(b,g \cdot h) = \theta^{-1}(b) \cdot (g \cdot h) = (\theta^{-1}(b) \cdot g) \cdot h = \Theta(b,g) \cdot h. \end{align*} Thus $\Theta$ is $G$-equivariant when $U \times G$ carries the standard right action on the second factor. Also $q(\Theta(b,g)) = b$, so $q$ corresponds under $\Theta$ to the projection $U \times G \to U$. Therefore $q: P \to B$ is locally a smooth $G$-equivariant product projection and in particular is a smooth submersion.[/step]

[guided]The main technical point is the smoothness of the inverse trivialization. We do not prove it by appealing to the theorem under discussion. Instead, we use the diffeomorphism supplied by the slice theorem. Fix $p_0 \in P$ and abbreviate $S := S_{p_0}$, $O := O_{p_0}$, $U := U_{p_0}$, $\Phi := \Phi_{p_0}$, and $\theta := \theta_{p_0}$. The slice theorem gives \begin{align*} \Phi: S \times G &\to O \end{align*} with $\Phi(s,g) = s \cdot g$, and the previous step identifies $U$ smoothly with $S$ through $\theta: S \to U$. Therefore the local trivialization \begin{align*} \Theta: U \times G &\to q^{-1}(U) \end{align*} specified by $\Theta(b,g) = \theta^{-1}(b) \cdot g$ is just the slice diffeomorphism $\Phi$ written with $U$ in place of $S$. Consequently $\Theta$ is smooth and bijective. Now compute its inverse explicitly. Let $\pi_S: S \times G \to S$ and $\pi_G: S \times G \to G$ denote the two projection maps. For $p \in q^{-1}(U) = O$, the point $\Phi^{-1}(p)$ is the unique pair $(s,g) \in S \times G$ such that $p = s \cdot g$. Hence \begin{align*} \Psi: q^{-1}(U) &\to U \times G \end{align*} is given by $\Psi(p) = (q(p),\pi_G(\Phi^{-1}(p)))$. The first component is smooth in these coordinates because \begin{align*} q(p) = \theta(\pi_S(\Phi^{-1}(p))). \end{align*} The second component is smooth because it is $\pi_G \circ \Phi^{-1}$. Therefore $\Psi = \Theta^{-1}$ is smooth, and $\Theta$ is a diffeomorphism. Finally, the principal equivariance condition follows from associativity of the right action. For every $b \in U$ and $g,h \in G$, \begin{align*} \Theta(b,g \cdot h) = \theta^{-1}(b) \cdot (g \cdot h) = (\theta^{-1}(b) \cdot g) \cdot h = \Theta(b,g) \cdot h. \end{align*} Also $q(\Theta(b,g)) = b$, so the quotient map is the projection to $U$ in this product chart. This proves both local triviality and the submersion property.[/guided]

[step:Conclude the principal bundle structure and uniqueness]The preceding step constructs, around every $b_0 \in B$, an open neighbourhood $U \subset B$ and a $G$-equivariant diffeomorphism $\Theta: U \times G \to q^{-1}(U)$ such that $q \circ \Theta$ is the projection onto $U$. These are exactly the local trivializations required for a smooth principal right $G$-bundle. It remains to justify uniqueness of the smooth structure. Let $B'$ be the same orbit set with another smooth structure for which $q:P\to B'$ is a smooth submersion. A smooth submersion is an open map by the local normal form for submersions, so for every slice neighbourhood $O\subset P$ the subset $U=q(O)$ is open in $B'$. Fix a slice chart $\theta:S\to U$ from above, and regard the same subset $U$ as an open subset of $B'$. The map $q|_S:S\to U\subset B'$ is smooth because it is the restriction of the smooth map $q:P\to B'$. To prove its inverse is smooth, use the Submersion Local Section Theorem for $q:P\to B'$. Fix $b\in U$ and let $s_b:=(q|_S)^{-1}(b)\in S$. The theorem gives an open neighbourhood $V\subset B'$ of $b$ and a smooth local section $\sigma:V\to P$ with $q\circ\sigma=\operatorname{id}_V$ and $\sigma(b)=s_b$. Since $O$ is an open neighbourhood of $s_b$ in $P$, shrink $V$ so that $\sigma(V)\subset O$. If $r:O\to S$ denotes the smooth first component $r=\pi_S\circ\Phi^{-1}$ of the slice diffeomorphism, then on $V\cap U$ the inverse of $q|_S$ is $r\circ\sigma$, hence is smooth. Thus each slice coordinate map $\theta^{-1}:U\to S$ is smooth for the alternative smooth structure $B'$. Conversely, the map $\theta:S\to U\subset B'$ is smooth because $\theta=q|_S$ and $q:P\to B'$ is smooth. Therefore the identity map from the slice-atlas smooth structure on $B$ to the alternative smooth structure $B'$ is smooth in every slice chart, and the identity map from $B'$ back to the slice-atlas smooth structure is smooth because the slice coordinate maps are smooth on $B'$. The two smooth structures are therefore identical. Hence $P/G$ has the required unique smooth structure and $q:P\to P/G$ is a smooth principal $G$-bundle.[/step]

[guided]We prove uniqueness by comparing the slice atlas with an arbitrary competing smooth structure on the same orbit set. Let $B'$ denote that competing smooth manifold structure, and assume $q:P\to B'$ is a smooth submersion. First we need the slice domains to be open in $B'$. This is where submersions enter: by the local normal form for submersions, a smooth submersion is locally a projection, and [projections are open maps](/theorems/955). Hence $q:P\to B'$ is open. Since each slice neighbourhood $O\subset P$ is open, its image $U=q(O)$ is open in $B'$. Fix a slice chart $\theta:S\to U$. The map $\theta:S\to U\subset B'$ is the restriction $q|_S$, so it is smooth as a map into $B'$. We must also show that the inverse map $U\to S$ is smooth in the $B'$-smooth structure. Fix $b\in U$ and let $s_b=(q|_S)^{-1}(b)\in S$. The Submersion Local Section Theorem applied to the smooth submersion $q:P\to B'$ gives an open neighbourhood $V\subset B'$ of $b$ and a smooth local section $\sigma:V\to P$ such that \begin{align*} q\circ\sigma=\operatorname{id}_V \end{align*} and $\sigma(b)=s_b$. Since $O$ is open in $P$ and contains $s_b$, we shrink $V$ so that $\sigma(V)\subset O$. Define the smooth retraction-to-the-slice map \begin{align*} r:O&\to S \end{align*} by $r=\pi_S\circ\Phi^{-1}$, where $\pi_S:S\times G\to S$ is the first projection. For every $b'\in V\cap U$, the point $\sigma(b')$ lies in the same orbit as the unique slice representative $(q|_S)^{-1}(b')$. Therefore \begin{align*} (q|_S)^{-1}(b')=r(\sigma(b')). \end{align*} Thus $(q|_S)^{-1}=r\circ\sigma$ on $V\cap U$, and this is smooth. Since $b$ was arbitrary, the inverse of every slice chart is smooth for the competing structure. We now have smoothness in both directions. The map from a slice chart $S$ into $B'$ is smooth because it is $q|_S$. The map from $B'$ into the slice coordinates is smooth locally because it is $r\circ\sigma$. Hence the identity map between the slice-atlas smooth structure and the competing smooth structure is a diffeomorphism. The smooth structure is unique.[/guided]