Metamath Proof Explorer

Theorem omsuc

Description: Multiplication with successor. Definition 8.15 of TakeutiZaring p. 62. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion omsuc ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 suc ⁡ B = A ⋅ 𝑜 B + 𝑜 A

Proof

Step Hyp Ref Expression
1 rdgsuc ⊢ B ∈ On → rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ suc ⁡ B = x ∈ V ⟼ x + 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ B
2 1 adantl ⊢ A ∈ On ∧ B ∈ On → rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ suc ⁡ B = x ∈ V ⟼ x + 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ B
3 suceloni ⊢ B ∈ On → suc ⁡ B ∈ On
4 omv ⊢ A ∈ On ∧ suc ⁡ B ∈ On → A ⋅ 𝑜 suc ⁡ B = rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ suc ⁡ B
5 3 4 sylan2 ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 suc ⁡ B = rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ suc ⁡ B
6 ovex ⊢ A ⋅ 𝑜 B ∈ V
7 oveq1 ⊢ x = A ⋅ 𝑜 B → x + 𝑜 A = A ⋅ 𝑜 B + 𝑜 A
8 eqid ⊢ x ∈ V ⟼ x + 𝑜 A = x ∈ V ⟼ x + 𝑜 A
9 ovex ⊢ A ⋅ 𝑜 B + 𝑜 A ∈ V
10 7 8 9 fvmpt ⊢ A ⋅ 𝑜 B ∈ V → x ∈ V ⟼ x + 𝑜 A ⁡ A ⋅ 𝑜 B = A ⋅ 𝑜 B + 𝑜 A
11 6 10 ax-mp ⊢ x ∈ V ⟼ x + 𝑜 A ⁡ A ⋅ 𝑜 B = A ⋅ 𝑜 B + 𝑜 A
12 omv ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B = rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ B
13 12 fveq2d ⊢ A ∈ On ∧ B ∈ On → x ∈ V ⟼ x + 𝑜 A ⁡ A ⋅ 𝑜 B = x ∈ V ⟼ x + 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ B
14 11 13 eqtr3id ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B + 𝑜 A = x ∈ V ⟼ x + 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ B
15 2 5 14 3eqtr4d ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 suc ⁡ B = A ⋅ 𝑜 B + 𝑜 A