[proofplan] We first extract transition functions from a given principal bundle by comparing two equivariant local trivializations on an overlap. Equivariance forces every chart change over the base to be left multiplication in the fibre by a uniquely determined smooth map into $G$, and composition of chart changes gives the cocycle identity. Conversely, we glue the local products $U_i \times G$ using the prescribed cocycle, prove that the gluing relation is an [equivalence relation](/page/Equivalence%20Relation) with no unwanted identifications inside one chart, and then use the local products as the smooth atlas. The cocycle identity also guarantees that the projection and right $G$-action are well-defined and that the resulting bundle has exactly the prescribed transition maps. [/proofplan]

[step:Extract transition maps from equivariant product charts]For each $i \in I$, write the trivialization as \begin{align*} \Phi_i: \pi^{-1}(U_i) \to U_i \times G. \end{align*} Since $\Phi_i$ is a $G$-equivariant local trivialization over $U_i$, it has the form \begin{align*} \Phi_i(q) = (\pi(q), \theta_i(q)) \end{align*} for a smooth map \begin{align*} \theta_i: \pi^{-1}(U_i) \to G. \end{align*} The right $G$-equivariance of $\Phi_i$ means that, for every $q \in \pi^{-1}(U_i)$ and every $a \in G$, \begin{align*} \theta_i(q \cdot a) = \theta_i(q)a. \end{align*} Fix indices $i,j \in I$ with $U_i \cap U_j \neq \varnothing$. Define the overlap chart change \begin{align*} T_{ij}: (U_i \cap U_j) \times G \to (U_i \cap U_j) \times G \end{align*} by \begin{align*} T_{ij} := \Phi_i \circ \Phi_j^{-1}. \end{align*} Since both trivializations cover the identity map on $U_i \cap U_j$, there is a smooth map \begin{align*} A_{ij}: (U_i \cap U_j) \times G \to G \end{align*} such that \begin{align*} T_{ij}(p,h) = (p,A_{ij}(p,h)). \end{align*} The map $T_{ij}$ is right $G$-equivariant, because both $\Phi_i$ and $\Phi_j$ are right $G$-equivariant. Hence, for every $p \in U_i \cap U_j$ and every $h,a \in G$, \begin{align*} A_{ij}(p,ha) = A_{ij}(p,h)a. \end{align*} Define \begin{align*} g_{ij}: U_i \cap U_j \to G \end{align*} by \begin{align*} g_{ij}(p) := A_{ij}(p,e). \end{align*} The map $g_{ij}$ is smooth because it is the composition of the smooth map $A_{ij}$ with the smooth section $p \mapsto (p,e)$. Taking $h=e$ and $a=h$ in the equivariance identity gives \begin{align*} A_{ij}(p,h) = g_{ij}(p)h. \end{align*} Therefore \begin{align*} \Phi_i \circ \Phi_j^{-1}(p,h) = (p,g_{ij}(p)h). \end{align*} The same formula also proves uniqueness: if another map $\tilde g_{ij}: U_i \cap U_j \to G$ satisfies the same identity, then evaluating at $h=e$ gives $\tilde g_{ij}(p)=g_{ij}(p)$ for every $p \in U_i \cap U_j$.[/step]

