# Proof: Vector Rotation using Quaternions

## Propositions

The Großmann Identity states that

$\mathbf{a} \times (\mathbf{b} \times\mathbf{c}) = (\mathbf{a}\cdot\mathbf{c})\mathbf{b}-(\mathbf{a}\cdot\mathbf{b})\mathbf{c}$

The 3D vector cross-product is anti-commutative

$\mathbf{a}\times\mathbf{b}=-(\mathbf{b}\times\mathbf{a})$

A vector is always orthogonal to its normal

$\mathbf{a}\cdot\mathbf{b}\times\mathbf{a}=0$

A quaternion written in vector form is defined as

$\mathbf{q} = (w, \mathbf{v})$

Quaternion multiplication using vector form is defined as

$\mathbf{q}_1\mathbf{q}_2 = (w_1w_2- \mathbf{v}_1\cdot\mathbf{v}_2, w_1\mathbf{v}_2 + w_2\mathbf{v}_1 + \mathbf{v}_1\times\mathbf{v}_2)$

Since the quaternion we use to rotate a vector is a versor, i.e $$|\mathbf{q}|=1$$, we know that

$w^2 = 1 - \mathbf{v}\cdot\mathbf{v}$

## Efficient vector rotation

The classic text book approach of rotating a vector $$\mathbf{u}\in\mathbb{R}^3$$ by using a versor $$\mathbf{q}=(w, \mathbf{v})$$ embeds the vector $$\mathbf{u}$$ into the augmented quaternion $$\mathbf{p} = (0, \mathbf{u})$$ and determines the rotation by

$\mathbf{p}' = (0, \mathbf{u}') = \mathbf{q}\mathbf{p}\overline{\mathbf{q}}$

However, this approach requires too many multiplications and a much better way is taking apart the expression

$\begin{array}{rl} \mathbf{p}\overline{\mathbf{q}} &= (0,\mathbf{u})(w, -\mathbf{v})\\ &= (\mathbf{u}\cdot\mathbf{v}, w\mathbf{u} - \mathbf{u}\times\mathbf{v}) \end{array}$

From which follows that

$\begin{array}{rl} \mathbf{q}\mathbf{p}\overline{\mathbf{q}} &= (w, \mathbf{v})(\mathbf{u}\cdot\mathbf{v}, w\mathbf{u} - \mathbf{u}\times\mathbf{v})\\ &= (w(\mathbf{u}\cdot\mathbf{v}) - \mathbf{v}\cdot(w\mathbf{u} - \mathbf{u}\times\mathbf{v}), w(w\mathbf{u} - \mathbf{u}\times\mathbf{v}) + (\mathbf{u}\cdot\mathbf{v})\mathbf{v}+ \mathbf{v}\times(w\mathbf{u} - \mathbf{u}\times\mathbf{v}) )\\ &= (0, w^2\mathbf{u} + w\mathbf{v}\times\mathbf{u}+(\mathbf{u}\cdot\mathbf{v})\mathbf{v} + w\mathbf{v}\times\mathbf{u} + \mathbf{v}\times(\mathbf{v}\times\mathbf{u}))\\ &= (0, \mathbf{u} - (\mathbf{v}\cdot\mathbf{v})\mathbf{u}+ 2w\mathbf{v}\times\mathbf{u}+(\mathbf{u}\cdot\mathbf{v})\mathbf{v}+(\mathbf{v}\cdot\mathbf{u})\mathbf{v} - (\mathbf{v}\cdot\mathbf{v})\mathbf{u}\\ &= (0, \mathbf{u} + 2w\mathbf{v}\times\mathbf{u}+2(\mathbf{u}\cdot\mathbf{v})\mathbf{v}- 2(\mathbf{v}\cdot\mathbf{v})\mathbf{u})\\ &= (0, \mathbf{u} + 2w\mathbf{v}\times\mathbf{u} + 2\mathbf{v}\times(\mathbf{v}\times\mathbf{u}))\\ &= (0, \mathbf{u} + w\mathbf{t} + \mathbf{v}\times\mathbf{t}) \end{array}$

with

$\mathbf{t}=2\mathbf{v}\times\mathbf{u}$

Which is a pretty nice finding! We can then rotate a vector $$\mathbf{u}$$ by

$\begin{array}{rl} \mathbf{t}&=2\mathbf{v}\times\mathbf{u}\\ R(\mathbf{u}) &= \mathbf{u} + w\mathbf{t} + \mathbf{v}\times\mathbf{t} \end{array}$