Definition df-bj-oppc 37234

Description: Define the negation (operation giving the opposite) on the set of extended complex numbers and the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-oppc	⊢ -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-bj-oppc

Step	Hyp	Ref	Expression
1		coppcc 37233	. 2 class -ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 37209	. . . 4 class ℂ̅
4		ccchat 37226	. . . 4 class ℂ̂
5	3, 4	cun 3948	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1539	. . . . 5 class 𝑥
7		cinfty 37224	. . . . 5 class ∞
8	6, 7	wceq 1540	. . . 4 wff 𝑥 = ∞
9		cc 11149	. . . . . 6 class ℂ
10	6, 9	wcel 2108	. . . . 5 wff 𝑥 ∈ ℂ
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1539	. . . . . . . 8 class 𝑦
13		caddcc 37231	. . . . . . . 8 class +ℂ̅
14	6, 12, 13	co 7429	. . . . . . 7 class (𝑥 +ℂ̅ 𝑦)
15		cc0 11151	. . . . . . 7 class 0
16	14, 15	wceq 1540	. . . . . 6 wff (𝑥 +ℂ̅ 𝑦) = 0
17	16, 11, 9	crio 7385	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0)
18		chalf 37197	. . . . . . . 8 class 1/2
19		c0r 10902	. . . . . . . 8 class 0R
20	18, 19	cop 4630	. . . . . . 7 class ⟨1/2, 0R⟩
21	6, 20, 13	co 7429	. . . . . 6 class (𝑥 +ℂ̅ ⟨1/2, 0R⟩)
22		cinftyexpitau 37192	. . . . . 6 class +∞eiτ
23	21, 22	cfv 6559	. . . . 5 class (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))
24	10, 17, 23	cif 4524	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))
25	8, 7, 24	cif 4524	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))))
26	2, 5, 25	cmpt 5223	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))
27	1, 26	wceq 1540	1 wff -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))

This definition is referenced by: (None)