[guided]The point of the equivariance hypothesis is that it rigidifies the possible form of a change of trivialization. We begin with two product charts \begin{align*} \Phi_i: \pi^{-1}(U_i) \to U_i \times G \end{align*} and \begin{align*} \Phi_j: \pi^{-1}(U_j) \to U_j \times G. \end{align*} Because each chart lies over the identity map on the base, the composite \begin{align*} T_{ij}: (U_i \cap U_j) \times G \to (U_i \cap U_j) \times G, \qquad T_{ij} := \Phi_i \circ \Phi_j^{-1} \end{align*} preserves the base point. Thus there is a smooth map \begin{align*} A_{ij}: (U_i \cap U_j) \times G \to G \end{align*} with \begin{align*} T_{ij}(p,h) = (p,A_{ij}(p,h)). \end{align*} Now we use right equivariance. Since both $\Phi_i$ and $\Phi_j$ commute with the right $G$-action, the chart change $T_{ij}$ also commutes with that action. The right action on a local product is \begin{align*} (p,h)\cdot a = (p,ha), \end{align*} so equivariance gives \begin{align*} T_{ij}(p,ha) = T_{ij}((p,h)\cdot a)=T_{ij}(p,h)\cdot a. \end{align*} In terms of $A_{ij}$, this says \begin{align*} (p,A_{ij}(p,ha)) = (p,A_{ij}(p,h)a), \end{align*} and hence \begin{align*} A_{ij}(p,ha)=A_{ij}(p,h)a. \end{align*} This identity says that the value of $A_{ij}$ at every fibre coordinate $h$ is determined by its value at the identity element $e \in G$. Define \begin{align*} g_{ij}: U_i \cap U_j \to G \end{align*} by \begin{align*} g_{ij}(p) := A_{ij}(p,e). \end{align*} Then, taking $h=e$ and $a=h$ in the equivariance identity, we obtain \begin{align*} A_{ij}(p,h)=A_{ij}(p,e)h=g_{ij}(p)h. \end{align*} Therefore the chart change is exactly \begin{align*} \Phi_i \circ \Phi_j^{-1}(p,h)=(p,g_{ij}(p)h). \end{align*} The map $g_{ij}$ is smooth because $A_{ij}$ is smooth and the map $p \mapsto (p,e)$ from $U_i \cap U_j$ to $(U_i \cap U_j)\times G$ is smooth. Finally, uniqueness is forced by evaluating the transition formula at $h=e$: any map producing the same chart change must equal $p \mapsto A_{ij}(p,e)$.[/guided]

[step:Derive the identity and cocycle equations from chart composition] For $p \in U_i$, the overlap chart change from the $i$-chart to itself is the identity map: \begin{align*} \Phi_i \circ \Phi_i^{-1}(p,h) = (p,h). \end{align*} By the transition formula, this is also \begin{align*} \Phi_i \circ \Phi_i^{-1}(p,h) = (p,g_{ii}(p)h). \end{align*} Taking $h=e$ gives $g_{ii}(p)=e$. Now let $p \in U_i \cap U_j \cap U_k$ and $h \in G$. The equality of chart changes \begin{align*} \Phi_i \circ \Phi_k^{-1} = (\Phi_i \circ \Phi_j^{-1}) \circ (\Phi_j \circ \Phi_k^{-1}) \end{align*} on $(U_i \cap U_j \cap U_k)\times G$ gives \begin{align*} (p,g_{ik}(p)h) = (p,g_{ij}(p)g_{jk}(p)h). \end{align*} Taking $h=e$ gives \begin{align*} g_{ik}(p)=g_{ij}(p)g_{jk}(p). \end{align*} Thus the transition maps satisfy the required cocycle identity. [/step]

[step:Construct the glued total space and identify the equivalence relation] Assume now that smooth maps $g_{ij}: U_i \cap U_j \to G$ satisfying the stated identities are given. Let \begin{align*} E := \bigsqcup_{i \in I}(U_i \times G) \end{align*} and denote by $(p,h)_i$ the element $(p,h)$ in the $i$-th summand. Define a binary relation $\sim_0$ on $E$ by declaring \begin{align*} (p,h)_j \sim_0 (p,g_{ij}(p)h)_i \end{align*} whenever $p \in U_i \cap U_j$ and $h \in G$. Define $\sim$ to be the equivalence relation on $E$ generated by $\sim_0$. We first record two consequences of the cocycle equations. For $p \in U_i \cap U_j$, the cocycle identity with $k=i$ gives \begin{align*} g_{ij}(p)g_{ji}(p)=g_{ii}(p)=e, \end{align*} and the cocycle identity with $k=j$ gives \begin{align*} g_{ji}(p)g_{ij}(p)=g_{jj}(p)=e. \end{align*} Thus $g_{ji}(p)=g_{ij}(p)^{-1}$. Because $\sim$ is defined as the equivalence relation generated by the elementary identifications, it is reflexive, symmetric, and transitive by construction. The cocycle identities show that finite chains have the expected normal form. A reverse elementary move from the $i$-summand to the $j$-summand multiplies by $g_{ji}(p)$, which equals $g_{ij}(p)^{-1}$ by the preceding computation, so every forward or reverse move from index $a$ to index $b$ contributes the factor $g_{ba}(p)$. Hence, if a chain over the fixed base point $p$ moves through indices $i_0,i_1,\dots,i_m$, then its total fibre multiplication is \begin{align*} g_{i_m i_{m-1}}(p)\cdots g_{i_2 i_1}(p)g_{i_1 i_0}(p)=g_{i_m i_0}(p). \end{align*} This follows by repeated use of $g_{ab}(p)g_{bc}(p)=g_{ac}(p)$ on the relevant triple overlaps. In particular, the generated relation is exactly the relation prescribed by the transition data. Let \begin{align*} P_g := E/{\sim} \end{align*} and write $[p,h]_i$ for the equivalence class of $(p,h)_i$. [/step]

[step:Prove that each local product maps bijectively onto the inverse image over its base open set]Define \begin{align*} \pi_g: P_g \to M \end{align*} by \begin{align*} \pi_g([p,h]_i) := p. \end{align*} This is well-defined because the relation only identifies points with the same base point $p$. For each $i \in I$, define \begin{align*} \Psi_i: U_i \times G \to \pi_g^{-1}(U_i) \end{align*} by \begin{align*} \Psi_i(p,h):=[p,h]_i. \end{align*} The map $\Psi_i$ is surjective: if $[p,h]_j \in \pi_g^{-1}(U_i)$, then $p \in U_i \cap U_j$, and the defining relation gives \begin{align*} [p,h]_j=[p,g_{ij}(p)h]_i. \end{align*} The map $\Psi_i$ is injective. If $[p,h]_i=[q,a]_i$, then the relation preserves base points, so $p=q$. Since any chain of identifications from the $i$-chart back to the $i$-chart multiplies the fibre coordinate by the product $g_{ii}(p)=e$ after collapsing the chain with the cocycle identity, the final fibre coordinate must equal the initial one. Hence $a=h$. Therefore $\Psi_i$ is a bijection.[/step]

[guided]We need the local products to survive the quotient without folding a single product $U_i \times G$ onto itself. Define \begin{align*} \pi_g: P_g \to M \end{align*} by \begin{align*} \pi_g([p,h]_i)=p. \end{align*} This is well-defined because every allowed identification has the form \begin{align*} (p,h)_j \sim (p,g_{ij}(p)h)_i, \end{align*} so it never changes the base point. Now define the candidate local chart map \begin{align*} \Psi_i: U_i \times G \to \pi_g^{-1}(U_i) \end{align*} by \begin{align*} \Psi_i(p,h)=[p,h]_i. \end{align*} Surjectivity is exactly why the transition relation was chosen in this direction. If $[p,h]_j$ is a point [lying over](/theorems/2876) $U_i$, then $p \in U_i \cap U_j$. The defining relation gives \begin{align*} [p,h]_j=[p,g_{ij}(p)h]_i, \end{align*} so the same quotient point is represented in the $i$-th product. Injectivity is the only subtle point. Suppose \begin{align*} [p,h]_i=[q,a]_i. \end{align*} Since the elementary identifications preserve base points, every finite chain representing equality in the generated equivalence relation preserves base points, so we first get $p=q$. Thus all identifications occur over one fixed point $p \in M$. A finite chain of elementary identifications from the $i$-summand back to the $i$-summand has the form of multiplying the fibre coordinate successively by transition elements \begin{align*} g_{i_1 i_0}(p),\quad g_{i_2 i_1}(p),\quad \dots,\quad g_{i_m i_{m-1}}(p), \end{align*} where $i_0=i$ and $i_m=i$. If one of the elementary moves is traversed in the reverse direction, it contributes the inverse of the forward transition element; since $g_{ba}(p)=g_{ab}(p)^{-1}$, this inverse is exactly the transition element for the reversed pair of indices. Thus the displayed product describes arbitrary finite chains, not only chains following the originally written generating direction. The cocycle identity collapses this product step by step: \begin{align*} g_{i_m i_{m-1}}(p)\cdots g_{i_2 i_1}(p)g_{i_1 i_0}(p)=g_{i_m i_0}(p)=g_{ii}(p)=e. \end{align*} Thus the total multiplication along the chain is the identity element of $G$, so the fibre coordinate cannot change. Hence $a=h$, and $\Psi_i$ is injective.[/guided]

