Product rule for vector bundle (Leibniz rule)

Question

Let $\pi:E\to Y$ be a vector bundle. Write $\mathrm{T}(E/Y)\subset \mathrm TE$ for its vertical bundle. Write $\delta:\mathrm{T}(E/Y)\cong \pi^\ast E:\ell$ for the vector bundle isomorphisms over $E$ given fiberwise by the canonical isomorphisms between a vector space and its tangent space at a point.

Trying to carry over the product rule for differentiable maps between vector spaces, I have arrived at the following "formula", where $f\in C^\infty_Y$ is a real function, $s$ is a local section of $\pi$, and $+_\mathrm{T},\cdot_\mathrm{T}$ are the addition and scalar multiplication of the secondary vector bundle structure $\mathrm TE\to \mathrm TY$. $$\mathrm T_y(f\cdot s)(\dot\beta)\overset{?}{=}(f\circ \beta)^\prime(0)\cdot \overbrace{\ell(sy,sy)}^{\in \mathrm T_{sy}\pi^{-1}(y)}\overset{?}{+_\mathrm{T}}\overbrace{f(y)\cdot_{\mathrm T}\mathrm T_ys(\dot\beta)}^{\in \mathrm T_{f(y)s(y)}E}$$

Question 1. Is this formula correct? If so, the RHS lies in $\mathrm T_{(1+f(y))s(y)}E$, which looks a bit strange...

Question 2. For differentiable maps between vector spaces, the product rule is a consequence of the chain rule along with the additional structures of sums and powers. Is there a coordinate free way of arriving at this formula?

Added. I think the correct formula is $$\mathrm T_y(f\cdot s)(\dot\beta)\overset{?}{=}(f\circ \beta)^\prime(0)\cdot \overbrace{\ell(fysy,sy)}^{\in \mathrm T_{fysy}\pi^{-1}(y)}+\overbrace{f(y)\cdot_{\mathrm T}\mathrm T_ys(\dot\beta)}^{\in \mathrm T_{fysy}E},$$ but I'm not sure how to prove it.

Answer 1

Your formula is not right as stated: As you notices, the RHS should not lie in the tangent space of $E$ at the point $(1+f(y))s(y)$ but in the tangent space at $f(y)s(y).$ You can derive a correct formula as follows: For a fixed scalar $\lambda\in\mathbb K$ consider the diffeomorphism $$\lambda\colon E\to E,$$ and the induced differential $$D\lambda\colon TE\to TE.$$ Note that $D\lambda$ maps the vertical space $V_vE$ at $v\in E$ to the vertical space at $\lambda v\in E.$ Then, if $f$ is constant, set $\lambda=f$ and obtain $$D (fs)(\delta')=Df\circ Ds(\delta').$$ This should correspond to the second summand on the right hand side.

Next, consider a scalar curve $\lambda(t)$, and the corresponding curve $$\lambda(t) v.$$ It's derivative (at $t=0$) is a vertical tangent vector at $\lambda(0)v\in E$ which (identifying the vertical tangent space $V_vE$ with the fiber $E_{\pi(v)}$) is given by $\lambda'(0) v.$ This should correspond to the first summand in the formula.

Applying the chain rule to $$M\to M\times \mathbb K,\, p\mapsto (p,f(p))$$ and $$M\times \mathbb K\to E; (p,\lambda)\mapsto \lambda s(p)$$ you obtain the desired formula.