Definition df-mpq 7457

Description: Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-mpq

Step	Hyp	Ref	Expression
1		cmpq 7389	. 2 class .pQ
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnpi 7384	. . . 4 class N.
5	4, 4	cxp 4672	. . 3 class ( N. X. N. )
6	2	cv 1371	. . . . . 6 class x
7		c1st 6223	. . . . . 6 class 1st
8	6, 7	cfv 5270	. . . . 5 class ( 1st ` x )
9	3	cv 1371	. . . . . 6 class y
10	9, 7	cfv 5270	. . . . 5 class ( 1st ` y )
11		cmi 7386	. . . . 5 class .N
12	8, 10, 11	co 5943	. . . 4 class ( ( 1st ` x ) .N ( 1st ` y ) )
13		c2nd 6224	. . . . . 6 class 2nd
14	6, 13	cfv 5270	. . . . 5 class ( 2nd ` x )
15	9, 13	cfv 5270	. . . . 5 class ( 2nd ` y )
16	14, 15, 11	co 5943	. . . 4 class ( ( 2nd ` x ) .N ( 2nd ` y ) )
17	12, 16	cop 3635	. . 3 class <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >.
18	2, 3, 5, 5, 17	cmpo 5945	. 2 class ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
19	1, 18	wceq 1372	1 wff .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )

This definition is referenced by:  dfmpq2  7467  mulpipq2  7483