Definition df-add

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

	Ref	Expression
Assertion	df-add	$$⊢+=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caddc	$$class+$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		vz	$$setvarz$$
4	1	cv	$$setvarx$$
5		cc	$$classℂ$$
6	4 5	wcel	$$wffx\in ℂ$$
7	2	cv	$$setvary$$
8	7 5	wcel	$$wffy\in ℂ$$
9	6 8	wa	$$wff\left(x\in ℂ\wedge y\in ℂ\right)$$
10		vw	$$setvarw$$
11		vv	$$setvarv$$
12		vu	$$setvaru$$
13		vf	$$setvarf$$
14	10	cv	$$setvarw$$
15	11	cv	$$setvarv$$
16	14 15	cop	$$class⟨w,v⟩$$
17	4 16	wceq	$$wffx=⟨w,v⟩$$
18	12	cv	$$setvaru$$
19	13	cv	$$setvarf$$
20	18 19	cop	$$class⟨u,f⟩$$
21	7 20	wceq	$$wffy=⟨u,f⟩$$
22	17 21	wa	$$wff\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)$$
23	3	cv	$$setvarz$$
24		cplr	$$class{+}_{𝑹}$$
25	14 18 24	co	$$class\left(w{+}_{𝑹}u\right)$$
26	15 19 24	co	$$class\left(v{+}_{𝑹}f\right)$$
27	25 26	cop	$$class⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩$$
28	23 27	wceq	$$wffz=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩$$
29	22 28	wa	$$wff\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)$$
30	29 13	wex	$$wff\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)$$
31	30 12	wex	$$wff\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)$$
32	31 11	wex	$$wff\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)$$
33	32 10	wex	$$wff\exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)$$
34	9 33	wa	$$wff\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)\right)$$
35	34 1 2 3	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)\right)\right\}$$
36	0 35	wceq	$$wff+=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨w{+}_{𝑹}u,v{+}_{𝑹}f⟩\right)\right)\right\}$$