Definition df-bj-mulc 35396

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 (given df-bj-invc 35398).

Note that this definition uses · and Arg and /. Indeed, it would be contrived to bypass ordinary complex multiplication, and the present two-step definition looks like a good compromise. (Contributed by BJ, 22-Jun-2019.)

Assertion

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

Detailed syntax breakdown of Definition df-bj-mulc

Step	Hyp	Ref	Expression
1		cmulc 35395	. 2 class ·ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 35365	. . . . 5 class ℂ̅
4	3, 3	cxp 5586	. . . 4 class (ℂ̅ × ℂ̅)
5		ccchat 35382	. . . . 5 class ℂ̂
6	5, 5	cxp 5586	. . . 4 class (ℂ̂ × ℂ̂)
7	4, 6	cun 3889	. . 3 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
8	2	cv 1540	. . . . . . 7 class 𝑥
9		c1st 7815	. . . . . . 7 class 1st
10	8, 9	cfv 6430	. . . . . 6 class (1st ‘𝑥)
11		cc0 10855	. . . . . 6 class 0
12	10, 11	wceq 1541	. . . . 5 wff (1st ‘𝑥) = 0
13		c2nd 7816	. . . . . . 7 class 2nd
14	8, 13	cfv 6430	. . . . . 6 class (2nd ‘𝑥)
15	14, 11	wceq 1541	. . . . 5 wff (2nd ‘𝑥) = 0
16	12, 15	wo 843	. . . 4 wff ((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0)
17		cinfty 35380	. . . . . . 7 class ∞
18	10, 17	wceq 1541	. . . . . 6 wff (1st ‘𝑥) = ∞
19	14, 17	wceq 1541	. . . . . 6 wff (2nd ‘𝑥) = ∞
20	18, 19	wo 843	. . . . 5 wff ((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞)
21		cc 10853	. . . . . . . 8 class ℂ
22	21, 21	cxp 5586	. . . . . . 7 class (ℂ × ℂ)
23	8, 22	wcel 2109	. . . . . 6 wff 𝑥 ∈ (ℂ × ℂ)
24		cmul 10860	. . . . . . 7 class ·
25	10, 14, 24	co 7268	. . . . . 6 class ((1st ‘𝑥) · (2nd ‘𝑥))
26		carg 35393	. . . . . . . . . 10 class Arg
27	10, 26	cfv 6430	. . . . . . . . 9 class (Arg‘(1st ‘𝑥))
28	14, 26	cfv 6430	. . . . . . . . 9 class (Arg‘(2nd ‘𝑥))
29		caddcc 35387	. . . . . . . . 9 class +ℂ̅
30	27, 28, 29	co 7268	. . . . . . . 8 class ((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥)))
31		ctau 15892	. . . . . . . 8 class τ
32		cdiv 11615	. . . . . . . 8 class /
33	30, 31, 32	co 7268	. . . . . . 7 class (((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)
34		cinftyexpitau 35348	. . . . . . 7 class +∞eiτ
35	33, 34	cfv 6430	. . . . . 6 class (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))
36	23, 25, 35	cif 4464	. . . . 5 class if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)))
37	20, 17, 36	cif 4464	. . . 4 class if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))))
38	16, 11, 37	cif 4464	. . 3 class if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)))))
39	2, 7, 38	cmpt 5161	. 2 class (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))))))
40	1, 39	wceq 1541	1 wff ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))))))

This definition is referenced by: (None)