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. )