Definition df-bj-oppc 35338

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 35337	. 2 class -ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 35313	. . . 4 class ℂ̅
4		ccchat 35330	. . . 4 class ℂ̂
5	3, 4	cun 3881	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1538	. . . . 5 class 𝑥
7		cinfty 35328	. . . . 5 class ∞
8	6, 7	wceq 1539	. . . 4 wff 𝑥 = ∞
9		cc 10800	. . . . . 6 class ℂ
10	6, 9	wcel 2108	. . . . 5 wff 𝑥 ∈ ℂ
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1538	. . . . . . . 8 class 𝑦
13		caddcc 35335	. . . . . . . 8 class +ℂ̅
14	6, 12, 13	co 7255	. . . . . . 7 class (𝑥 +ℂ̅ 𝑦)
15		cc0 10802	. . . . . . 7 class 0
16	14, 15	wceq 1539	. . . . . 6 wff (𝑥 +ℂ̅ 𝑦) = 0
17	16, 11, 9	crio 7211	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0)
18		chalf 35301	. . . . . . . 8 class 1/2
19		c0r 10553	. . . . . . . 8 class 0R
20	18, 19	cop 4564	. . . . . . 7 class ⟨1/2, 0R⟩
21	6, 20, 13	co 7255	. . . . . 6 class (𝑥 +ℂ̅ ⟨1/2, 0R⟩)
22		cinftyexpitau 35296	. . . . . 6 class +∞eiτ
23	21, 22	cfv 6418	. . . . 5 class (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))
24	10, 17, 23	cif 4456	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))
25	8, 7, 24	cif 4456	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))))
26	2, 5, 25	cmpt 5153	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))
27	1, 26	wceq 1539	1 wff -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))

This definition is referenced by: (None)