This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omsuc

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

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

Proof

Step Hyp Ref Expression
1 rdgsuc ⊢ ( 𝐵 ∈ On → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
3 onsuc ⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ On )
4 omv ⊢ ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
5 3 4 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
6 ovex ⊢ ( 𝐴 ·o 𝐵 ) ∈ V
7 oveq1 ⊢ ( 𝑥 = ( 𝐴 ·o 𝐵 ) → ( 𝑥 +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
8 eqid ⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) )
9 ovex ⊢ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) ∈ V
10 7 8 9 fvmpt ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
11 6 10 ax-mp ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 )
12 omv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
13 12 fveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
14 11 13 eqtr3id ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
15 2 5 14 3eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )