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)=s₁ etc.

Require to prove:

e₀ = c₁c₂c₃ + s₁s₂s₃ = sqrt(1 + C1C2 + C2C3 + C3C1 + S1S2S3) / 2

e₁ = c₁c₂s₃ - s₁s₂c₃ = (C1S3 + C2S3 - S1S2C3) / 4e₀

e₂ = c₁s₂c₃ + s₁c₂s₃ = (S1S3 + C1C3S2 + S2) / 4e₀

e₃ = s₁c₂c₃ - c₁s₂s₃ = (C2S1 + C3S1 - C1S2S3) / 4e₀

Lemmas

To begin with, some lemmas.

Lemma 1

C1C2          = (2c₁c₁ - 1)(1 - 2s₂s₂)

          = 2c₁c₁ - 4c₁c₁s₂s₂ - 1 + 2s₂s₂

C1C2 + C2C3 + C3C1

          = 2sum(c_ic_i + s_is_i) - 3 - 4sum(c_ic_is_is_i)

          = 3 - 4sum(c_ic_is_is_i)

Lemma 2

prod(c_ic_i) + prod(s_is_i)

          = prod(c_ic_i) + prod(1 - c_ic_i)

          = prod(c_ic_i) + 1 - sum(c_ic_i) + sum(c_ic_ic_jc_j) - prod(c_ic_i)

          = 1 - sum(c_ic_i(1 - c_jc_j))

          = 1 - sum(c_ic_is_js_j)

Lemma 3

c₁c₁c₂c₂ - s₁s₁s₂s₂

          = c₁c₁(1 - s₂s₂) - (1 - c₁c₁)s₂s₂

          = c₁c₁ - s₂s₂

Lemma 4

c₁c₁ + s₃s₃ - 2c₁c₁s₃s₃

          = c₁c₁(c₃c₃ + s₃s₃) + s₃s₃(c₁c₁ + s₁s₁) - 2c₁c₁s₃s₃

          = c₁c₁c₃c₃ + s₁s₁s₃s₃

Proofs

e0

4e₀e₀(RHS)        = 1 + C1C2 + C2C3 + C3C1 + S1S2S3

          = 1 + (3 - 4sum(c_ic_is_is_i)) + 8c₁c₂c₃s₁s₂s₃ (Lemma 1)

          = 4(1 - sum(c_ic_is_is_i) + 2c₁c₂c₃s₁s₂s₃)

e₀e₀(LHS)        = (c₁c₂c₃ + s₁s₂s₃)(c₁c₂c₃ + s₁s₂s₃)

          = prod(c_ic_i) + 2c₁c₂c₃s₁s₂s₃ + prod(s_is_i)

          = 1 - sum(c_ic_is_js_j) + 2c₁c₂c₃s₁s₂s₃ (Lemma 2)

e1

4e₀e₁(RHS)     = (2c₁c₁-1).2s₃c₃ + (1-2s₂s₂).2s₃c₃ - 2s₁c₁.2s₂c₂.C3

          = 4(s₃c₃(c₁c₁ - s₂s₂) - c₁c₂s₁s₂.C3)

e₀e₁(LHS)     = (c₁c₂c₃ + s₁s₂s₃)(c₁c₂s₃ - s₁s₂c₃)

          = c₁c₁c₂c₂c₃s₃ - c₁c₂c₃c₃s₁s₂ + c₁c₂s₁s₂s₃s₃ - c₃s₁s₁s₂s₂s₃

          = c₃s₃(c₁c₁c₂c₂ - s₁s₁s₂s₂) - c₁c₂s₁s₂(c₃c₃ - s₃s₃)

          = c₃s₃(c₁c₁ - s₂s₂) - c₁c₂s₁s₂.C3 (Lemma 3)

e2

4e₀e₂(RHS)     = 2s₁c₁.2s₃c₃ + (2c₁c₁-1).(1-2s₃s₃).2s₂c₂ + 2s₂c₂

          = 4(c₁c₃s₁s₃ + c₂s₂(c₁c₁ + s₃s₃ - 2c₁c₁s₃s₃))

          = 4(c₁c₃s₁s₃ + c₂c₂(c₁c₁c₃c₃ + s₁s₁s₃s₃)) (Lemma 4)

e₀e₂(LHS)     = (c₁c₂c₃ + s₁s₂s₃)(c₁s₂c₃ + s₁c₂s₃)

          = c₁c₁c₂c₃c₃s₂ + c₁c₂c₂c₃s₁s₃ + c₁c₃s₁s₂s₂s₃ + c₂s₁s₁s₂s₃s₃

          = c₁c₃s₁s₃(c₂c₂ + s₂s₂) + c₂s₂(c₁c₁c₃c₃ + s₁s₁s₃s₃)

          = c₁c₃s₁s₃ + c₂s₂(c₁c₁c₃c₃ + s₁s₁s₃s₃)

e3

4e₀e₃(RHS)     = (2c₂c₂-1).2s₁c₁ + (1-2s₃s₃).2s₁c₁ - C1.2s₂c₂.2s₃c₃

          = 4(c₁s₁(c₂c₂ - s₃s₃) - c₂c₃s₂s₃.C1)

e₀e₂(LHS)     = (c₁c₂c₃ + s₁s₂s₃)(s₁c₂c₃ - c₁s₂s₃)

          = c₁c₂c₂c₃c₃s₁ - c₁c₁c₂c₃s₂s₃ + c₂c₃s₁s₁s₂s₃ - c₁s₁s₂s₂s₃s₃

          = c₁s₁(c₂c₂c₃c₃ - s₂s₂s₃s₃) - c₂c₃s₂s₃(c₁c₁ - s₁s₁)

          = c₁c₁(c₂c₂ - s₃s₃) - c₂c₃s₂s₃.C1 (Lemma 3)