Coordinate free proof for $a\times (b\times c) = b(a\cdot c) - c(a\cdot b)$ The vector triple product is defined as $\mathbf{a}\times (\mathbf{b}\times \mathbf{c})$. This is often re-written in the following way:
\begin{align*}\mathbf{a}\times (\mathbf{b}\times \mathbf{c}) = \mathbf{b}(\mathbf{a}\cdot\mathbf{c}) - \mathbf{c}(\mathbf{a}\cdot\mathbf{b})\end{align*}
This is a very useful identity for integrating over vector fields and so on (usually in physics).
Every proof I have encountered splits the vectors into components first. This is understandable, because the cross product is purely a three dimensional construct. However, I'm curious as to whether or not there is a coordinate free proof of this identity. Although I don't know much differential geometry, I feel that tensors and so on may form a suitable framework for a coordinate free proof.
 A: Since $b\times c$ is normal to the plane $b,\,c$ span, $a\times (b\times c)$, which is orthogonal to this vector, is in said plane. The coefficients $B,\,C$ for which the result is $Bb+Cc$ are invariant under rotations, and clearly $B$ must be linear in $a,\,c$ while $C$ is linear in $a,\,b$, so constants $B',\,C'$ exist with $a\times (b\times c) =B'  (a\cdot c) b + C'  (a\cdot b) c$. Since the left-hand side is antisymmetric, $C'=-B'$. Since $B'$ must be a constant (since both sides are linear in each vector), we can use any vectors we like for which both sides are non-zero to compute $B'$. Example: $a=b=i,\,c=j$ so $a\times (b\times c) = i\times k = -j$ and $(a\cdot c) b - (a\cdot b) c = -j$ as required.
A: Okay, I really hate the sign issues with the Hodge star, so I am gonna assume that $\star\star=1$, the end result will be good.
The fundamental relationship is that for $k$-vectors/forms, we have $\langle\omega,\eta\rangle\mu=\omega\wedge\star\eta$, where the angle brackets are the inner product on the exterior algebra and $\mu$ is the volume form/multivector.
Let's start with $x$ being an arbitrary vector and taking a look at $$ \langle x,a\times(b\times c)\rangle\mu=\langle x,\star(a\wedge\star(b\wedge c))\rangle\mu= \\=x\wedge(a\wedge\star(b\wedge c))=(x\wedge a)\wedge\star(b\wedge c)= \\=\langle x\wedge a,b\wedge c\rangle\mu=\det\left(\begin{matrix}\langle x,b\rangle & \langle x,c\rangle \\ \langle a,b\rangle & \langle a,c\rangle\end{matrix}\right)\mu= \\=(\langle x,b\rangle \langle a,c\rangle-\langle x,c\rangle \langle a,b\rangle)\mu, $$ comparing the LHS with the RHS we can "divide" (ofc not really divide) by $\mu$ since the coefficients need to agree, and because $x$ was arbitrary, and the inner product is nondegenerate, we can  "" divide ""  by $x$ and we have $$ a\times(b\times c)=b\langle a,c\rangle-c\langle a,b\rangle. $$
A: Let $\mathbf{a}$, $\mathbf{b}$, $\mathbf{c}$ be vector fields on $\mathbb{R}^{3}$ (we could extend to $\mathbb{R}^{n}$ if we wish!), considered as a Riemannian manifold equipped with metric $g$ and induced Hodge map $\star$. Let $\mathbf{a}$, $\mathbf{b}$, $\mathbf{c}$ have corresponding vector field representations $U,V,W$ on $\mathbb{R}^{n}$ respectively. Then
$$\begin{align}
\mathbf{a}\times(\mathbf{b}\times \mathbf{c}) \,\equiv\,  \star(\widetilde{U} \wedge \star(\widetilde{V} \wedge \widetilde{W})) 
\end{align}$$
where $\widetilde{X}$ denotes the metric dual of $X$ (i.e. $\widetilde{X}=g(X,-)$) and the equivalence is up to metric dual. Then
$$\begin{align}
\star(\widetilde{U} \wedge \star(\widetilde{V} \wedge \widetilde{W})) &\,=\, \star(\widetilde{U} \wedge i_{W}\star \widetilde{V}) \,=\, \star (  i_{W}\widetilde{U} \wedge \star \widetilde{V} -  i_{W} (\widetilde{U}\wedge \star \widetilde{V})) \\
&\,=\, (i_{W}\widetilde{U})\star\star \widetilde{V} - \star i_{W}(\widetilde{U}\wedge\star \widetilde{V}) \\
&\,=\, g(U,W)\widetilde{V}  - \star(\widetilde{U}\wedge\star \widetilde{V}) \wedge \widetilde{W} \\
&\,=\, g(U,W)\widetilde{V} - g(U,V)\widetilde{W}
\end{align}$$
where $i_{X}$ denotes the interior derivative with respect to $X$ and we have used the identities:
$$\begin{align}
\star\star \alpha &\,=\, \alpha \\[0.2cm]
\star(\widetilde{X}\wedge\star\widetilde{Y}) &\,=\, g(X,Y) \\[0.2cm]
\star(\alpha \wedge \widetilde{X}) &\,=\, i_{X}\star \alpha \\[0.2cm]
\widetilde{X} \wedge \star\alpha &\,=\, (-1)^{p+1}\star i_{W}\alpha
\end{align}$$
for any $p$-form $\alpha$ and vector fields $X,Y$ (note that the first and second identities are specific to $\mathbb{R}^{3}$). Then note that 
$$g(U,W)\equiv \mathbf{a}\cdot\mathbf{c}\quad\text{and}\quad g(U,V)\equiv\mathbf{a}\cdot\mathbf{b}$$
and so then the result follows after taking the metric dual of our expression.
A: I just want to add a proof using my favourite method for this kind of thing: Penrose graphical notation. I think it is as coordinate free as you can go.
Every piece of the diagram has a meaning. Tensors are shapes with a lines going upwards or downwards, depending on the type of tensor. For example, vectors have 1 line going upwards, and covectors one line going downwards.
Contracion is represented joining the lines.
For example: the first line on the right side, over the word "proof", is the statement $(b\times c)^{a} = b^{b}c^{c}g_{bd}g_{ce}\epsilon^{dea} = b^{b}c^{c}\epsilon_{bcd}g^{da}$ where the indices are proper abstract indices: they do not represent components, but the slots of the tensors.
At the bottom I repeat the properties I use.