[step:Give the quotient its unique smooth structure]We define the atlas topology on $P_g$ by declaring a set $O\subset P_g$ to be open exactly when $\Psi_i^{-1}(O\cap \pi_g^{-1}(U_i))$ is open in $U_i\times G$ for every $i\in I$. The smooth charts are the inverses $\Psi_i^{-1}:\pi_g^{-1}(U_i)\to U_i\times G$. To prove that this atlas gives a smooth manifold structure, we verify directly that the model pieces are smooth manifolds, the chart changes are smooth diffeomorphisms satisfying the compatibility equations, and the atlas topology is [Hausdorff](/page/Hausdorff%20Space) and [second countable](/page/Second%20Countable%20Space). The model pieces $U_i \times G$ are smooth manifolds because $U_i$ is open in the smooth manifold $M$ and $G$ is a Lie group. On an overlap $U_i \cap U_j$, the transition map \begin{align*} \Psi_i^{-1}\circ \Psi_j: (U_i \cap U_j)\times G \to (U_i \cap U_j)\times G \end{align*} is \begin{align*} \Psi_i^{-1}\circ \Psi_j(p,h)=(p,g_{ij}(p)h). \end{align*} The fibre component map $(p,h)\mapsto g_{ij}(p)h$ is smooth because $g_{ij}$ is smooth and multiplication in the Lie group $G$ is smooth. Its inverse is \begin{align*} (p,h)\mapsto (p,g_{ji}(p)h), \end{align*} which is smooth for the same reason. The identities $g_{ii}=e$ and $g_{ij}g_{jk}=g_{ik}$ give the identity and cocycle conditions for these chart changes. It remains to verify the topological hypotheses. Since $M$ is [second countable](/page/Second%20Countable%20Space), it is Lindelof, so choose a countable subcover $(U_{i_m})_{m\in\mathbb N}$ of $(U_i)_{i\in I}$. Since $G$ is a Lie group, it is second countable. For each $m$, choose a countable basis $\mathcal B_m$ for $U_{i_m}\times G$. The family \begin{align*} \{\Psi_{i_m}(B): m\in\mathbb N, B\in\mathcal B_m\} \end{align*} is a countable basis for the atlas topology on $P_g$, because the charts $\Psi_{i_m}$ cover $P_g$ and all chart changes are homeomorphisms. To prove Hausdorffness, take two distinct points $x,y\in P_g$. If $\pi_g(x)$ and $\pi_g(y)$ are distinct points of $M$, choose disjoint open neighbourhoods $V_x,V_y\subset M$ of these base points, using that smooth manifolds are Hausdorff. For any [open set](/page/Open%20Set) $V\subset M$, the set $\pi_g^{-1}(V)$ is open in the atlas topology because \begin{align*} \Psi_i^{-1}(\pi_g^{-1}(V)\cap \pi_g^{-1}(U_i))=(V\cap U_i)\times G \end{align*} for every $i\in I$. Hence $\pi_g^{-1}(V_x)$ and $\pi_g^{-1}(V_y)$ are disjoint open neighbourhoods of $x$ and $y$. If $\pi_g(x)=\pi_g(y)=p$, choose an index $i$ with $p\in U_i$. Write $x=\Psi_i(p,h)$ and $y=\Psi_i(p,a)$ with $h,a\in G$. Since $\Psi_i$ is injective, $h\neq a$. Because $G$ is Hausdorff, choose disjoint open neighbourhoods $W_h,W_a\subset G$ of $h$ and $a$. Then $\Psi_i(U_i\times W_h)$ and $\Psi_i(U_i\times W_a)$ are disjoint open neighbourhoods of $x$ and $y$. The preceding verification shows that the atlas topology and charts $\Psi_i^{-1}$ define a smooth manifold structure on $P_g$. This topology is also the [quotient topology](/page/Quotient%20Topology) induced from the disjoint union $E$. Indeed, for a subset $O\subset P_g$, the quotient definition says that $O$ is open exactly when its preimage in every summand $U_i\times G$ is open; that preimage is precisely $\Psi_i^{-1}(O\cap \pi_g^{-1}(U_i))$. This is the defining condition for the atlas topology above. The smooth structure is unique because the maps $\Psi_i:U_i\times G\to\pi_g^{-1}(U_i)$ are required to be smooth inverse charts covering $P_g$; any such smooth structure has exactly the same atlas and hence the same maximal smooth atlas.[/step]

