Theorem mulpqnq

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

	Ref	Expression
Assertion	mulpqnq	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-mq	|- .Q = ( ( /Q o. .pQ ) |` ( Q. X. Q. ) )
2	1	fveq1i	|- ( .Q ` <. A , B >. ) = ( ( ( /Q o. .pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. )
3	2	a1i	|- ( ( A e. Q. /\ B e. Q. ) -> ( .Q ` <. A , B >. ) = ( ( ( /Q o. .pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) )
4		opelxpi	|- ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( Q. X. Q. ) )
5	4	fvresd	|- ( ( A e. Q. /\ B e. Q. ) -> ( ( ( /Q o. .pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) = ( ( /Q o. .pQ ) ` <. A , B >. ) )
6		df-mpq	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
7		opex	|- <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. _V
8	6 7	fnmpoi	|- .pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) )
9		elpqn	|- ( A e. Q. -> A e. ( N. X. N. ) )
10		elpqn	|- ( B e. Q. -> B e. ( N. X. N. ) )
11		opelxpi	|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) )
12	9 10 11	syl2an	|- ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) )
13		fvco2	|- ( ( .pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) ) /\ <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) ) -> ( ( /Q o. .pQ ) ` <. A , B >. ) = ( /Q ` ( .pQ ` <. A , B >. ) ) )
14	8 12 13	sylancr	|- ( ( A e. Q. /\ B e. Q. ) -> ( ( /Q o. .pQ ) ` <. A , B >. ) = ( /Q ` ( .pQ ` <. A , B >. ) ) )
15	3 5 14	3eqtrd	|- ( ( A e. Q. /\ B e. Q. ) -> ( .Q ` <. A , B >. ) = ( /Q ` ( .pQ ` <. A , B >. ) ) )
16		df-ov	|- ( A .Q B ) = ( .Q ` <. A , B >. )
17		df-ov	|- ( A .pQ B ) = ( .pQ ` <. A , B >. )
18	17	fveq2i	|- ( /Q ` ( A .pQ B ) ) = ( /Q ` ( .pQ ` <. A , B >. ) )
19	15 16 18	3eqtr4g	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )