I wish to prove the identity $$\nabla \cdot (X \times Y) = (\nabla \times X) \cdot Y - X \cdot (\nabla \times Y)$$ where $X, Y$ are vector fields in $\mathbb{R}^3$ and $\times, \cdot$ are the cross, dot product respectively by converting it to the language of differential forms. Letting $X, Y$ correspond to the 1-forms $\omega_1, \omega_2,$ we have $X \times Y = *(\omega_1 \wedge \omega_2), \nabla \cdot = * d *, \nabla \times = * d,$ so $$\nabla \cdot (X \times Y) = *(d(*(*(\omega_1 \wedge \omega_2)) = *d(\omega_1 \wedge \omega_2) = *(d\omega_1 \wedge \omega_2 - \omega_1 \wedge d\omega_2).$$
Thus, we just need to show $(\nabla \times X) \cdot Y$ corresponds to $*(d\omega_1 \wedge \omega_2)$ and the other term will be similar. The best I could do was get it to $(*d\omega_1) \cdot Y = (*d\omega_1)(Y)$ using the fact that $A \cdot B = \omega(B)$ if $A, B$ are vector fields and $\omega$ is the 1-form corresponding to $A.$
Letting $\omega = d\omega_1,$ the claim we need to prove is that $*(\omega \wedge \omega')$ and $(*\omega)(A)$ are equivalent if $A, \omega'$ are. Because both sides are linear, we can just check the case $\omega' = dx_1, A = e_1$ WLOG. But even this seems like too much work because we have to write $\omega = a_1 dx_1 \wedge dx_2 + a_2 dx_2 \wedge dx_3 + a_3 dx_3 \wedge dx_1$ and expand both sides. Is there a faster way to finish the problem that relies on expressing the dot product purely in differential forms (no vector fields)?
It turns out that $*(\omega_1 \wedge *\omega_2) = *(*\omega_1 \wedge \omega_2)$ corresponds to $X \cdot Y.$ Using this on $\nabla \times X = * d \omega_1, Y = \omega_2,$ we get $$(\nabla \times X) \cdot Y = *(**d\omega_1 \wedge \omega_2) = *(d\omega_1 \wedge \omega_2).$$