### Defining and manipulating vector equations with cross and dot products

Hello, I have been experimenting with Sage to see what it can or can't do. Consider the following simple problem.
Show $[ \mathbf{A} \times (\mathbf{B} \times \mathbf{C}) ] + [ \mathbf{B} \times (\mathbf{C} \times \mathbf{A}) ] + [ \mathbf{C} \times (\mathbf{A} \times \mathbf{B}) ] = 0 $ where $\mathbf{A}, \mathbf{B}, \mathbf{C} \in \mathbb{R}^3$. In Sage I can do this in one line

```
eqn = A.cross_product(B.cross_product(C)) + B.cross_product(C.cross_product(A)) + C.cross_product(A.cross_product(B))
```

where A,B and C are elements of $SR^3$. Now I can show component wise `eqn[0].expand()`

`eqn[1].expand()`

`eqn[2].expand()`

that it's zero.
A much simpler way is to use the identity $\mathbf{A} \times ( \mathbf{B} \times \mathbf{C} ) = \mathbf{B}( \mathbf{A} \cdot \mathbf{C} ) - \mathbf{C}( \mathbf{A} \cdot \mathbf{B} )$ and plug it in. Yet this is easier done by hand than by computer.
My question is can Sage do this? Can I define a vector equation in sage, and sub in vector identities to manipulate or simplify the equation?
Thanks