Ordinal Sum of Powers

From ProofWiki
Jump to navigation Jump to search

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$


Sources