This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulpipq2

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

		Ref	Expression
	Assertion	mulpipq2	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )

Proof

Step	Hyp	Ref	Expression
1		fveq2	\|- ( x = A -> ( 1st ` x ) = ( 1st ` A ) )
2	1	oveq1d	\|- ( x = A -> ( ( 1st ` x ) .N ( 1st ` y ) ) = ( ( 1st ` A ) .N ( 1st ` y ) ) )
3		fveq2	\|- ( x = A -> ( 2nd ` x ) = ( 2nd ` A ) )
4	3	oveq1d	\|- ( x = A -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` y ) ) )
5	2 4	opeq12d	\|- ( x = A -> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. = <. ( ( 1st ` A ) .N ( 1st ` y ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. )
6		fveq2	\|- ( y = B -> ( 1st ` y ) = ( 1st ` B ) )
7	6	oveq2d	\|- ( y = B -> ( ( 1st ` A ) .N ( 1st ` y ) ) = ( ( 1st ` A ) .N ( 1st ` B ) ) )
8		fveq2	\|- ( y = B -> ( 2nd ` y ) = ( 2nd ` B ) )
9	8	oveq2d	\|- ( y = B -> ( ( 2nd ` A ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` B ) ) )
10	7 9	opeq12d	\|- ( y = B -> <. ( ( 1st ` A ) .N ( 1st ` y ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
11		df-mpq	\|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) \|-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
12		opex	\|- <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. e. _V
13	5 10 11 12	ovmpo	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )