Definition df-bj-mulc 32310

Description: Define the multiplication of extended complex numbers and of the complex projective line (Riemann sphere). In our convention, a product with 0 is 0, even when the other factor is infinite. An alternate convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. Note that our convention entails (0 / 0) = 0. (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-mulc	⊢ ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))))))

Detailed syntax breakdown of Definition df-bj-mulc

Step	Hyp	Ref	Expression
1		cmulc 32309	. 2 class ·ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 32279	. . . . 5 class ℂ̅
4	3, 3	cxp 5036	. . . 4 class (ℂ̅ × ℂ̅)
5		ccchat 32296	. . . . 5 class ℂ̂
6	5, 5	cxp 5036	. . . 4 class (ℂ̂ × ℂ̂)
7	4, 6	cun 3538	. . 3 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
8	2	cv 1474	. . . . . . 7 class 𝑥
9		c1st 7057	. . . . . . 7 class 1st
10	8, 9	cfv 5804	. . . . . 6 class (1st ‘𝑥)
11		cc0 9815	. . . . . 6 class 0
12	10, 11	wceq 1475	. . . . 5 wff (1st ‘𝑥) = 0
13		c2nd 7058	. . . . . . 7 class 2nd
14	8, 13	cfv 5804	. . . . . 6 class (2nd ‘𝑥)
15	14, 11	wceq 1475	. . . . 5 wff (2nd ‘𝑥) = 0
16	12, 15	wo 382	. . . 4 wff ((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0)
17		cinfty 32294	. . . . . . 7 class ∞
18	10, 17	wceq 1475	. . . . . 6 wff (1st ‘𝑥) = ∞
19	14, 17	wceq 1475	. . . . . 6 wff (2nd ‘𝑥) = ∞
20	18, 19	wo 382	. . . . 5 wff ((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞)
21		cc 9813	. . . . . . . 8 class ℂ
22	21, 21	cxp 5036	. . . . . . 7 class (ℂ × ℂ)
23	8, 22	wcel 1977	. . . . . 6 wff 𝑥 ∈ (ℂ × ℂ)
24		cmul 9820	. . . . . . 7 class ·
25	10, 14, 24	co 6549	. . . . . 6 class ((1st ‘𝑥) · (2nd ‘𝑥))
26		carg 32307	. . . . . . . . . 10 class Arg
27	10, 26	cfv 5804	. . . . . . . . 9 class (Arg‘(1st ‘𝑥))
28	14, 26	cfv 5804	. . . . . . . . 9 class (Arg‘(2nd ‘𝑥))
29		caddc 9818	. . . . . . . . 9 class +
30	27, 28, 29	co 6549	. . . . . . . 8 class ((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))
31		cprcpal 32305	. . . . . . . 8 class prcpal
32	30, 31	cfv 5804	. . . . . . 7 class (prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥))))
33		cinftyexpi 32270	. . . . . . 7 class inftyexpi
34	32, 33	cfv 5804	. . . . . 6 class (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))
35	23, 25, 34	cif 4036	. . . . 5 class if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥))))))
36	20, 17, 35	cif 4036	. . . 4 class if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))))
37	16, 11, 36	cif 4036	. . 3 class if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥))))))))
38	2, 7, 37	cmpt 4643	. 2 class (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))))))
39	1, 38	wceq 1475	1 wff ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))))))

This definition is referenced by: (None)