[guided]The quotient $P_g$ is only a set until we put a topology and smooth structure on it. The intended charts are the inverses of the bijections \begin{align*} \Psi_i:U_i\times G\to \pi_g^{-1}(U_i) \end{align*} constructed above. We define the atlas topology by declaring $O\subset P_g$ to be open exactly when $\Psi_i^{-1}(O\cap \pi_g^{-1}(U_i))$ is open in $U_i\times G$ for every $i\in I$. To show that this really gives a smooth manifold structure, we verify the required ingredients directly: smooth model pieces, smooth transition maps, compatibility on triple overlaps, and the topological conditions that the atlas topology is [Hausdorff](/page/Hausdorff%20Space) and [second countable](/page/Second%20Countable%20Space). The model pieces are smooth manifolds because each $U_i$ is an open subset of the smooth manifold $M$, and $G$ is a Lie group. On the overlap $U_i\cap U_j$, the transition map between the proposed charts is \begin{align*} \Psi_i^{-1}\circ \Psi_j:(U_i\cap U_j)\times G\to (U_i\cap U_j)\times G \end{align*} and it is given by \begin{align*} \Psi_i^{-1}\circ \Psi_j(p,h)=(p,g_{ij}(p)h). \end{align*} This map is smooth because $g_{ij}:U_i\cap U_j\to G$ is smooth and multiplication in the Lie group $G$ is smooth. Its inverse is \begin{align*} (p,h)\mapsto (p,g_{ji}(p)h), \end{align*} which is smooth for the same reason. The identities $g_{ii}=e$ and $g_{ij}g_{jk}=g_{ik}$ give exactly the identity and cocycle conditions for these chart changes. For second countability, use that a second-countable manifold is Lindelof. Since $M$ is second countable, the open cover $(U_i)_{i\in I}$ has a countable subcover $(U_{i_m})_{m\in\mathbb N}$. Since $G$ is a Lie group, it is second countable, so each product $U_{i_m}\times G$ has a countable basis $\mathcal B_m$. The sets \begin{align*} \{\Psi_{i_m}(B):m\in\mathbb N,\ B\in\mathcal B_m\} \end{align*} form a countable basis for the atlas topology because the charts $\Psi_{i_m}$ cover $P_g$ and all chart changes are homeomorphisms. For Hausdorffness, take distinct points $x,y\in P_g$. If their base points are distinct, then the Hausdorff property of the smooth manifold $M$ gives disjoint open neighbourhoods $V_x,V_y\subset M$ of $\pi_g(x)$ and $\pi_g(y)$. We must first know that their inverse images under $\pi_g$ are open in the atlas topology. If $V\subset M$ is open, then in the $i$-th chart we have \begin{align*} \Psi_i^{-1}(\pi_g^{-1}(V)\cap \pi_g^{-1}(U_i))=(V\cap U_i)\times G, \end{align*} which is open in $U_i\times G$. Therefore $\pi_g^{-1}(V)$ is open. Applying this to $V_x$ and $V_y$, the inverse images $\pi_g^{-1}(V_x)$ and $\pi_g^{-1}(V_y)$ are disjoint open neighbourhoods of $x$ and $y$. If instead $\pi_g(x)=\pi_g(y)=p$, choose $i\in I$ with $p\in U_i$ and write $x=\Psi_i(p,h)$ and $y=\Psi_i(p,a)$. Since $\Psi_i$ is injective and $x\neq y$, we have $h\neq a$. The Hausdorff property of $G$ gives disjoint open neighbourhoods $W_h,W_a\subset G$, and then $\Psi_i(U_i\times W_h)$ and $\Psi_i(U_i\times W_a)$ separate $x$ and $y$. The direct atlas verification is now complete. The atlas topology is the same as the quotient topology from the disjoint union $E$: a subset $O\subset P_g$ is open in the quotient topology exactly when its preimage in each summand $U_i\times G$ is open, and that preimage is $\Psi_i^{-1}(O\cap \pi_g^{-1}(U_i))$, which is exactly the atlas-topology condition. Therefore $P_g$ has a unique smooth structure for which the maps $\Psi_i$ are smooth inverse charts, and uniqueness follows because any such smooth structure has the same covering atlas and hence the same maximal smooth atlas.[/guided]

