[proofplan] Fix $p \in P$ and compare the orbit map $\rho_p: G \to P$ with the fibre $\nu^{-1}(\nu(p))$. The principal bundle axioms imply that $\rho_p$ parametrizes exactly this fibre, and a local principal trivialization shows that this parametrization is a diffeomorphism onto the fibre as an embedded submanifold. Differentiating at the identity identifies $T_eG = \mathfrak g$ with the tangent space to the fibre at $p$, which is precisely the vertical space $\ker d\nu_p$. [/proofplan] [step:Show that the orbit map parametrizes the fibre through $p$] Fix $p \in P$, and set $m := \nu(p) \in M$. Define the orbit map \begin{align*} \rho_p: G \to P, \quad g \mapsto p \cdot g. \end{align*} Because the right $G$-action on $P$ is fibre-preserving, we have $\nu(p \cdot g) = \nu(p) = m$ for every $g \in G$, so $\operatorname{im}\rho_p \subseteq \nu^{-1}(m)$. Conversely, since $\nu: P \to M$ is a principal $G$-bundle, the right action of $G$ on each fibre is transitive. Thus, for every $q \in \nu^{-1}(m)$, there exists $g \in G$ such that $q = p \cdot g$. Hence \begin{align*} \operatorname{im}\rho_p = \nu^{-1}(m). \end{align*} The same principal bundle axiom gives freeness of the action on the fibre: if $p \cdot g = p \cdot h$, then $g = h$. Therefore $\rho_p: G \to \nu^{-1}(m)$ is bijective. [/step] [step:Use a principal trivialization to identify the orbit map as a diffeomorphism onto the fibre] Choose an open neighbourhood $U \subset M$ of $m$ and a smooth principal trivialization \begin{align*} \Phi: \nu^{-1}(U) \to U \times G \end{align*} Let $\operatorname{pr}_1:U\times G\to U$ denote the first projection. The trivialization satisfies $\operatorname{pr}_1 \circ \Phi = \nu$ and $\Phi(q \cdot g) = (\operatorname{pr}_1(\Phi(q)), a(q)g)$, where $a: \nu^{-1}(U) \to G$ is the second component of $\Phi$. Since $p \in \nu^{-1}(U)$, write $\Phi(p) = (m, g_p)$ for the uniquely determined element $g_p \in G$. For every $g \in G$, \begin{align*} \Phi(\rho_p(g)) = \Phi(p \cdot g) = (m, g_pg). \end{align*} Thus, under the chart $\Phi$, the map $\rho_p: G \to \nu^{-1}(m)$ is identified with the smooth map \begin{align*} G \to \{m\} \times G, \quad g \mapsto (m, g_pg). \end{align*} Left multiplication by $g_p$ is a diffeomorphism of $G$, so this map is a diffeomorphism from $G$ onto $\{m\} \times G$. Transporting by the trivialization $\Phi$ shows that \begin{align*} \rho_p: G \to \nu^{-1}(m) \end{align*} is a diffeomorphism onto the fibre, viewed as the embedded submanifold $\Phi^{-1}(\{m\} \times G)$ of $P$. [guided] The point of introducing a trivialization is to avoid treating the fibre only as a set. We need a smooth statement: the orbit map must identify the Lie group $G$ with the fibre as a smooth submanifold of $P$. Choose an open neighbourhood $U \subset M$ of $m := \nu(p)$ and a smooth principal trivialization \begin{align*} \Phi: \nu^{-1}(U) \to U \times G. \end{align*} This means $\operatorname{pr}_1 \circ \Phi = \nu$, so the fibre over $m$ is carried by $\Phi$ onto $\{m\} \times G$. It also means that the trivialization respects the right action: if the second component of $\Phi(q)$ is denoted by $a(q) \in G$, then \begin{align*} \Phi(q \cdot g) = (\nu(q), a(q)g). \end{align*} Since $p \in \nu^{-1}(U)$, there is a unique $g_p \in G$ such that \begin{align*} \Phi(p) = (m, g_p). \end{align*} For each $g \in G$, the equivariance of the trivialization gives \begin{align*} \Phi(\rho_p(g)) = \Phi(p \cdot g) = (m, g_pg). \end{align*} Thus, in the product coordinates supplied by $\Phi$, the orbit map is just \begin{align*} G \to \{m\} \times G, \quad g \mapsto (m, g_pg). \end{align*} This is smooth, and its inverse is \begin{align*} \{m\} \times G \to G, \quad (m, h) \mapsto g_p^{-1}h. \end{align*} Therefore the orbit map is a diffeomorphism from $G$ onto the fibre $\nu^{-1}(m)$ with its embedded submanifold structure. This is the smooth input needed before differentiating: the derivative of $\rho_p$ at $e$ identifies $T_eG$ with the tangent space to that fibre at $p$. [/guided] [/step] [step:Identify the tangent space to the fibre with the vertical tangent space] In the local principal trivialization above, $\nu$ is represented by the projection $U\times G\to U$, hence $\nu$ is a submersion. Therefore the fibre $\nu^{-1}(m)$ is an embedded level submanifold, and its tangent space at $p$ is \begin{align*} T_p(\nu^{-1}(m)) = \ker(d\nu_p). \end{align*} By definition, $\ker(d\nu_p) = V_pP$. Therefore \begin{align*} T_p(\nu^{-1}(m)) = V_pP. \end{align*} [/step] [step:Differentiate the orbit parametrization at the identity] Since $\rho_p: G \to \nu^{-1}(m)$ is a diffeomorphism and $\rho_p(e) = p$, its differential at the identity element $e \in G$ is a linear isomorphism \begin{align*} d(\rho_p)_e: T_eG \to T_p(\nu^{-1}(m)). \end{align*} Using $T_eG = \mathfrak g$ and $T_p(\nu^{-1}(m)) = V_pP$, this becomes a linear isomorphism \begin{align*} d(\rho_p)_e: \mathfrak g \to V_pP. \end{align*} By the definition of the fundamental vector field, for every $\xi \in \mathfrak g$, \begin{align*} d(\rho_p)_e(\xi) = (\xi_P)_p. \end{align*} Hence the map \begin{align*} \mathfrak g \to V_pP, \quad \xi \mapsto (\xi_P)_p \end{align*} is a linear isomorphism. This proves the theorem. [/step]