Theorem om0suclim

Description: Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of Schloeder p. 4. See om0 , omsuc , and omlim . (Contributed by RP, 18-Jan-2025)

	Ref	Expression
Assertion	om0suclim	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( ( 𝐴 ·o 𝐶 ) +o 𝐴 ) ) ∧ ( Lim 𝐵 → ( 𝐴 ·o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ·o 𝑐 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		om0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
2		omsuc	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ·o suc 𝐶 ) = ( ( 𝐴 ·o 𝐶 ) +o 𝐴 ) )
3		omlim	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( 𝐴 ·o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ·o 𝑐 ) )
4	3	anassrs	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐴 ·o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ·o 𝑐 ) )
5	1 2 4	onov0suclim	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( ( 𝐴 ·o 𝐶 ) +o 𝐴 ) ) ∧ ( Lim 𝐵 → ( 𝐴 ·o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ·o 𝑐 ) ) ) )