Metamath Proof Explorer

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 ⊢ A ∈ On ∧ B ∈ On → B = ∅ → A ⋅ 𝑜 B = ∅ ∧ B = suc ⁡ C ∧ C ∈ On → A ⋅ 𝑜 B = A ⋅ 𝑜 C + 𝑜 A ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ c ∈ B A ⋅ 𝑜 c

Proof

Step Hyp Ref Expression
1 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
2 omsuc ⊢ A ∈ On ∧ C ∈ On → A ⋅ 𝑜 suc ⁡ C = A ⋅ 𝑜 C + 𝑜 A
3 omlim ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ c ∈ B A ⋅ 𝑜 c
4 3 anassrs ⊢ A ∈ On ∧ B ∈ On ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ c ∈ B A ⋅ 𝑜 c
5 1 2 4 onov0suclim ⊢ A ∈ On ∧ B ∈ On → B = ∅ → A ⋅ 𝑜 B = ∅ ∧ B = suc ⁡ C ∧ C ∈ On → A ⋅ 𝑜 B = A ⋅ 𝑜 C + 𝑜 A ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ c ∈ B A ⋅ 𝑜 c