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

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-plpq

Detailed syntax breakdown