mulpiord

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

		Ref	Expression
	Assertion	mulpiord	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A \cdot_{𝑵} B = A \cdot_{𝑜} B$

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in 𝑵 \land B \in 𝑵) \to ⟨A, B⟩ \in (𝑵 \times 𝑵)$
2		fvres	$⊢ ⟨A, B⟩ \in (𝑵 \times 𝑵) \to ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}) (⟨A, B⟩) = \cdot_{𝑜} (⟨A, B⟩)$
3		df-ov	$⊢ A \cdot_{𝑵} B = \cdot_{𝑵} (⟨A, B⟩)$
4		df-mi	$⊢ \cdot_{𝑵} = {\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}$
5	4	fveq1i	$⊢ \cdot_{𝑵} (⟨A, B⟩) = ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}) (⟨A, B⟩)$
6	3 5	eqtri	$⊢ A \cdot_{𝑵} B = ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}) (⟨A, B⟩)$
7		df-ov	$⊢ A \cdot_{𝑜} B = \cdot_{𝑜} (⟨A, B⟩)$
8	2 6 7	3eqtr4g	$⊢ ⟨A, B⟩ \in (𝑵 \times 𝑵) \to A \cdot_{𝑵} B = A \cdot_{𝑜} B$
9	1 8	syl	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A \cdot_{𝑵} B = A \cdot_{𝑜} B$

Metamath Proof Explorer