Definition df-plpq

Description: Define pre-addition 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. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition +Q ( df-plq ) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q ( df-enq ). (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) (New usage is discouraged.)

	Ref	Expression
Assertion	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 ) ) >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplpq	|- +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		c2nd	|- 2nd
10	4	cv	|- y
11	10 9	cfv	|- ( 2nd ` y )
12	7 11 8	co	|- ( ( 1st ` x ) .N ( 2nd ` y ) )
13		cpli	|- +N
14	10 5	cfv	|- ( 1st ` y )
15	6 9	cfv	|- ( 2nd ` x )
16	14 15 8	co	|- ( ( 1st ` y ) .N ( 2nd ` x ) )
17	12 16 13	co	|- ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) )
18	15 11 8	co	|- ( ( 2nd ` x ) .N ( 2nd ` y ) )
19	17 18	cop	|- <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >.
20	1 4 3 3 19	cmpo	|- ( 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 ) ) >. )
21	0 20	wceq	|- +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 ) ) >. )