# Proving $[\mathcal{L}_X, \iota_Y] = \iota_{[X,Y]}$ using only Cartan's formula

I'm aware of some related questions on this site, e.g., this question, but my following query is somewhat distinct. I also know I only need to prove the relation $$[\mathcal{L}_X, \iota_Y] = \iota_{[X,Y]}$$ for a function $$f$$ and an exact 1-form $$df$$, since the interior product is an antiderivation, as was done in that post. However, for my own sake I wanted to show the equality for an arbitrary $$p$$-form $$\alpha = a_I dx^I$$ (with multi-index $$I$$) with a brute-force application of Cartan's formula $$\mathcal{L}_X = \iota_X \circ d + d \circ \iota_X$$, and after expanding all my terms, ended up with the following: $$[\mathcal{L}_X, \iota_Y] \alpha = a_I \Big(\iota_X \circ d \circ \iota_Y - \iota_Y \circ d \circ \iota_X + d \circ \iota_X \circ \iota_Y \Big) dx^I$$ The problem term I'm finding is mainly $$a_I d \circ \iota_X \circ \iota_Y dx^I = a_{i_1 \dots i_p} d \circ \iota_X \circ \iota_Y dx^{i_1} \wedge\dots dx^{i_p}.$$ Since this term is trivially zero if $$\alpha$$ is a 1-form, I'm tempted to believe it should be zero for any $$p$$-form. However, I am having trouble seeing how to show this. Is this true generally? Or does it cancel non-trivial contributions from the other terms when $$\alpha$$ is not a zero or one form?

• Did you include the derivatives on $a_I$? Jan 6, 2021 at 1:57
• @Keshav yes, I first expanded the LHS as $\iota_X d \iota_Y + d \iota_X \iota_Y - \iota_Y \iota_X d - \iota_Y d \iota_X$ and then just applied each operation successively. All derivatives of the $a_I$ cancelled. I also expected this since the RHS does not contain any derivatives.
– user488914
Jan 6, 2021 at 5:27