Definition df-plpq 7152

Description: Define pre-addition 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. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition +Q (df-plqqs 7157) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 7155). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 28-Aug-1995.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-plpq

Step	Hyp	Ref	Expression
1		cplpq 7084	. 2 class +pQ
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnpi 7080	. . . 4 class N.
5	4, 4	cxp 4537	. . 3 class ( N. X. N. )
6	2	cv 1330	. . . . . . 7 class x
7		c1st 6036	. . . . . . 7 class 1st
8	6, 7	cfv 5123	. . . . . 6 class ( 1st ` x )
9	3	cv 1330	. . . . . . 7 class y
10		c2nd 6037	. . . . . . 7 class 2nd
11	9, 10	cfv 5123	. . . . . 6 class ( 2nd ` y )
12		cmi 7082	. . . . . 6 class .N
13	8, 11, 12	co 5774	. . . . 5 class ( ( 1st ` x ) .N ( 2nd ` y ) )
14	9, 7	cfv 5123	. . . . . 6 class ( 1st ` y )
15	6, 10	cfv 5123	. . . . . 6 class ( 2nd ` x )
16	14, 15, 12	co 5774	. . . . 5 class ( ( 1st ` y ) .N ( 2nd ` x ) )
17		cpli 7081	. . . . 5 class +N
18	13, 16, 17	co 5774	. . . 4 class ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) )
19	15, 11, 12	co 5774	. . . 4 class ( ( 2nd ` x ) .N ( 2nd ` y ) )
20	18, 19	cop 3530	. . 3 class <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >.
21	2, 3, 5, 5, 20	cmpo 5776	. 2 class ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
22	1, 21	wceq 1331	1 wff +pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )

This definition is referenced by:  dfplpq2  7162