Theorem: Quaternions Defined by Ordered Pairs

Consider the quaternions $\Bbb H$ as numbers in the form:
: $a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$
where:
: $a, b, c, d$ are real numbers;
: $\mathbf 1, \mathbf i, \mathbf j, \mathbf k$ are entities related to each other in the following way:
{{begin-eqn}}     
{{eqn | l = \mathbf i \mathbf j = - \mathbf j \mathbf i
      | r = \mathbf k
      | c = 
}}
{{eqn | l = \mathbf j \mathbf k = - \mathbf k \mathbf j
      | r = \mathbf i
      | c = 
}}
{{eqn | l = \mathbf k \mathbf i = - \mathbf i \mathbf k
      | r = \mathbf j
      | c = 
}}
{{eqn | l = \mathbf i^2 = \mathbf j^2 = \mathbf k^2 = \mathbf i \mathbf j \mathbf k
      | r = - \mathbf 1
      | c = 
}}
{{end-eqn}}
Now consider the quaternions $\Bbb H$ defined as ordered pairs $\tuple {x, y}$ where $x, y \in \C$ are complex numbers, on which the operation of multiplication is defined as follows:
Let $w = a_1 + b_1 i, x = c_1 + d_1 i, y = a_2 + b_2 i, z = c_2 + d_2 i$ be complex numbers.
Then $\tuple {w, x} \tuple {y, z}$ is defined as:
:$\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
where $\overline w$ and $\overline x$ are the complex conjugates of $w$ and $x$ respectively.
These two definitions are equivalent.

Proof:
First we identify the following:
{{begin-eqn}}
{{eqn | n = 1
      | l = \mathbf 1
      | r = \tuple {1, 0}
      | c = 
}}
{{eqn | n = 2
      | l = \mathbf i
      | r = \tuple {i, 0}
      | c = 
}}
{{eqn | n = 3
      | l = \mathbf j
      | r = \tuple {0, i}
      | c = 
}}
{{eqn | n = 4
      | l = \mathbf k
      | r = \tuple {0, 1}
      | c = 
}}
{{end-eqn}}
We can see that:
{{begin-eqn}}
{{eqn | l = \mathbf 1^2
      | r = \tuple {1, 0} \tuple {1, 0}
      | c = 
}}
{{eqn | r = \tuple {1 \times 1 - 0 \times 0, 1 \times 0 + 0 \times 1}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {1, 0}
      | c = 
}}
{{eqn | r = \mathbf 1
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf i^2
      | r = \tuple {i, 0} \tuple {i, 0}
      | c = 
}}
{{eqn | r = \tuple {i \times i - 0 \times 0, \paren {-i} \times 0 + 0 \times i}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {-1, 0}
      | c = 
}}
{{eqn | r = -\mathbf 1
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf j^2
      | r = \tuple {0, i} \tuple {0, i}
      | c = 
}}
{{eqn | r = \tuple {0 \times 0 - i \times \paren {-i}, 0 \times i + i \times 0}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {-1, 0}
      | c = 
}}
{{eqn | r = -\mathbf 1
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf k^2
      | r = \tuple {0, 1} \tuple {0, 1}
      | c = 
}}
{{eqn | r = \tuple {0 \times 0 - 1 \times 1, 0 \times 1 + 1 \times 0}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {-1, 0}
      | c = 
}}
{{eqn | r = -\mathbf 1
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf i \mathbf j
      | r = \tuple {i, 0} \tuple {0, i}
      | c = 
}}
{{eqn | r = \tuple {i \times 0 - i \times 0, \paren {-i} \times i + 0 \times 0}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {0, 1}
      | c = 
}}
{{eqn | r = \mathbf k
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf j \mathbf k
      | r = \tuple {0, i} \tuple {0, 1}
      | c = 
}}
{{eqn | r = \tuple {0 \times 0 - 1 \times \paren {-i}, 0 \times 1 + i \times 0}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {i, 0}
      | c = 
}}
{{eqn | r = \mathbf i
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \mathbf k \mathbf i
      | r = \tuple {0, 1} \tuple {i, 0} 
      | c = 
}}
{{eqn | r = \tuple {0 \times i - 0 \times 1, 0 \times 0 + 1 \times i}
      | c = from $\tuple {w, x} \tuple {y, z} := \tuple {w y - z \overline x, \overline w z + x y}$
}}
{{eqn | r = \tuple {0, i}
      | c = 
}}
{{eqn | r = \mathbf j
      | c = 
}}
{{end-eqn}}
Let:
:$w = a_1 + b_1 i$
:$x = d_1 + c_1 i$
:$y = a_2 + b_2 i$
:$z = d_2 + c_2 i$
and so:
:$\overline w = a_1 - b_1 i$
:$\overline x = d_1 - c_1 i$
Then substituting for $(1)$ to $(4)$ above, we have:
{{begin-eqn}}
{{eqn | l = w
      | r = a_1 \mathbf 1 + b_1 \mathbf i
      | c = 
}}
{{eqn | l = x
      | r = d_1 \mathbf k + c_1 \mathbf j
      | c = 
}}
{{eqn | l = y
      | r = a_2 \mathbf 1 + b_2 \mathbf i
      | c = 
}}
{{eqn | l = z
      | r = d_2 \mathbf k + c_2 \mathbf j
      | c = 
}}
{{end-eqn}}
Notice the way $\mathbf j$ and $\mathbf k$ are configured. See that they are what appears to be in the wrong order.
We can then demonstrate the equivalence by showing that:
{{begin-eqn}}
{{eqn | ll= \tuple {w, x} \tuple {y, z}
      | l = =
      | o = 
      | r = (
      | c = 
}}
{{eqn | o = 
      | r = \paren {a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2} + \paren {a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2} i
      | c = 
}}
{{eqn | o = ,
      | r = \paren {a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2} + \paren {a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2} i
      | c = 
}}
{{eqn | o = 
      | r = )
      | c = 
}}
{{end-eqn}}
which is equivalent to:
{{begin-eqn}}
{{eqn | ll= \mathbf x_1 \mathbf x_2
      | l = =
      | o = 
      | r = \paren {a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2} \mathbf 1
      | c = 
}}
{{eqn | o = +
      | r = \paren {a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2} \mathbf i
      | c = 
}}
{{eqn | o = +
      | r = \paren {a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2} \mathbf j
      | c = 
}}
{{eqn | o = +
      | r = \paren {a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2} \mathbf k
      | c = 
}}
{{end-eqn}}
where:
:$x_1 = a_1 \mathbf 1 + b_1 \mathbf i + c_1 \mathbf j + d_1 \mathbf k$
:$x_2 = a_2 \mathbf 1 + b_2 \mathbf i + c_2 \mathbf j + d_2 \mathbf k$
in accordance with Quaternion Multiplication.
Thus:
{{begin-eqn}}
{{eqn | l = w y
      | r = \paren {a_1 a_2 - b_1 b_2} + \paren {a_1 b_2 + b_1 a_2} i
      | c = 
}}
{{eqn | l = z \overline x
      | r = \paren {d_1 d_2 + c_1 c_2} + \paren {d_1 c_2 - c_1 d_2} i
}}
{{eqn | l = \overline w z
      | r = \paren {a_1 d_2 + b_1 c_2} + \paren {a_1 c_2 - b_1 d_2} i
}}
{{eqn | l = x y
      | r = \paren {d_1 a_2 - c_1 b_2} + \paren {d_1 b_2 + c_1 a_2} i
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = w y - z \overline x
      | r = \paren {a_1 a_2 - b_1 b_2 - c_1 c_2 - d_1 d_2} + \paren {a_1 b_2 + b_1 a_2 + c_1 d_2 - d_1 c_2} i
      | c = 
}}
{{eqn | l = \overline w z + x y
      | r = \paren {a_1 d_2 + b_1 c_2 - c_1 b_2 + d_1 a_2} + \paren {a_1 c_2 - b_1 d_2 + c_1 a_2 + d_1 b_2} i
}}
{{end-eqn}}
as required.
{{qed}}