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	$$⊢{+}_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplpq	$$class{+}_{\mathrm{𝑝𝑸}}$$
1		vx	$$setvarx$$
2		cnpi	$$class𝑵$$
3	2 2	cxp	$$class\left(𝑵\times 𝑵\right)$$
4		vy	$$setvary$$
5		c1st	$$class{1}^{st}$$
6	1	cv	$$setvarx$$
7	6 5	cfv	$$class{1}^{st}\left(x\right)$$
8		cmi	$$class{\cdot }_{𝑵}$$
9		c2nd	$$class{2}^{nd}$$
10	4	cv	$$setvary$$
11	10 9	cfv	$$class{2}^{nd}\left(y\right)$$
12	7 11 8	co	$$class\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right)$$
13		cpli	$$class{+}_{𝑵}$$
14	10 5	cfv	$$class{1}^{st}\left(y\right)$$
15	6 9	cfv	$$class{2}^{nd}\left(x\right)$$
16	14 15 8	co	$$class\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right)$$
17	12 16 13	co	$$class\left(\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right)\right)$$
18	15 11 8	co	$$class\left(2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right)$$
19	17 18	cop	$$class⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩$$
20	1 4 3 3 19	cmpo	$$class\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$
21	0 20	wceq	$$wff{+}_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$