Ordinal Exponentiation of Terms

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x, y, z$ be ordinals.

Let $n$ be a finite ordinal.

Let $x$ be a limit ordinal.

Let $y, z, n$ all be greater than $0$.


Then:

$\paren {x^y \times n}^z = x^{y \mathop \times z} \times n$ if $z$ is not a limit ordinal
$\paren {x^y \times n}^z = x^{y \mathop \times z}$ if $z$ is a limit ordinal.


Proof

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


Basis for the Induction

The hypothesis requires that $z \ne 0$, so the induction starts at $z = 1$.


\(\ds \paren {x^y \times n}^1\) \(=\) \(\ds x^y \times n\) Definition of Ordinal Exponentiation
\(\ds \) \(=\) \(\ds x^{y \mathop \times 1} \times n\) Ordinal Multiplication by One

This proves the basis for the induction.

$\Box$


Induction Step

\(\ds \paren {x^y \times n}^z\) \(=\) \(\ds x^{y \mathop \times z} \times n\) Inductive Hypothesis
\(\ds \leadsto \ \ \) \(\ds \paren {x^y \times n}^{z^+}\) \(=\) \(\ds \paren {x^y \times n}^z \times x^y \times n\) Definition of Ordinal Exponentiation
\(\ds \) \(=\) \(\ds x^{y \mathop \times z} \times n \times x^y \times n\) Inductive Hypothesis
\(\ds \) \(=\) \(\ds x^{y \mathop \times z} \times x^y \times n\) Finite Ordinal Times Ordinal
\(\ds \) \(=\) \(\ds x^{y \mathop \times z + y} \times n\) Ordinal Sum of Powers
\(\ds \) \(=\) \(\ds x^{y \mathop \times z^+} \times n\) Definition of Ordinal Multiplication

This proves the induction step.

$\Box$


Limit Case

Suppose that this statement holds for all $w \in z$ where $z$ is a limit ordinal.


Then:

\(\ds x^{y \mathop \times z}\) \(=\) \(\ds \paren {x^y}^z\) Ordinal Power of Power
\(\ds \) \(\le\) \(\ds \paren {x^y \times n}^z\) Subset is Right Compatible with Ordinal Exponentiation
\(\ds \) \(=\) \(\ds \bigcup_{w \mathop \in z} \paren {x^y \times n}^w\) Definition of Ordinal Exponentiation
\(\ds \) \(\le\) \(\ds \bigcup_{w \mathop \in z} x^{y \mathop \times w} \times n\) Proof by Cases where $w \in K_I$ or $w \in K_{II}$
\(\ds \) \(\le\) \(\ds \bigcup_{w \mathop \in z} x^{y \mathop \times w + 1}\) Membership is Left Compatible with Ordinal Exponentiation
\(\ds \) \(\le\) \(\ds \bigcup_{w \mathop \in z} x^{y \mathop \times w^+}\) Membership is Left Compatible with Ordinal Multiplication and Membership is Left Compatible with Ordinal Exponentiation
\(\ds \) \(=\) \(\ds \bigcup_{w \mathop \in z} \left({ x^y }\right)^{w^+}\) Ordinal Power of Power
\(\ds \) \(=\) \(\ds \paren {x^y}^z\) Definition of Ordinal Exponentiation

This proves the limit case.

$\blacksquare$


Sources