Ordinal Multiplication by Zero

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ be an ordinal.

\(\ds x \cdot \O\) \(=\) \(\ds \O\)
\(\ds \O \cdot x\) \(=\) \(\ds \O\)


Proof

\(\ds x \cdot \O\) \(=\) \(\ds \O\) Definition of Ordinal Multiplication

For $\O \cdot x = \O$, the proof shall proceed by Transfinite Induction on $x$.


Basis for the Induction

\(\ds \O \cdot \O\) \(=\) \(\ds \O\) Definition of Ordinal Multiplication

This proves the basis for the induction.


Induction Step

\(\ds \O \cdot x\) \(=\) \(\ds \O\) Inductive Hypothesis
\(\ds \leadsto \ \ \) \(\ds \paren {\O \cdot x} + \O\) \(=\) \(\ds \O\) Definition of Ordinal Addition
\(\ds \O \cdot x^+\) \(=\) \(\ds \paren {\O \cdot x} + \O\) Definition of Ordinal Multiplication
\(\ds \leadsto \ \ \) \(\ds \O \cdot x^+\) \(=\) \(\ds \O\) Equality is Transitive

This proves the induction step.


Limit Case

\(\ds \forall y \in x: \, \) \(\ds \O \cdot y\) \(=\) \(\ds \O\) Hypothesis
\(\ds \leadsto \ \ \) \(\ds \bigcup_{y \mathop \in x} \paren {\O \cdot y}\) \(=\) \(\ds \O\) Indexed Union Equality
\(\ds \O \cdot x\) \(=\) \(\ds \bigcup_{y \mathop \in x} \paren {\O \cdot y}\) Definition of Ordinal Multiplication
\(\ds \leadsto \ \ \) \(\ds \O \cdot x\) \(=\) \(\ds \O\) Equality is Transitive

This proves the limit case.

$\blacksquare$


Sources