Metamath Proof Explorer

Theorem mulpqf

Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulpqf 
|- .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )

Proof

Step Hyp Ref Expression
1 xp1st 
 |-  ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
2 xp1st 
 |-  ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
3 mulclpi 
 |-  ( ( ( 1st ` x ) e. N. /\ ( 1st ` y ) e. N. ) -> ( ( 1st ` x ) .N ( 1st ` y ) ) e. N. )
4 1 2 3 syl2an 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 1st ` x ) .N ( 1st ` y ) ) e. N. )
5 xp2nd 
 |-  ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
6 xp2nd 
 |-  ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
7 mulclpi 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. )
8 5 6 7 syl2an 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. )
9 4 8 opelxpd 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) )
10 9 rgen2 
 |-  A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. )
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 11 fmpo 
 |-  ( A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) <-> .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) )
13 10 12 mpbi 
 |-  .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )