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 
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )

Proof

Step Hyp Ref Expression
1 opelxpi 
 |-  ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) )
2 fvres 
 |-  ( <. A , B >. e. ( N. X. N. ) -> ( ( .o |` ( N. X. N. ) ) ` <. A , B >. ) = ( .o ` <. A , B >. ) )
3 df-ov 
 |-  ( A .N B ) = ( .N ` <. A , B >. )
4 df-mi 
 |-  .N = ( .o |` ( N. X. N. ) )
5 4 fveq1i 
 |-  ( .N ` <. A , B >. ) = ( ( .o |` ( N. X. N. ) ) ` <. A , B >. )
6 3 5 eqtri 
 |-  ( A .N B ) = ( ( .o |` ( N. X. N. ) ) ` <. A , B >. )
7 df-ov 
 |-  ( A .o B ) = ( .o ` <. A , B >. )
8 2 6 7 3eqtr4g 
 |-  ( <. A , B >. e. ( N. X. N. ) -> ( A .N B ) = ( A .o B ) )
9 1 8 syl 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )