This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑦 ) ) ⟩ )