# Ordinal Sum of Powers

## Theorem

Let $x$, $y$, and $z$ be ordinals.

Then:

$x^y \times x^z = x^{y + z}$

## Proof

The proof shall proceed by Transfinite Induction on $z$.

### Basis for the Induction

$x^0 = 1$ for all $x$
 $\displaystyle x^y \times x^z$ $=$ $\displaystyle x^y$ by Ordinal Multiplication by Zero $\displaystyle$ $=$ $\displaystyle x^{y + z}$ by Ordinal Addition by Zero

This proves the basis for the induction.

$\Box$

### Induction Step

Suppose that $x^y \times x^z = x^{y + z}$.

Then:

 $\displaystyle x^y \times x^{z^+}$ $=$ $\displaystyle x^y \times \left({ x^z \times x }\right)$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle \left({ x^y \times x^z }\right) \times x$ by Ordinal Multiplication is Associative $\displaystyle$ $=$ $\displaystyle x^{y + z} \times x$ by Inductive Hypothesis $\displaystyle$ $=$ $\displaystyle x^{\left({y + z}\right)^+}$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle x^{\left({y + z^+}\right)}$ definition of ordinal addition

This proves the induction step.

$\Box$

### Limit Case

Suppose that $\forall w \in z: x^y \times x^w = x^{y + w}$ for limit ordinal $z$.

 $\displaystyle \forall w \in z: \ \$ $\displaystyle \left({x^y \times x^w}\right)$ $\le$ $\displaystyle \left({x^y \times x^z}\right)$ by Membership is Left Compatible with Ordinal Multiplication $\displaystyle \implies \ \$ $\displaystyle \bigcup_{w \in z} \left({ x^y \times x^w }\right)$ $\le$ $\displaystyle \left({ x^y \times x^z }\right)$ by Indexed Union Subset

Conversely:

 $\displaystyle w \in \left({ x^y \times x^z }\right)$ $\implies$ $\displaystyle \exists u \in x^z: w \in \left({ x^y \times u }\right)$ by Ordinal is Less than Ordinal times Limit $\displaystyle$ $\implies$ $\displaystyle \exists v \in z: \exists u \in x^v: w \in \left({ x^y \times u }\right)$ by Ordinal is Less than Ordinal to Limit Power

But this means that $u$ is bounded above by $x^v$ for some $v \in z$.

Thus there exists a $v \in z$ such that:

$w \le \left({ x^y \times x^v }\right)$

By Supremum Inequality for Ordinals, it follows that:

$\left({ x^y \times x^z }\right) \le \bigcup_{w \in z} \left({ x^y \times x^w }\right)$

 $\displaystyle \left({ x^y \times x^z }\right)$ $=$ $\displaystyle \bigcup_{w \in z} \left({ x^y \times x^w }\right)$ Definition of Set Equality $\displaystyle$ $=$ $\displaystyle \bigcup_{w \in z} x^{y+w}$ Inductive Hypothesis for the Limit Case

$\Box$

 $\displaystyle \forall w \in z: \ \$ $\displaystyle y + w$ $\le$ $\displaystyle y + z$ by Membership is Left Compatible with Ordinal Addition $\displaystyle \forall w \in z: \ \$ $\displaystyle x^{y + w}$ $\le$ $\displaystyle x^{y + z}$ by Membership is Left Compatible with Ordinal Exponentiation $\displaystyle \implies \ \$ $\displaystyle \bigcup_{w \in z} x^{y + w}$ $\le$ $\displaystyle x^{y + z}$ by Indexed Union Subset

Conversely:

 $\displaystyle w \in x^{y + z}$ $\implies$ $\displaystyle \exists u \in \left({y + z}\right): w \in x^u$ definition of ordinal exponentiation $\displaystyle$ $\implies$ $\displaystyle \exists v \in z: \exists u \in \left({y + v}\right): w \in x^u$ definition of ordinal addition

Thus, $u$ is bounded above by $\left({ y + v }\right)$ for some $v \in z$.

Therefore:

$x^u \le x^{y + v}$

By Supremum Inequality for Ordinals, it follows that:

$x^{y + z} \le \bigcup_{w \in z} x^{y + w}$

Thus, by definition of set equality:

$x^{y + z} = \bigcup_{w \in z} x^{y + w}$

$\Box$

Combining the results of the first and second lemmas for the limit case:

$x^{y+z} = x^y \times x^z$

This proves the limit case.

$\blacksquare$