On a theorem on Lie derivatives

I am a little confused proving this theorem (for $p$-forms on $M^n$, $M^n$ is a smooth manifold): $L_X\cdot i_Y-i_Y\cdot L_X=i_{[X,Y]}$ where $X,Y$ are smooth vector fields.

Now it is clear that both sides are anti-derivations, since $L_X$ is a derivation, $i_Y$ and $i_{[X,Y]}$ are anti-derivations.

Now this reduces the problem to proving that the theorem is true for $f\in C^\infty$ and $df$ for such $f$.

It seems to me the the L.H.S is zero for both $f$ and $df$.

For $f$:

L.H.S $=0$ is trivial since $i_Y$ for any zero-form is $0$

for $df$

$$i_Y \, df=df(Y) \implies L_X(i_Y \, df)=L_X(df(Y))$$

And

$$L_X(df)=dL_X(f) \implies i_Y(L_X(df))=L_X(df)(Y)$$

Hence L.H.S. $=0$

Have I made an error here ?

Thanks for any help or pointers.

-
I follow the first part of your question, but I think that since we have that $i_X: \Omega^{n} \to \Omega^{n-1}$ is definition of interior product, the result follows since $i_X df= f$ and since all zero-forms are trivially zero (need it for the Lie algebra) LHS vanishes. –  Jaivir Baweja Jan 30 '13 at 22:58
@JaivirBaweja what makes you think that $i_X df = f$? –  ZulfiqarIII Jan 30 '13 at 23:01
@nonlinearism for $f$ the rhs also vanishes, so that's good. However, $L_X( df(Y) ) \neq L_x(df)(Y)$ (the first one being the Lie derivative of the function $df(Y)$, the second one being the 1-form $L_X(df)$ evaluated at $Y$), so your second conclusion does not hold. –  ZulfiqarIII Jan 30 '13 at 23:03
Why should $(L_X (df))(Y) = L_X (df(Y))$? –  Eric O. Korman Jan 30 '13 at 23:38

As per my comment, $(L_X (df))(Y) \ne L_X (df(Y))$? One way to prove what you want is to use the fact that Lie differentiation satisfies the Leibniz rule with respect to contraction: $$L_X(df(Y)) = (L_X df)(Y) + df L_X Y = i_Y L_X(df) + i_{[X,Y]} df.$$ Subtracting off $i_Y L_X(df)$ gives the right hand side.

-
Thanks Eric, I see my error. –  nonlinearism Jan 31 '13 at 21:14
Let $\alpha$ be a $p$-form, and let $\phi_t$ be the flow along $X$. By definition $$L_X i_Y(\alpha) = \left\{ \dfrac{d}{dt}\phi_t^* (i_Y \alpha) \right\}_{t=0} = \left\{ \dfrac{d}{dt} i_{\phi_t^* Y} (\phi_t^* \alpha) \right\}_{t=0}$$ so by the chain rule and linearity of $Y \mapsto i_Y$ we find $$L_X i_Y(\alpha) = i_{ L_X Y } \alpha + i_Y L_X \alpha.$$ Since $L_X Y = [X,Y]$ this proves the claim.