I'm reviewing my understanding on derivative on Banach spaces. Could you please verify if it looks fine or contains logical gaps/errors? Thank you so much for your help!
Suppose that $E,F$ are Banach spaces and that $f:E \to F$ is differentiable on $E$. For $a, v \in E$, we define a map $$\begin {array}{l|rcl} g & \mathbb R & \longrightarrow & F \\ & t & \longmapsto & f(a+tv) \end{array}$$
Compute $\partial g (t)$.
My understanding:
By the definition of total derivative, we have $\partial f (x) \in \mathcal L(E,F)$, i.e. $$\begin {array}{l|rcl} \partial f (x) & E & \longrightarrow & F \\ & y & \longmapsto & \partial f (x) (y) \end{array}$$
Here $\partial f (x) (y)$ denotes the value of the map $\partial f (x)$ when evaluated at $y$. Hence $\partial f (x) (y)$ is not the arithmetic product of $\partial f (x)$ and $y$.
Consider the map $$\begin {array}{l|rcl} h & \mathbb R & \longrightarrow & E \\ & t & \longmapsto & a+tv \end{array}$$
It follows that $$\begin {array}{l|rcl} \partial h(t) & \mathbb R & \longrightarrow & E \\ & l & \longmapsto & lv \end{array}$$
It follows from $g = f \circ h$ and the chain rule that $\partial g (t) = \partial f (h(t)) \circ \partial h(t)$. This means $$\begin {array}{l|rcl} \partial g(t) & \mathbb R & \longrightarrow & F \\ & l & \longmapsto & \partial f(a+tv)(lv) \end{array}$$ and consequently $$\forall t,l \in \mathbb R:\partial g(t) (l) = \partial f(a+tv)(lv)$$
It follows from $\partial f(a+tv)$ is a linear map that $$\forall t,l \in \mathbb R:\partial g(t) (l) = \Big(\partial f(a+tv)(v)\Big) \cdot l$$
Here $\Big(\partial f(a+tv)(v)\Big) \cdot l$ denotes the arithmetic product of $\partial f(a+tv)(v)$ and $l$.
By the the definition of directional derivative, we have $$\forall t,l \in \mathbb R:\partial g(t) (l) = \Big(D_v f(a+tv)\Big) \cdot l$$
Here $\Big(D_v f(a+tv)\Big) \cdot l$ denotes the arithmetic product of $D_v f(a+tv)$ and $l$.
I don't think you've told us the question you're trying to solve. But it seems that you have written some map $g:\mathbb R \to F$ as a composition $$ g = f \circ h$$ and are trying to apply chain rule. Note that the functions are related to the spaces like
$$\mathbb R \xrightarrow{h} E \xrightarrow{f} F$$ in particular, $\partial h$ has no reason to care about $F$. It should be $$\partial h : \mathbb R\to L(\mathbb R,E)$$ or $$ \partial h(t) : \mathbb R \to E.$$
The chain rule is then correctly applied, if I understand your yet undefined symbols correctly, but I would advise against using the symbol $l$ for a parameter and then writing it as if its a linear map $l(\dots)$.
PS: following the discussion on Meta here: The problem with proof verification I think it would be better if in the future, you posted your solution as an answer to your own question.