linear algebra - Is there a slick proof for the identity that expresses the inner product of imaginary octonions in terms of the cross product?

Consider the octonions $\mathbb O$ and in particular their imaginary part $\operatorname{Im}\mathbb O$. Let $(-,-)$ be the scalar product induced by the identification of the imaginary octonions with $\Bbb R^7$. Furthermore, define the cross product of (any) octonions by $x\times y:= \frac{1}{2}(xy-yx)$. For imaginary octonions $x,y$, there is the nice identity $x\times y=(x,y)+x\cdot y$, where the dot denotes octonion multiplication.

Define the linear map $L_{x,y}:\operatorname{Im}\mathbb O\to \operatorname{Im}\mathbb O$ by $L_{x,y}(v)=x\times (y\times v)$, where $x,y$ are also imaginary quaternions. It is easy to prove by explicit calculation (plugging in a basis) that there is the following identity:

$$(x,y)=-\frac{1}{6}\operatorname{tr}L \qquad \qquad x,y\in \operatorname{Im}\mathbb O$$

This identity is useful because it shows that octonion multiplication of imaginary octonions only depends on the cross product, and thereby yields the equivalence of two common definitions of the exceptional Lie group $G_2$. I don't like the brute force proof, so I am left wondering whether there is a better way to see that this identity holds. Is anyone aware of a slick(er) proof?

EDIT: It was just pointed out to me by Ted Shifrin that $\operatorname{tr}L$ is the would-be Killing form on $\Bbb R^7$ seen as an (almost-but-not-quite) Lie algebra (equipped with the cross product). This might point the way towards a nice proof (?)

Answer

Since $L_{x,y}$ is linear in $x$ and $y$, it suffices to compute the trace in two cases: when $x$ and $y$ are parallel and when they are perpendicular (assuming $x$ and $y$ have norm $1$ as well).

In the first case, it's just the square of $L_x=x\times-$, which annihilates $x$ and equals multiplication by $x$ on its orthogonal complement, so $L_{x,x}$ will be multiplication by negative one on $x$'s orthogonal complement; the trace is obviously $-6$.

In the second case, $L_{x,y}$ annihilates $y$ and $xy$, sends $x$ to $y$, and $z\perp xy \Rightarrow x\perp yz$, implying

$$\langle L_{x,y}z,z\rangle=\langle x(yz),z\rangle=\langle yz,\bar{x}z\rangle=\langle y,\bar{x}\rangle|z|^2=0$$

when $z\perp \{x,y,xy\}$, thus $L_{x,y}$ is skew-hermitian on $\{x,y,xy\}^\perp$ hence has trace zero.