# Maths - Rotations

This proof was kindly provided by William Lupton

# Introduction

Write sin(heading)=S1, cos(heading)=C1, attitude=(S2, C2), bank=(S3, C3) and sin(heading/2)=s1 etc.

Require to prove:

e0 = c1c2c3 + s1s2s3 = sqrt(1 + C1C2 + C2C3 + C3C1 + S1S2S3) / 2

e1 = c1c2s3 - s1s2c3 = (C1S3 + C2S3 - S1S2C3) / 4e0

e2 = c1s2c3 + s1c2s3 = (S1S3 + C1C3S2 + S2) / 4e0

e3 = s1c2c3 - c1s2s3 = (C2S1 + C3S1 - C1S2S3) / 4e0

# Lemmas

To begin with, some lemmas.

## Lemma 1

C1C2          = (2c1c1 - 1)(1 - 2s2s2)

= 2c1c1 - 4c1c1s2s2 - 1 + 2s2s2

C1C2 + C2C3 + C3C1

= 2sum(cici + sisi) - 3 - 4sum(cicisisi)

= 3 - 4sum(cicisisi)

## Lemma 2

prod(cici) + prod(sisi)

= prod(cici) + prod(1 - cici)

= prod(cici) + 1 - sum(cici) + sum(cicicjcj) - prod(cici)

= 1 - sum(cici(1 - cjcj))

= 1 - sum(cicisjsj)

## Lemma 3

c1c1c2c2 - s1s1s2s2

= c1c1(1 - s2s2) - (1 - c1c1)s2s2

= c1c1 - s2s2

## Lemma 4

c1c1 + s3s3 - 2c1c1s3s3

= c1c1(c3c3 + s3s3) + s3s3(c1c1 + s1s1) - 2c1c1s3s3

= c1c1c3c3 + s1s1s3s3

# Proofs

## e0

4e0e0(RHS)        = 1 + C1C2 + C2C3 + C3C1 + S1S2S3

= 1 + (3 - 4sum(cicisisi)) + 8c1c2c3s1s2s3 (Lemma 1)

= 4(1 - sum(cicisisi) + 2c1c2c3s1s2s3)

e0e0(LHS)        = (c1c2c3 + s1s2s3)(c1c2c3 + s1s2s3)

= prod(cici) + 2c1c2c3s1s2s3 + prod(sisi)

= 1 - sum(cicisjsj) + 2c1c2c3s1s2s3 (Lemma 2)

## e1

4e0e1(RHS)     = (2c1c1-1).2s3c3 + (1-2s2s2).2s3c3 - 2s1c1.2s2c2.C3

= 4(s3c3(c1c1 - s2s2) - c1c2s1s2.C3)

e0e1(LHS)     = (c1c2c3 + s1s2s3)(c1c2s3 - s1s2c3)

= c1c1c2c2c3s3 - c1c2c3c3s1s2 + c1c2s1s2s3s3 - c3s1s1s2s2s3

= c3s3(c1c1c2c2 - s1s1s2s2) - c1c2s1s2(c3c3 - s3s3)

= c3s3(c1c1 - s2s2) - c1c2s1s2.C3 (Lemma 3)

## e2

4e0e2(RHS)     = 2s1c1.2s3c3 + (2c1c1-1).(1-2s3s3).2s2c2 + 2s2c2

= 4(c1c3s1s3 + c2s2(c1c1 + s3s3 - 2c1c1s3s3))

= 4(c1c3s1s3 + c2c2(c1c1c3c3 + s1s1s3s3)) (Lemma 4)

e0e2(LHS)     = (c1c2c3 + s1s2s3)(c1s2c3 + s1c2s3)

= c1c1c2c3c3s2 + c1c2c2c3s1s3 + c1c3s1s2s2s3 + c2s1s1s2s3s3

= c1c3s1s3(c2c2 + s2s2) + c2s2(c1c1c3c3 + s1s1s3s3)

= c1c3s1s3 + c2s2(c1c1c3c3 + s1s1s3s3)

## e3

4e0e3(RHS)     = (2c2c2-1).2s1c1 + (1-2s3s3).2s1c1 - C1.2s2c2.2s3c3

= 4(c1s1(c2c2 - s3s3) - c2c3s2s3.C1)

e0e2(LHS)     = (c1c2c3 + s1s2s3)(s1c2c3 - c1s2s3)

= c1c2c2c3c3s1 - c1c1c2c3s2s3 + c2c3s1s1s2s3 - c1s1s2s2s3s3

= c1s1(c2c2c3c3 - s2s2s3s3) - c2c3s2s3(c1c1 - s1s1)

= c1c1(c2c2 - s3s3) - c2c3s2s3.C1 (Lemma 3)