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	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{\cdot }_{𝑵}B=A{\cdot }_{𝑜}B$$

Proof

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