Definition df-bj-mulc 37225

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 37227).

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 37224	. 2 class ·ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 37194	. . . . 5 class ℂ̅
4	3, 3	cxp 5681	. . . 4 class (ℂ̅ × ℂ̅)
5		ccchat 37211	. . . . 5 class ℂ̂
6	5, 5	cxp 5681	. . . 4 class (ℂ̂ × ℂ̂)
7	4, 6	cun 3948	. . 3 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
8	2	cv 1539	. . . . . . 7 class 𝑥
9		c1st 8008	. . . . . . 7 class 1st
10	8, 9	cfv 6559	. . . . . 6 class (1st ‘𝑥)
11		cc0 11151	. . . . . 6 class 0
12	10, 11	wceq 1540	. . . . 5 wff (1st ‘𝑥) = 0
13		c2nd 8009	. . . . . . 7 class 2nd
14	8, 13	cfv 6559	. . . . . 6 class (2nd ‘𝑥)
15	14, 11	wceq 1540	. . . . 5 wff (2nd ‘𝑥) = 0
16	12, 15	wo 848	. . . 4 wff ((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0)
17		cinfty 37209	. . . . . . 7 class ∞
18	10, 17	wceq 1540	. . . . . 6 wff (1st ‘𝑥) = ∞
19	14, 17	wceq 1540	. . . . . 6 wff (2nd ‘𝑥) = ∞
20	18, 19	wo 848	. . . . 5 wff ((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞)
21		cc 11149	. . . . . . . 8 class ℂ
22	21, 21	cxp 5681	. . . . . . 7 class (ℂ × ℂ)
23	8, 22	wcel 2108	. . . . . 6 wff 𝑥 ∈ (ℂ × ℂ)
24		cmul 11156	. . . . . . 7 class ·
25	10, 14, 24	co 7429	. . . . . 6 class ((1st ‘𝑥) · (2nd ‘𝑥))
26		carg 37222	. . . . . . . . . 10 class Arg
27	10, 26	cfv 6559	. . . . . . . . 9 class (Arg‘(1st ‘𝑥))
28	14, 26	cfv 6559	. . . . . . . . 9 class (Arg‘(2nd ‘𝑥))
29		caddcc 37216	. . . . . . . . 9 class +ℂ̅
30	27, 28, 29	co 7429	. . . . . . . 8 class ((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥)))
31		ctau 16234	. . . . . . . 8 class τ
32		cdiv 11916	. . . . . . . 8 class /
33	30, 31, 32	co 7429	. . . . . . 7 class (((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)
34		cinftyexpitau 37177	. . . . . . 7 class +∞eiτ
35	33, 34	cfv 6559	. . . . . 6 class (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))
36	23, 25, 35	cif 4524	. . . . 5 class if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)))
37	20, 17, 36	cif 4524	. . . 4 class if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))))
38	16, 11, 37	cif 4524	. . 3 class if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)))))
39	2, 7, 38	cmpt 5223	. 2 class (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ))))))
40	1, 39	wceq 1540	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)