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 = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplpq	⊢ +pQ
1		vx	⊢ 𝑥
2		cnpi	⊢ N
3	2 2	cxp	⊢ ( N × N )
4		vy	⊢ 𝑦
5		c1st	⊢ 1st
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( 1st ‘ 𝑥 )
8		cmi	⊢ ·N
9		c2nd	⊢ 2nd
10	4	cv	⊢ 𝑦
11	10 9	cfv	⊢ ( 2nd ‘ 𝑦 )
12	7 11 8	co	⊢ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) )
13		cpli	⊢ +N
14	10 5	cfv	⊢ ( 1st ‘ 𝑦 )
15	6 9	cfv	⊢ ( 2nd ‘ 𝑥 )
16	14 15 8	co	⊢ ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) )
17	12 16 13	co	⊢ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) )
18	15 11 8	co	⊢ ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) )
19	17 18	cop	⊢ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩
20	1 4 3 3 19	cmpo	⊢ ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ )
21	0 20	wceq	⊢ +pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ )