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

Metamath Proof Explorer

Definition df-plr

Description: Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-plr +R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplr ⊢ +R
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 vz ⊢ 𝑧
4 1 cv ⊢ 𝑥
5 cnr ⊢ R
6 4 5 wcel ⊢ 𝑥 ∈ R
7 2 cv ⊢ 𝑦
8 7 5 wcel ⊢ 𝑦 ∈ R
9 6 8 wa ⊢ ( 𝑥 ∈ R ∧ 𝑦 ∈ R )
10 vw ⊢ 𝑤
11 vv ⊢ 𝑣
12 vu ⊢ 𝑢
13 vf ⊢ 𝑓
14 10 cv ⊢ 𝑤
15 11 cv ⊢ 𝑣
16 14 15 cop ⊢ ⟨ 𝑤 , 𝑣 ⟩
17 cer ⊢ ~R
18 16 17 cec ⊢ [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R
19 4 18 wceq ⊢ 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R
20 12 cv ⊢ 𝑢
21 13 cv ⊢ 𝑓
22 20 21 cop ⊢ ⟨ 𝑢 , 𝑓 ⟩
23 22 17 cec ⊢ [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R
24 7 23 wceq ⊢ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R
25 19 24 wa ⊢ ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R )
26 3 cv ⊢ 𝑧
27 cpp ⊢ +P
28 14 20 27 co ⊢ ( 𝑤 +P 𝑢 )
29 15 21 27 co ⊢ ( 𝑣 +P 𝑓 )
30 28 29 cop ⊢ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩
31 30 17 cec ⊢ [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R
32 26 31 wceq ⊢ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R
33 25 32 wa ⊢ ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R )
34 33 13 wex ⊢ ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R )
35 34 12 wex ⊢ ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R )
36 35 11 wex ⊢ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R )
37 36 10 wex ⊢ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R )
38 9 37 wa ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R ) )
39 38 1 2 3 coprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R ) ) }
40 0 39 wceq ⊢ +R = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑢 , 𝑓 ⟩ ] ~R ) ∧ 𝑧 = [ ⟨ ( 𝑤 +P 𝑢 ) , ( 𝑣 +P 𝑓 ) ⟩ ] ~R ) ) }