Definition df-plus 4039

Description: Define addition over complex numbers.

Assertion

Ref	Expression
df-plus	⊢ + = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩))}

Distinct variable group(s):   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-plus

Step	Hyp	Ref	Expression
1		caddc 4031	. 2 class +
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class ℂ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℂ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ ℂ
9	5, 8	wa 196	. . . 4 wff (x ∈ ℂ ∧ y ∈ ℂ)
10		vw	. . . . . . . . . . . . 13 set w
11	10	cv 1089	. . . . . . . . . . . 12 class w
12		vv	. . . . . . . . . . . . 13 set v
13	12	cv 1089	. . . . . . . . . . . 12 class v
14	11, 13	cop 1810	. . . . . . . . . . 11 class ⟨w, v⟩
15	3, 14	wceq 1091	. . . . . . . . . 10 wff x = ⟨w, v⟩
16		vu	. . . . . . . . . . . . 13 set u
17	16	cv 1089	. . . . . . . . . . . 12 class u
18		vf	. . . . . . . . . . . . 13 set f
19	18	cv 1089	. . . . . . . . . . . 12 class f
20	17, 19	cop 1810	. . . . . . . . . . 11 class ⟨u, f⟩
21	7, 20	wceq 1091	. . . . . . . . . 10 wff y = ⟨u, f⟩
22	15, 21	wa 196	. . . . . . . . 9 wff (x = ⟨w, v⟩ ∧ y = ⟨u, f⟩)
23		vz	. . . . . . . . . . 11 set z
24	23	cv 1089	. . . . . . . . . 10 class z
25		cplr 3791	. . . . . . . . . . . 12 class +R
26	11, 17, 25	co 3001	. . . . . . . . . . 11 class (w +R u)
27	13, 19, 25	co 3001	. . . . . . . . . . 11 class (v +R f)
28	26, 27	cop 1810	. . . . . . . . . 10 class ⟨(w +R u), (v +R f)⟩
29	24, 28	wceq 1091	. . . . . . . . 9 wff z = ⟨(w +R u), (v +R f)⟩
30	22, 29	wa 196	. . . . . . . 8 wff ((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩)
31	30, 18	wex 678	. . . . . . 7 wff ∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩)
32	31, 16	wex 678	. . . . . 6 wff ∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩)
33	32, 12	wex 678	. . . . 5 wff ∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩)
34	33, 10	wex 678	. . . 4 wff ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩)
35	9, 34	wa 196	. . 3 wff ((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩))
36	35, 2, 6, 23	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩))}
37	1, 36	wceq 1091	1 wff + = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +R u), (v +R f)⟩))}

This definition is referenced by:  addcnsr 4047  axaddex 4059

metamath.org