Definition df-bj-oppc 35411

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 35410	. 2 class -ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 35386	. . . 4 class ℂ̅
4		ccchat 35403	. . . 4 class ℂ̂
5	3, 4	cun 3885	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1538	. . . . 5 class 𝑥
7		cinfty 35401	. . . . 5 class ∞
8	6, 7	wceq 1539	. . . 4 wff 𝑥 = ∞
9		cc 10869	. . . . . 6 class ℂ
10	6, 9	wcel 2106	. . . . 5 wff 𝑥 ∈ ℂ
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1538	. . . . . . . 8 class 𝑦
13		caddcc 35408	. . . . . . . 8 class +ℂ̅
14	6, 12, 13	co 7275	. . . . . . 7 class (𝑥 +ℂ̅ 𝑦)
15		cc0 10871	. . . . . . 7 class 0
16	14, 15	wceq 1539	. . . . . 6 wff (𝑥 +ℂ̅ 𝑦) = 0
17	16, 11, 9	crio 7231	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0)
18		chalf 35374	. . . . . . . 8 class 1/2
19		c0r 10622	. . . . . . . 8 class 0R
20	18, 19	cop 4567	. . . . . . 7 class ⟨1/2, 0R⟩
21	6, 20, 13	co 7275	. . . . . 6 class (𝑥 +ℂ̅ ⟨1/2, 0R⟩)
22		cinftyexpitau 35369	. . . . . 6 class +∞eiτ
23	21, 22	cfv 6433	. . . . 5 class (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))
24	10, 17, 23	cif 4459	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))
25	8, 7, 24	cif 4459	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))))
26	2, 5, 25	cmpt 5157	. 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)