Theorem mulpipq

Description: Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	mulpipq	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( A .N C ) , ( B .N D ) >. )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	|- ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) )
2		opelxpi	|- ( ( C e. N. /\ D e. N. ) -> <. C , D >. e. ( N. X. N. ) )
3		mulpipq2	|- ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( ( 1st ` <. A , B >. ) .N ( 1st ` <. C , D >. ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. )
4	1 2 3	syl2an	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( ( 1st ` <. A , B >. ) .N ( 1st ` <. C , D >. ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. )
5		op1stg	|- ( ( A e. N. /\ B e. N. ) -> ( 1st ` <. A , B >. ) = A )
6		op1stg	|- ( ( C e. N. /\ D e. N. ) -> ( 1st ` <. C , D >. ) = C )
7	5 6	oveqan12d	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( 1st ` <. A , B >. ) .N ( 1st ` <. C , D >. ) ) = ( A .N C ) )
8		op2ndg	|- ( ( A e. N. /\ B e. N. ) -> ( 2nd ` <. A , B >. ) = B )
9		op2ndg	|- ( ( C e. N. /\ D e. N. ) -> ( 2nd ` <. C , D >. ) = D )
10	8 9	oveqan12d	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) = ( B .N D ) )
11	7 10	opeq12d	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> <. ( ( 1st ` <. A , B >. ) .N ( 1st ` <. C , D >. ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. = <. ( A .N C ) , ( B .N D ) >. )
12	4 11	eqtrd	|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( A .N C ) , ( B .N D ) >. )