Metamath Proof Explorer

Theorem onmsuc

Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onmsuc ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 peano2 ⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω )
2 nnon ⊢ ( suc 𝐵 ∈ ω → suc 𝐵 ∈ On )
3 1 2 syl ⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ On )
4 omv ⊢ ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
5 3 4 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
6 1 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → suc 𝐵 ∈ ω )
7 6 fvresd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
8 5 7 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) )
9 ovex ⊢ ( 𝐴 ·o 𝐵 ) ∈ V
10 oveq1 ⊢ ( 𝑥 = ( 𝐴 ·o 𝐵 ) → ( 𝑥 +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
11 eqid ⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) )
12 ovex ⊢ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) ∈ V
13 10 11 12 fvmpt ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
14 9 13 ax-mp ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 )
15 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
16 omv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
17 15 16 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
18 fvres ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
19 18 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
20 17 19 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) )
21 20 fveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
22 14 21 syl5eqr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
23 frsuc ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
24 23 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
25 22 24 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) )
26 8 25 eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )