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

Metamath Proof Explorer

Theorem mulpiord

Description: Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulpiord ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opelxpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
2 fvres ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( ( ·o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ·o ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
3 df-ov ⊢ ( 𝐴 ·N 𝐵 ) = ( ·N ‘ ⟨ 𝐴 , 𝐵 ⟩ )
4 df-mi ⊢ ·N = ( ·o ↾ ( N × N ) )
5 4 fveq1i ⊢ ( ·N ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ·o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 3 5 eqtri ⊢ ( 𝐴 ·N 𝐵 ) = ( ( ·o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 df-ov ⊢ ( 𝐴 ·o 𝐵 ) = ( ·o ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8 2 6 7 3eqtr4g ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )
9 1 8 syl ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )