# 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$
 $\ds x^y \times x^z$ $=$ $\ds x^y$ Ordinal Multiplication by Zero $\ds$ $=$ $\ds x^{y + z}$ 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:

 $\ds x^y \times x^{z^+}$ $=$ $\ds x^y \times \paren {x^z \times x}$ Definition of Ordinal Exponentiation $\ds$ $=$ $\ds \paren {x^y \times x^z} \times x$ Ordinal Multiplication is Associative $\ds$ $=$ $\ds x^{y + z} \times x$ Inductive Hypothesis $\ds$ $=$ $\ds x^{\paren {y + z}^+}$ Definition of Ordinal Exponentiation $\ds$ $=$ $\ds x^{y + z^+}$ 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$.

 $\ds \forall w \in z: \,$ $\ds x^y \times x^w$ $\le$ $\ds x^y \times x^z$ Membership is Left Compatible with Ordinal Multiplication $\ds \leadsto \ \$ $\ds \bigcup_{w \mathop \in z} \paren {x^y \times x^w}$ $\le$ $\ds x^y \times x^z$ Indexed Union Subset

Conversely:

 $\ds w$ $\in$ $\ds x^y \times x^z$ $\ds \leadsto \ \$ $\ds \exists u \in x^z: \,$ $\ds w$ $\in$ $\ds x^y \times u$ Ordinal is Less than Ordinal times Limit $\ds \leadsto \ \$ $\ds \exists v \in z: \exists u \in x^v: \,$ $\ds w$ $\in$ $\ds x^y \times u$ 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 x^y \times x^v$

By Supremum Inequality for Ordinals, it follows that:

$\ds x^y \times x^z \le \bigcup_{w \mathop \in z} \paren {x^y \times x^w}$

 $\ds x^y \times x^z$ $=$ $\ds \bigcup_{w \mathop \in z} \paren {x^y \times x^w}$ Definition 2 of Set Equality $\ds$ $=$ $\ds \bigcup_{w \mathop \in z} x^{y + w}$ Inductive Hypothesis for the Limit Case

$\Box$

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

Conversely:

 $\ds w$ $\in$ $\ds x^{y + z}$ $\ds \leadsto \ \$ $\ds \exists u \in y + z: \,$ $\ds w$ $\in$ $\ds x^u$ Definition of Ordinal Exponentiation $\ds \leadsto \ \$ $\ds \exists v \in z: \exists u \in y + v: \,$ $\ds w$ $\in$ $\ds x^u$ Definition of Ordinal Addition

Thus, $u$ is bounded above by $y + v$ for some $v \in z$.

Therefore:

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

By Supremum Inequality for Ordinals, it follows that:

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

Thus, by definition of set equality:

$\ds x^{y + z} = \bigcup_{w \mathop \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$