[proofplan] We turn the $G$-valued cocycle into a $\operatorname{Diff}(F')$-valued cocycle by sending each $g \in G$ to the diffeomorphism of $F'$ induced by the given left action. The cocycle identities ensure that the stated gluing rule is an [equivalence relation](/page/Equivalence%20Relation). The quotient is then given local trivializations by remembering the representative in each chart, and the transition maps between these trivializations are exactly $b \mapsto \rho(g_{ij}(b))$. Since these transition maps are smooth and lie in $\rho(G)$, the quotient is a smooth fibre bundle with structure group contained in the action image. [/proofplan]

[step:Turn the action into smooth transition diffeomorphisms] Let $e_G \in G$ denote the identity element of the Lie group $G$, and let $\operatorname{id}_{F'}:F'\to F'$ denote the identity diffeomorphism of $F'$. Let $\alpha:G\times F'\to F'$ denote the given smooth left action. For each $g \in G$, define the map $\rho(g):F'\to F'$ by $\rho(g)(y)=\alpha(g,y)=g\cdot y$ for $y\in F'$. Because $\alpha$ is a left action, $\rho(g)\circ \rho(h)=\rho(gh)$ for all $g,h\in G$, and $\rho(g^{-1})$ is the inverse diffeomorphism of $\rho(g)$. Hence $\rho:G\to \operatorname{Diff}(F')$ is the action homomorphism. For every $i,j \in I$, define the fibre transition map $\gamma_{ij}:U_i\cap U_j\to \operatorname{Diff}(F')$ by $\gamma_{ij}(b)=\rho(g_{ij}(b))$. The smoothness of $g_{ij}:U_i\cap U_j\to G$ and of $\alpha$ implies that the evaluation map $(U_i\cap U_j)\times F'\to F'$ given by $(b,y)\mapsto \gamma_{ij}(b)(y)=g_{ij}(b)\cdot y$ is smooth. For $b\in U_i\cap U_j\cap U_k$, the cocycle identity for $(g_{ij})$ gives \begin{align*} \gamma_{ij}(b)\circ \gamma_{jk}(b)=\rho(g_{ij}(b)g_{jk}(b))=\rho(g_{ik}(b))=\gamma_{ik}(b). \end{align*} Also $\gamma_{ii}(b)=\rho(e_G)=\operatorname{id}_{F'}$. Thus $(\gamma_{ij})$ is a smooth $\operatorname{Diff}(F')$-valued cocycle. [/step]

[step:Verify that the gluing relation is an equivalence relation]Let $X:=\bigsqcup_{i \in I} U_i \times F'$ be the disjoint union, and write an element of the $i$th summand as $(i,b,y)$ with $b \in U_i$ and $y \in F'$. Define $(i,b,y)\sim(j,c,z)$ exactly when $b=c \in U_i\cap U_j$ and $z=\gamma_{ji}(b)(y)$. Reflexivity follows from $\gamma_{ii}(b)=\operatorname{id}_{F'}$. For symmetry, if $z=\gamma_{ji}(b)(y)$, then \begin{align*} \gamma_{ij}(b)(z)=\gamma_{ij}(b)\gamma_{ji}(b)(y)=\gamma_{ii}(b)(y)=y, \end{align*} so $(j,b,z)\sim(i,b,y)$. For transitivity, suppose $(i,b,y)\sim(j,b,z)$ and $(j,b,z)\sim(k,b,w)$. Then $z=\gamma_{ji}(b)(y)$ and $w=\gamma_{kj}(b)(z)$. Using the cocycle identity with indices $k,j,i$ gives \begin{align*} w=\gamma_{kj}(b)\gamma_{ji}(b)(y)=\gamma_{ki}(b)(y). \end{align*} Hence $(i,b,y)\sim(k,b,w)$.[/step]

[guided]We need the quotient construction to be meaningful, so the first point is to check that the proposed identification is actually an equivalence relation. Let $X:=\bigsqcup_{i \in I} U_i \times F'$, and write points in $X$ as triples $(i,b,y)$, where $b \in U_i$ and $y \in F'$. The relation says that two representatives over the same base point are identified by the transition diffeomorphism: $(i,b,y)\sim(j,b,z)$ exactly when $z=\gamma_{ji}(b)(y)$. Here $e_G \in G$ denotes the identity element of $G$, and $\operatorname{id}_{F'}:F'\to F'$ denotes the identity diffeomorphism of $F'$. Reflexivity asks whether $(i,b,y)$ is identified with itself. Since the cocycle satisfies $g_{ii}(b)=e_G$, we have $\gamma_{ii}(b)=\rho(e_G)=\operatorname{id}_{F'}$. Therefore $\gamma_{ii}(b)(y)=y$, so $(i,b,y)\sim(i,b,y)$. For symmetry, assume $(i,b,y)\sim(j,b,z)$. By definition, $z=\gamma_{ji}(b)(y)$. The cocycle identity gives $\gamma_{ij}(b)\gamma_{ji}(b)=\gamma_{ii}(b)=\operatorname{id}_{F'}$. Applying this identity to $y$ yields \begin{align*} \gamma_{ij}(b)(z)=\gamma_{ij}(b)\gamma_{ji}(b)(y)=y. \end{align*} Thus $(j,b,z)\sim(i,b,y)$. For transitivity, assume $(i,b,y)\sim(j,b,z)$ and $(j,b,z)\sim(k,b,w)$. Then $z=\gamma_{ji}(b)(y)$ and $w=\gamma_{kj}(b)(z)$. Substituting the first equation into the second gives $w=\gamma_{kj}(b)\gamma_{ji}(b)(y)$. The cocycle identity with indices $k,j,i$ says $\gamma_{kj}(b)\gamma_{ji}(b)=\gamma_{ki}(b)$, so $w=\gamma_{ki}(b)(y)$. This is precisely the condition $(i,b,y)\sim(k,b,w)$. Hence $\sim$ is an equivalence relation.[/guided]

[step:Define the projection and local trivializations] Let $q:X\to E:=X/{\sim}$ be the quotient map, and write $[i,b,y]:=q(i,b,y)$. Define $\pi:E\to B$ by $\pi([i,b,y])=b$. This is well-defined because the relation only identifies points with the same base point $b$. For each $i \in I$, define $\Phi_i:\pi^{-1}(U_i)\to U_i\times F'$ by $\Phi_i([j,b,y])=(b,\gamma_{ij}(b)(y))$. This is well-defined: if $[j,b,y]=[k,b,z]$, then $z=\gamma_{kj}(b)(y)$, and hence \begin{align*} \gamma_{ik}(b)(z)=\gamma_{ik}(b)\gamma_{kj}(b)(y)=\gamma_{ij}(b)(y). \end{align*} Define $\Psi_i:U_i\times F'\to \pi^{-1}(U_i)$ by $\Psi_i(b,y)=[i,b,y]$. Then $\Phi_i(\Psi_i(b,y))=(b,y)$, and for $[j,b,y]\in \pi^{-1}(U_i)$, \begin{align*} \Psi_i(\Phi_i([j,b,y]))=[i,b,\gamma_{ij}(b)(y)]=[j,b,y]. \end{align*} Thus $\Phi_i$ is a bijective local trivialization over $U_i$. [/step]

[step:Compute the transition maps and impose the smooth manifold topology]On $U_i\cap U_j$, the change of trivialization $\Phi_i\circ \Phi_j^{-1}:(U_i\cap U_j)\times F'\to (U_i\cap U_j)\times F'$ is given by \begin{align*} \Phi_i\circ \Phi_j^{-1}(b,y)=(b,\gamma_{ij}(b)(y))=(b,g_{ij}(b)\cdot y). \end{align*} This map is smooth because it is the product of the identity map on $U_i\cap U_j$ with the smooth map $(U_i\cap U_j)\times F'\to F'$ given by $(b,y)\mapsto g_{ij}(b)\cdot y$, and that latter map is the composition of $(b,y)\mapsto (g_{ij}(b),y)$ with the smooth action $\alpha:G\times F'\to F'$. Put on $E$ the atlas topology determined by the bijections $\Phi_i$: a subset $W\subset E$ is open exactly when $\Phi_i(W\cap \pi^{-1}(U_i))$ is open in $U_i\times F'$ for every $i\in I$. This topology agrees with the [quotient topology](/page/Quotient%20Topology) induced by $q:X\to E$. Indeed, let $\iota_i:U_i\times F'\to X$ denote the inclusion of the $i$th summand. Since $q\circ \iota_i=\Psi_i$ and $\Phi_i=\Psi_i^{-1}$ on $\pi^{-1}(U_i)$, for every subset $W\subset E$ one has \begin{align*} \iota_i^{-1}(q^{-1}(W))=\Psi_i^{-1}(W)=\Phi_i(W\cap \pi^{-1}(U_i)). \end{align*} By the definition of the disjoint-union topology on $X$, $q^{-1}(W)$ is open in $X$ exactly when all the displayed sets are open in $U_i\times F'$. Hence the atlas topology and the quotient topology coincide. The displayed transition maps are smooth diffeomorphisms, so by the standard smooth atlas construction the charts $\Phi_i$ define a smooth atlas. The sets $\pi^{-1}(U_i)$ cover $E$ because $(U_i)$ covers $B$. This atlas topology is Hausdorff. If $e,e'\in E$ satisfy $\pi(e)\ne \pi(e')$, choose disjoint open neighbourhoods of $\pi(e)$ and $\pi(e')$ in the Hausdorff manifold $B$ and take their inverse images under $\pi$. If $\pi(e)=\pi(e')=b$, choose $i\in I$ with $b\in U_i$; then $e,e'\in \pi^{-1}(U_i)$, and the Hausdorff product manifold $U_i\times F'$ separates $\Phi_i(e)$ and $\Phi_i(e')$. Pulling those separating neighbourhoods back by $\Phi_i$ separates $e$ and $e'$ in $E$. The atlas topology is second countable. Since $B$ is second countable, it is Lindelof. Refine the open cover $(U_i)$ by coordinate domains contained in members of the cover; Lindelof gives a countable subcover, which we denote by $(V_a)_{a\in A}$ with $A$ countable. For each $a\in A$, choose an index $i(a)\in I$ such that $V_a\subset U_{i(a)}$. For each $a\in A$, restrict the already constructed chart to \begin{align*} \Phi_{i(a)}:\pi^{-1}(V_a)&\to V_a\times F'. \end{align*} These restricted charts are charts on the same space $E$; no new quotient is being formed. Since $B$ and $F'$ are second countable, each product $V_a\times F'$ has a countable basis, and the countable union over $a\in A$ of the inverse images of these basis elements under $\Phi_{i(a)}$ is a countable basis for $E$. With this smooth Hausdorff second-countable smooth manifold structure, each $\Phi_i$ is a diffeomorphism onto $U_i\times F'$. In the trivialization $\Phi_i$, the projection $\pi:E\to B$ equals the product projection $U_i\times F'\to U_i$ given by $(b,y)\mapsto b$. Therefore $\pi:E\to B$ is a smooth fibre bundle with fibre $F'$.[/step]

[guided]The point of this step is not only to write down formulas for coordinate changes, but also to verify that those formulas really produce a smooth manifold total space. On $U_i\cap U_j$, the inverse of $\Phi_j$ sends $(b,y)$ to $[j,b,y]$, so applying $\Phi_i$ gives \begin{align*} \Phi_i\circ \Phi_j^{-1}(b,y)=(b,\gamma_{ij}(b)(y))=(b,g_{ij}(b)\cdot y). \end{align*} This map is smooth because $g_{ij}:U_i\cap U_j\to G$ is smooth and the action map $\alpha:G\times F'\to F'$ is smooth. Its inverse is the corresponding transition map with indices reversed, since $\gamma_{ji}(b)=\gamma_{ij}(b)^{-1}$. We now define the topology from the charts and check that it is the quotient topology coming from $q:X\to E$. Declare $W\subset E$ to be open exactly when every $\Phi_i(W\cap \pi^{-1}(U_i))$ is open in $U_i\times F'$. Let $\iota_i:U_i\times F'\to X$ denote the inclusion of the $i$th summand. Since $q\circ \iota_i=\Psi_i$ and $\Phi_i=\Psi_i^{-1}$ on $\pi^{-1}(U_i)$, every subset $W\subset E$ satisfies \begin{align*} \iota_i^{-1}(q^{-1}(W))=\Psi_i^{-1}(W)=\Phi_i(W\cap \pi^{-1}(U_i)). \end{align*} The disjoint-union topology on $X$ says that $q^{-1}(W)$ is open exactly when all these inverse images in the summands are open. Thus the chart-defined topology is exactly the quotient topology. The compatibility computation above shows that these local definitions agree on overlaps. Therefore the charts form a smooth atlas on $E$, and the sets $\pi^{-1}(U_i)$ cover $E$ because the sets $U_i$ cover $B$. Why is $E$ a manifold in the usual sense? First, it is Hausdorff. If two points of $E$ lie over different base points, the Hausdorff property of $B$ gives disjoint base neighbourhoods, and their inverse images under $\pi$ separate the two points. If they lie over the same base point $b$, choose $i$ with $b\in U_i$; then both points are in the same chart $\pi^{-1}(U_i)$, and the Hausdorff property of $U_i\times F'$ separates their chart images. Pulling the separating sets back through $\Phi_i$ separates the original points. Second, it is second countable. Since $B$ is a second-countable smooth manifold, $B$ is Lindelof. For each point of $B$, choose a coordinate domain contained in some member of the original cover $(U_i)$; the resulting coordinate-domain cover has a countable subcover by Lindelofness. Denote this countable subcover by $(V_a)_{a\in A}$, and choose $i(a)\in I$ so that $V_a\subset U_{i(a)}$. We do not replace the quotient space; instead, we restrict the already constructed trivializations: \begin{align*} \Phi_{i(a)}:\pi^{-1}(V_a)&\to V_a\times F'. \end{align*} These restricted charts cover $E$ because the $V_a$ cover $B$. Each product $V_a\times F'$ has a countable basis because both factors are second countable, and the countable union of the inverse images of those basis elements under the restricted charts is a countable basis for $E$. Finally, in each chart $\Phi_i$, the projection $\pi$ becomes the ordinary product projection $(b,y)\mapsto b$. Hence $\pi$ is smooth and locally isomorphic to a product with fibre $F'$, which is exactly the definition of a smooth fibre bundle.[/guided]

[step:Identify the structure group] The transition function over $U_i\cap U_j$ acts on the fibre by $y \mapsto \gamma_{ij}(b)(y)=\rho(g_{ij}(b))(y)$. Thus every fibre-coordinate change belongs to $\rho(G)\subseteq \operatorname{Diff}(F')$. Hence the structure group of the smooth fibre bundle $\pi:E\to B$ is contained in the image of the action homomorphism $\rho:G\to \operatorname{Diff}(F')$. This proves the theorem. [/step]