*Antisymmetry of $\epsilon^{abc}$

*$\epsilon^{abc}\epsilon_{def} = \delta^{abc}_{def}$

*$\delta^{abc}_{dec} = \delta^{ab}_{de}$

*$\delta^{ab}_{cd}A_{ab} = 2A_{[cd]} = A_{cd} - A_{dc}$

A: Adapted from my previous proof of $\nabla \times (\vec{A} \times \vec{B})$:
\begin{align}
     \vec a \times (\vec b \times \vec c)
 & = a_l \hat{e}_l \times (b_i c_j \hat{e}_k \epsilon_{ijk}) \\
 & = a_l b_i c_j \epsilon_{ijk} \underbrace{ (\hat{e}_l \times \hat{e}_k)}_{(\hat{e}_l \times \hat{e}_k) = \hat{e}_m \epsilon_{lkm} } \\
 & = a_l b_i c_j \hat{e}_m \underbrace{\epsilon_{ijk} \epsilon_{mlk}}_{\text{contracted epsilon identity}} \\
 & = a_l b_i c_j \hat{e}_m \underbrace{(\delta_{im} \delta_{jl} - \delta_{il} \delta_{jm})}_{\text{They sift other subscripts}} \\
 & = a_j (b_i c_j \hat{e}_i) - a_i (b_i c_j \hat{e}_j) \\
 & = (b_i \hat{e}_i) (a_j c_j) - (c_j \hat{e}_j) (a_i b_i) \\
 & = \vec b (\vec a\cdot\vec c) - \vec c(\vec a\cdot \vec b)
\end{align}
A: We can do this by using the definition of the cross product as an bilinear map $V \times V \to V$. We also take as a basic property that it is orthogonal to each of its arguments,
$$ a \cdot (a \times b) = b \cdot (a \times b) = 0 \tag{Orth} $$
 We need another property to fix the scaling; the easiest one is that the magnitude of $a \times b$ is the area of the parallelogram spanned by $a$ and $b$. This effectively means that
$$ (a \times b) \cdot (a \times b) = (a \cdot a)(b \cdot b) - (a \cdot b)^2 \tag{Area} $$
(If this looks opaque, you might prefer to start with perpendicular $a$ and $b$, then extending with bilinearity.)
(A) and $v \cdot v = 0 \implies v = 0 $ force that 
$$a \times a = 0, \tag{Alt} $$
(alterating) and expanding $(a+b) \times (a+b)$ and using this implies that 
$$a \times b = - b \times a : \tag{AntiSym} $$
the cross product must be antisymmetric.
The scalar triple product is $[a,b,c] = a \cdot (b \times c)$. It is trilinear since both products are bilinear, and it is also zero when two arguments are equal, by (Orth) and (Alt):
$$ [a,a,b] = [a,b,a] = [b,a,a] = 0 $$
Using linearity on $[a+b,a+b,c]$ implies that further $[a,b,c] = -[b,a,c]$, and combining this with the inherited antisymmetry in the last two arguments from $\times$, we find that
$$ [a,b,c] = [b,c,a] = [c,a,b] = -[b,a,c] = -[a,c,b] = -[c,b,a] , $$
and in particular,
$$ a \cdot (b \times c) = (a \times b) \cdot c : $$
we can swap the position of the dot and the cross.
We can now derive a restricted form of the triple product identity: using linearity on (Area), we have
$$ 0 = ((a + b) \times c) \cdot ((a+b) \times c) + ((a+b) \cdot c)^2 - (a+b) \cdot (a+b))(c \cdot c) \\
= \dotsb = 0 + 0 + (a \times c) \cdot (b \times c) + (a \cdot c)(b \cdot c) - (a \cdot b)(c \cdot c) . $$
Switching the dot and the cross in the first term, we find that
$$ 0 = a \cdot ( c \times (b \times c) + (b \cdot c)c - (c \cdot c)b ) $$
But $a$ is arbitrary here, so
$$ c \times (c \times b) = (b \cdot c)c - (c \cdot c)b . \tag{R} $$
We can derive a couple more identities that are true in general, but now we can cheat and use that we are in three dimensions, so we can expand $a = \lambda b + \mu c + \nu (b \times c)$. Then using linearity, (R) and linearity again,
$$ a \times (b \times c) = \lambda (b \times (b \times c)) + \mu ( c \times b \times c ) \\ = \lambda( (c \cdot b)b - (b \cdot b)c ) + \mu ( (c \cdot c)b - (b \cdot c)c ) \\
= ((\lambda b + \mu c) \cdot c)b - ((\lambda b + \mu c) \cdot c)b $$
Finally, we can add the $\nu (b \times c)$ part back into both dot products, since it is orthogonal to $b$ and $c$, which gives
$$ a \times (b \times c) = (a \cdot c)b - (a \cdot b)c $$
as expected.
