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