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 𝑓 ) ⟩ ) ) }