[step:Define the projection and right action and verify the principal bundle axioms]The map \begin{align*} \pi_g: P_g \to M \end{align*} is smooth because, in the chart $\Psi_i$, it is the projection \begin{align*} U_i \times G \to U_i, \qquad (p,h)\mapsto p. \end{align*} Define a right action \begin{align*} P_g \times G \to P_g \end{align*} by \begin{align*} [p,h]_i \cdot a := [p,ha]_i. \end{align*} This is well-defined: if $[p,h]_j=[p,g_{ij}(p)h]_i$, then \begin{align*} [p,ha]_j=[p,g_{ij}(p)ha]_i=[p,(g_{ij}(p)h)a]_i. \end{align*} The [group action](/page/Group%20Action) identities follow from associativity and the identity element in $G$: \begin{align*} ([p,h]_i \cdot a)\cdot b=[p,(ha)b]_i=[p,h(ab)]_i=[p,h]_i\cdot(ab) \end{align*} and \begin{align*} [p,h]_i\cdot e=[p,he]_i=[p,h]_i. \end{align*} The action is smooth because, in each chart $\Psi_i$, it is the smooth map \begin{align*} (U_i \times G)\times G \to U_i \times G, \qquad ((p,h),a)\mapsto (p,ha). \end{align*} For each $i \in I$, the map $\Psi_i$ is a $G$-equivariant local trivialization of $\pi_g$ over $U_i$, since \begin{align*} \pi_g(\Psi_i(p,h))=p \end{align*} and \begin{align*} \Psi_i(p,h)\cdot a=[p,ha]_i=\Psi_i(p,ha). \end{align*} The right action is free and transitive on every fibre because, under $\Psi_i$, the fibre over $p$ is identified with $\{p\}\times G$ and the action is ordinary right multiplication on $G$. Hence $\pi_g: P_g \to M$ is a smooth principal right $G$-bundle.[/step]

