Defining and manipulating vector equations with cross and dot products

savecancel

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