Metamath Proof Explorer

Theorem om1

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. (Contributed by NM, 29-Oct-1995)

Ref Expression
Assertion om1 ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A

Proof

Step Hyp Ref Expression
1 df-1o ⊢ 1 𝑜 = suc ⁡ ∅
2 1 oveq2i ⊢ A ⋅ 𝑜 1 𝑜 = A ⋅ 𝑜 suc ⁡ ∅
3 peano1 ⊢ ∅ ∈ ω
4 onmsuc ⊢ A ∈ On ∧ ∅ ∈ ω → A ⋅ 𝑜 suc ⁡ ∅ = A ⋅ 𝑜 ∅ + 𝑜 A
5 3 4 mpan2 ⊢ A ∈ On → A ⋅ 𝑜 suc ⁡ ∅ = A ⋅ 𝑜 ∅ + 𝑜 A
6 2 5 syl5eq ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A ⋅ 𝑜 ∅ + 𝑜 A
7 om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅
8 7 oveq1d ⊢ A ∈ On → A ⋅ 𝑜 ∅ + 𝑜 A = ∅ + 𝑜 A
9 oa0r ⊢ A ∈ On → ∅ + 𝑜 A = A
10 6 8 9 3eqtrd ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A