Definition df-bj-oppc

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)

	Ref	Expression
Assertion	df-bj-oppc	$$⊢{-}_{\overline{ℂ}}=\left(x\in \left(\overline{ℂ}\cup \widehat{ℂ}\right)⟼if\left(x=\infty ,\infty ,if\left(x\in ℂ,\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right),{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppcc	$$class{-}_{\overline{ℂ}}$$
1		vx	$$setvarx$$
2		cccbar	$$class\overline{ℂ}$$
3		ccchat	$$class\widehat{ℂ}$$
4	2 3	cun	$$class\left(\overline{ℂ}\cup \widehat{ℂ}\right)$$
5	1	cv	$$setvarx$$
6		cinfty	$$class\infty$$
7	5 6	wceq	$$wffx=\infty$$
8		cc	$$classℂ$$
9	5 8	wcel	$$wffx\in ℂ$$
10		vy	$$setvary$$
11		caddcc	$$class{+}_{\overline{ℂ}}$$
12	10	cv	$$setvary$$
13	5 12 11	co	$$class\left(x{+}_{\overline{ℂ}}y\right)$$
14		cc0	$$class0$$
15	13 14	wceq	$$wffx{+}_{\overline{ℂ}}y=0$$
16	15 10 8	crio	$$class\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right)$$
17		cinftyexpitau	$$class{\mathrm{+\infty e}}^{i\tau }$$
18		chalf	$$class\frac{1}{2}$$
19		c0r	$$class{0}_{𝑹}$$
20	18 19	cop	$$class⟨\frac{1}{2},0_{𝑹}⟩$$
21	5 20 11	co	$$class\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)$$
22	21 17	cfv	$$class{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)$$
23	9 16 22	cif	$$classif\left(x\in ℂ,\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right),{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)\right)$$
24	7 6 23	cif	$$classif\left(x=\infty ,\infty ,if\left(x\in ℂ,\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right),{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)\right)\right)$$
25	1 4 24	cmpt	$$class\left(x\in \left(\overline{ℂ}\cup \widehat{ℂ}\right)⟼if\left(x=\infty ,\infty ,if\left(x\in ℂ,\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right),{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)\right)\right)\right)$$
26	0 25	wceq	$$wff{-}_{\overline{ℂ}}=\left(x\in \left(\overline{ℂ}\cup \widehat{ℂ}\right)⟼if\left(x=\infty ,\infty ,if\left(x\in ℂ,\left(\iota y\in ℂ|x{+}_{\overline{ℂ}}y=0\right),{\mathrm{+\infty e}}^{i\tau }\left(x{+}_{\overline{ℂ}}⟨\frac{1}{2},0_{𝑹}⟩\right)\right)\right)\right)$$