[guided]The projection is smooth because smoothness can be checked in the charts just constructed. In the chart $\Psi_i$, the projection $\pi_g:P_g\to M$ becomes the ordinary projection \begin{align*} U_i\times G\to U_i \end{align*} given by $(p,h)\mapsto p$, which is smooth. Define the right action by \begin{align*} [p,h]_i\cdot a=[p,ha]_i. \end{align*} The point to check is that this definition does not depend on the chosen representative. If the same quotient point is written using the $j$-chart, then on an overlap we have \begin{align*} [p,h]_j=[p,g_{ij}(p)h]_i. \end{align*} After multiplying by $a\in G$ on the right, the two representatives become \begin{align*} [p,ha]_j \end{align*} and \begin{align*} [p,g_{ij}(p)ha]_i=[p,(g_{ij}(p)h)a]_i. \end{align*} These are still identified by the same transition rule, so the action is well-defined. The action identities follow from the group law in $G$: \begin{align*} ([p,h]_i\cdot a)\cdot b=[p,(ha)b]_i=[p,h(ab)]_i=[p,h]_i\cdot(ab) \end{align*} and \begin{align*} [p,h]_i\cdot e=[p,he]_i=[p,h]_i. \end{align*} The action is smooth because, in the chart $\Psi_i$, it is the smooth product map \begin{align*} (U_i\times G)\times G\to U_i\times G \end{align*} given by $((p,h),a)\mapsto(p,ha)$. Finally, each $\Psi_i$ is a $G$-equivariant local trivialization: it covers the identity on $U_i$ because $\pi_g(\Psi_i(p,h))=p$, and it intertwines the right action because \begin{align*} \Psi_i(p,h)\cdot a=[p,ha]_i=\Psi_i(p,ha). \end{align*} On each fibre, this is ordinary right multiplication on $G$, which is free and transitive. Hence $\pi_g:P_g\to M$ is a smooth principal right $G$-bundle.[/guided]

[step:Identify the recovered transition maps and prove uniqueness up to isomorphism]For $p \in U_i \cap U_j$ and $h \in G$, the local trivializations $\Psi_i^{-1}$ and $\Psi_j^{-1}$ satisfy \begin{align*} \Psi_i^{-1}\circ \Psi_j(p,h)=(p,g_{ij}(p)h). \end{align*} Thus the constructed bundle has precisely the prescribed transition maps. Finally, suppose $\pi':P'\to M$ is another smooth principal right $G$-bundle with local trivializations \begin{align*} \Psi_i': U_i \times G \to (\pi')^{-1}(U_i) \end{align*} whose transition maps are the same $g_{ij}$. Define \begin{align*} F: P_g \to P' \end{align*} locally by \begin{align*} F([p,h]_i):=\Psi_i'(p,h). \end{align*} This is well-defined because, on $U_i \cap U_j$, \begin{align*} \Psi_j'(p,h)=\Psi_i'(p,g_{ij}(p)h). \end{align*} In the charts $\Psi_i$ and $\Psi_i'$, the map $F$ is the identity map on $U_i \times G$, so $F$ is smooth and bijective with smooth inverse. It preserves the base projection and commutes with the right $G$-action by construction. Therefore $F$ is an isomorphism of smooth principal right $G$-bundles, proving uniqueness up to isomorphism.[/step]

[guided]The transition maps of the constructed bundle are read directly from the charts. On $U_i\cap U_j$, we have \begin{align*} \Psi_i^{-1}\circ\Psi_j(p,h)=(p,g_{ij}(p)h), \end{align*} so the recovered transition function is exactly the prescribed map $g_{ij}:U_i\cap U_j\to G$. Now suppose $\pi':P'\to M$ is another smooth principal right $G$-bundle with local trivializations \begin{align*} \Psi_i':U_i\times G\to (\pi')^{-1}(U_i) \end{align*} and with the same transition functions $g_{ij}$. Define \begin{align*} F:P_g\to P' \end{align*} by the local formula \begin{align*} F([p,h]_i)=\Psi_i'(p,h). \end{align*} This is well-defined because if two representatives are related on an overlap, then \begin{align*} [p,h]_j=[p,g_{ij}(p)h]_i, \end{align*} and the equality of transition functions for $P'$ gives \begin{align*} \Psi_j'(p,h)=\Psi_i'(p,g_{ij}(p)h). \end{align*} Thus both representatives determine the same point of $P'$. In the chart $\Psi_i$ on $P_g$ and the chart $\Psi_i'$ on $P'$, the map $F$ is the identity map on $U_i\times G$. Therefore $F$ is smooth, bijective, and has smooth inverse obtained by the same chartwise identity construction. The formula also shows that $F$ preserves the projection to $M$ and commutes with the right $G$-action. Hence $F$ is an isomorphism of smooth principal right $G$-bundles, which proves uniqueness up to isomorphism.[/guided]