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

Metamath Proof Explorer

Definition df-mpq

Description: Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.4 of Gleason p. 119. (Contributed by NM, 28-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-mpq 
|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpq 
 |-  .pQ
1 vx 
 |-  x
2 cnpi 
 |-  N.
3 2 2 cxp 
 |-  ( N. X. N. )
4 vy 
 |-  y
5 c1st 
 |-  1st
6 1 cv 
 |-  x
7 6 5 cfv 
 |-  ( 1st ` x )
8 cmi 
 |-  .N
9 4 cv 
 |-  y
10 9 5 cfv 
 |-  ( 1st ` y )
11 7 10 8 co 
 |-  ( ( 1st ` x ) .N ( 1st ` y ) )
12 c2nd 
 |-  2nd
13 6 12 cfv 
 |-  ( 2nd ` x )
14 9 12 cfv 
 |-  ( 2nd ` y )
15 13 14 8 co 
 |-  ( ( 2nd ` x ) .N ( 2nd ` y ) )
16 11 15 cop 
 |-  <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >.
17 1 4 3 3 16 cmpo 
 |-  ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
18 0 17 wceq 
 |-  .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )