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	⊢ -ℂ̅ = ( 𝑥 ∈ ( ℂ̅ ∪ ℂ̂ ) ↦ if ( 𝑥 = ∞ , ∞ , if ( 𝑥 ∈ ℂ , ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 ) , ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppcc	⊢ -ℂ̅
1		vx	⊢ 𝑥
2		cccbar	⊢ ℂ̅
3		ccchat	⊢ ℂ̂
4	2 3	cun	⊢ ( ℂ̅ ∪ ℂ̂ )
5	1	cv	⊢ 𝑥
6		cinfty	⊢ ∞
7	5 6	wceq	⊢ 𝑥 = ∞
8		cc	⊢ ℂ
9	5 8	wcel	⊢ 𝑥 ∈ ℂ
10		vy	⊢ 𝑦
11		caddcc	⊢ +ℂ̅
12	10	cv	⊢ 𝑦
13	5 12 11	co	⊢ ( 𝑥 +ℂ̅ 𝑦 )
14		cc0	⊢ 0
15	13 14	wceq	⊢ ( 𝑥 +ℂ̅ 𝑦 ) = 0
16	15 10 8	crio	⊢ ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 )
17		cinftyexpitau	⊢ +∞eiτ
18		chalf	⊢ 1/2
19		c0r	⊢ 0R
20	18 19	cop	⊢ ⟨ 1/2 , 0R ⟩
21	5 20 11	co	⊢ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ )
22	21 17	cfv	⊢ ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) )
23	9 16 22	cif	⊢ if ( 𝑥 ∈ ℂ , ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 ) , ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) ) )
24	7 6 23	cif	⊢ if ( 𝑥 = ∞ , ∞ , if ( 𝑥 ∈ ℂ , ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 ) , ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) ) ) )
25	1 4 24	cmpt	⊢ ( 𝑥 ∈ ( ℂ̅ ∪ ℂ̂ ) ↦ if ( 𝑥 = ∞ , ∞ , if ( 𝑥 ∈ ℂ , ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 ) , ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) ) ) ) )
26	0 25	wceq	⊢ -ℂ̅ = ( 𝑥 ∈ ( ℂ̅ ∪ ℂ̂ ) ↦ if ( 𝑥 = ∞ , ∞ , if ( 𝑥 ∈ ℂ , ( ℩ 𝑦 ∈ ℂ ( 𝑥 +ℂ̅ 𝑦 ) = 0 ) , ( +∞eiτ ‘ ( 𝑥 +ℂ̅ ⟨ 1/2 , 0R ⟩ ) ) ) ) )