# What form of Leibniz rule is this (principal fiber bundle)?

Let $P(M,G)$ be a principal fiber bundle. Let $\sigma : U \subseteq M \rightarrow P$ be a smooth local section and $f : U \rightarrow G$ a smooth function. For $a \in G$, $R_a : P \rightarrow P$ is the map $u \mapsto u \cdot a$. For $u \in P$, $L_u : G \mapsto P$ is the map $g \mapsto u \cdot g$. Now let $\sigma' = \sigma \cdot f$, $x \in U$ and $X \in T_x M$. Why is

$$\sigma'_{*} (X) = (R_{f(x)})_{*}(\sigma_{*}(X)) + (L_{\sigma(x)})_{*}(f_{*}(X))$$

? My book says it's because of the Leibniz rule, but I don't know of any Leibniz rule that looks like that.

Let $\gamma:(-\varepsilon,\varepsilon)\to M$ be an smooth curve generating $X$, i.e. $\dot{\gamma}(0)=X$. We then write $\sigma(t)$, $f(t)$ for $\sigma(\gamma(t))$, $f(\gamma(t))$ so that by definition we have $$\sigma'_*(X)=\left.\frac{d}{dt}\right|_{t=0}\mu(\sigma(t),f(t)),$$ where $\mu:P\times G\to P$ denotes the $G$-action on $P$. Using the canonical isomorphism $T_{(\sigma(x),f(x))}(P\times G)\to T_{\sigma(x)}P\oplus T_{f(x)}G$, we compute \begin{align}\left.\frac{d}{dt}\right|_{t=0}\mu(\sigma(t),f(t))&=\mu_*(\dot{\sigma}(0),\dot{f}(0))=\mu_*(\dot{\sigma}(0),0)+\mu_*(0,\dot{f}(0))\\&=\left.\frac{d}{dt}\right|_{t=0}\mu(\sigma(t),f(0))+\left.\frac{d}{dt}\right|_{t=0}\mu(\sigma(0),f(t))\\&=\left.\frac{d}{dt}\right|_{t=0}R_{f(x)}(\sigma(t))+\left.\frac{d}{dt}\right|_{t=0}L_{\sigma(x)}(f(t))\\&= (R_{f(x)})_{*}(\sigma_{*}(X)) + (L_{\sigma(x)})_{*}(f_{*}(X))\end{align}