Definition df-bj-oppc 34514

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 34513	. 2 class -ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 34489	. . . 4 class ℂ̅
4		ccchat 34506	. . . 4 class ℂ̂
5	3, 4	cun 3932	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1530	. . . . 5 class 𝑥
7		cinfty 34504	. . . . 5 class ∞
8	6, 7	wceq 1531	. . . 4 wff 𝑥 = ∞
9		cc 10527	. . . . . 6 class ℂ
10	6, 9	wcel 2108	. . . . 5 wff 𝑥 ∈ ℂ
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1530	. . . . . . . 8 class 𝑦
13		caddcc 34511	. . . . . . . 8 class +ℂ̅
14	6, 12, 13	co 7148	. . . . . . 7 class (𝑥 +ℂ̅ 𝑦)
15		cc0 10529	. . . . . . 7 class 0
16	14, 15	wceq 1531	. . . . . 6 wff (𝑥 +ℂ̅ 𝑦) = 0
17	16, 11, 9	crio 7105	. . . . 5 class (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0)
18		chalf 34477	. . . . . . . 8 class 1/2
19		c0r 10280	. . . . . . . 8 class 0R
20	18, 19	cop 4565	. . . . . . 7 class ⟨1/2, 0R⟩
21	6, 20, 13	co 7148	. . . . . 6 class (𝑥 +ℂ̅ ⟨1/2, 0R⟩)
22		cinftyexpitau 34472	. . . . . 6 class +∞eiτ
23	21, 22	cfv 6348	. . . . 5 class (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))
24	10, 17, 23	cif 4465	. . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))
25	8, 7, 24	cif 4465	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩))))
26	2, 5, 25	cmpt 5137	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))
27	1, 26	wceq 1531	1 wff -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))

This definition is referenced by: (None)