Definition df-bj-oppc 36116

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 36115	. 2 class -ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 36091	. . . 4 class ℂ̅
4		ccchat 36108	. . . 4 class ℂ̂
5	3, 4	cun 3946	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1540	. . . . 5 class 𝑥
7		cinfty 36106	. . . . 5 class ∞
8	6, 7	wceq 1541	. . . 4 wff 𝑥 = ∞
9		cc 11107	. . . . . 6 class ℂ
10	6, 9	wcel 2106	. . . . 5 wff 𝑥 ∈ ℂ
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1540	. . . . . . . 8 class 𝑦
13		caddcc 36113	. . . . . . . 8 class +ℂ̅
14	6, 12, 13	co 7408	. . . . . . 7 class (𝑥 +ℂ̅ 𝑦)
15		cc0 11109	. . . . . . 7 class 0
16	14, 15	wceq 1541	. . . . . 6 wff (𝑥 +ℂ̅ 𝑦) = 0
17	16, 11, 9	crio 7363	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0)
18		chalf 36079	. . . . . . . 8 class 1/2
19		c0r 10860	. . . . . . . 8 class 0R
20	18, 19	cop 4634	. . . . . . 7 class ⟨1/2, 0R⟩
21	6, 20, 13	co 7408	. . . . . 6 class (𝑥 +ℂ̅ ⟨1/2, 0R⟩)
22		cinftyexpitau 36074	. . . . . 6 class +∞eiτ
23	21, 22	cfv 6543	. . . . 5 class (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))
24	10, 17, 23	cif 4528	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))
25	8, 7, 24	cif 4528	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))))
26	2, 5, 25	cmpt 5231	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))
27	1, 26	wceq 1541	1 wff -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))

This definition is referenced by: (None)