I've recently begun reading up on differential forms in a physics context, and my resources said that one can often derive vector identities from differential forms.
For instance,
$\nabla \cdot (\nabla \times F)=0$ and $\nabla \times (\nabla F)=0$ both follow from $\text{dd}=0$, where $\text{d}$ is the exterior derivative.
$A\cdot (B\times C)=B\cdot (C\times A)=C\cdot (A\times B)$ follows from $A \wedge B \wedge C=B \wedge C \wedge A=C \wedge A \wedge B$, where $\wedge$ is the wedge product.
$\nabla \cdot (A\times B)=B\cdot (\nabla\times A)-A\cdot(\nabla\times B)$ follows from the product rule for the exterior derivative: $d(A\wedge B)=dA\wedge B + (-1)^P A\wedge dB$ (where $P$ is the degree of $A$).
I tried deriving the infamous BAC-CAB rule, $A\times(B\times C)= B(A\cdot C) - C(A\cdot B)$, in this mode, but I couldn't get too far.
I would think the relevant expression in the language of differential forms should perhaps be $*(A\wedge *(B\wedge C)) = (B\wedge (A\lrcorner C) - C\wedge (A\lrcorner B))$, but I'm not sure. (Where $*$ is the Hodge star operator and $\lrcorner$ is the interior product).
Does anyone have some insight to share on deriving this identity or others from differential forms? Thanks!
Proving identities with geometric algebra (which subsumes differential forms):
Let $\langle A \rangle_n$ denote the grade-$n$ projection of a multivector $A$. For example, let $A = a + b \wedge c + d \wedge e \wedge f$. Then the grade-2 project is $\langle A \rangle_2 = a \wedge b$.
What geometric algebra has that differential forms does not is the geometric product, which marries the dot and wedge products. On two vectors $a$, $b$, the geometric product takes the form $ab$, which is
$$ab \equiv a \cdot b + a \wedge b$$
Like the wedge product, the geometric product is associative, but the vectors neither strictlly commute nor strictly anticommute in general.
We handle the Hodge dual by geometric product multiplication by the pseudoscalar $i = \hat x \wedge \hat y \wedge \hat z$. That is,
$$\star a = ia$$
For any vector $a$.
Using grade projection and the geometric product, it is quite easy to prove some of these identities. To prove the BAC-CAB rule, take $\langle abc \rangle_1$.
$$\langle a(bc) \rangle_1 = a \cdot (b \wedge c) + a (b \cdot c)$$
This groups the $(bc)$ vectors together. (nb. the "dot" product of a vector and a bivector is a vector. $a \cdot (b \wedge c)$ is a vector lying in the plane $b \wedge c$ orthogonal to $a$). But by associativity, we can group the $(ab)$ vectors together.
$$\langle (ab)c \rangle_1 = (b \cdot a) c + (a \wedge b) \cdot c$$
Since $(ab)c = a(bc)$, this generates an equation looking like
$$a \cdot (b \wedge c) + a(b \cdot c) = c(a \cdot b) + (a \wedge b) \cdot c$$
So we have the CAB part, but not the BAC part. Notice we have $a (b \cdot c)$ that we want to cancel. To do this, let's try $bca$.
$$\begin{align*} \langle bca \rangle_1 &= a(b \cdot c) + (b \wedge c) \cdot a \\ &= b (a \cdot c) + b \cdot (c \wedge a)\end{align*}$$
We can use this to subtract the top equation from the left and the bottom from the right to get:
$$2a \cdot (b \wedge c) = c (a \cdot b) - b(a \cdot c) + (a \wedge b) \cdot c - b \cdot (c \wedge a)$$
Not done yet. Let's look at one more expansion, of $cab$.
$$\begin{align*} \langle cab \rangle_1 &= (c \cdot a)b + (c \wedge a) \cdot b \\ &= c(a \cdot b) + c \cdot (a \wedge b)\end{align*}$$
Put all of these on one side of an equals sign, and you can cancel out the terms we don't want, yielding
$$2a \cdot (b \wedge c) = 2c(a \cdot b) - 2 b(a \cdot c)$$
This is the proper form of the BAC-CAB rule (within a factor of 2). The usual form can be recovered by $b \wedge c = i (b \times c)$.
Honestly, doing it this way is pretty onerous. I've done it several times, and breaking it down into components is a lot less tedious. One of the few times I've found that to be the case. Nevertheless, using associativity of the geometric product and grade projection is something I rely on heavily to derive useful identities or simplify expressions. It's just a pity that traditional differential forms lacks these very useful tools from clifford algebra.