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

Metamath Proof Explorer

Definition df-add

Description: Define addition over complex numbers. (Contributed by NM, 28-May-1995) (New usage is discouraged.)

Ref Expression
Assertion df-add + = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( 𝑤 +R 𝑢 ) , ( 𝑣 +R 𝑓 ) ⟩ ) ) }

Detailed syntax breakdown

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