df-bj-mulc - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-mulc		Structured version Visualization version GIF version

Definition df-bj-mulc 33133

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(((1^st ‘𝑥) = 0 ∨ (2^nd ‘𝑥) = 0), 0, if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))))))))

**Detailed syntax breakdown of Definition df-bj-mulc**
Step	Hyp	Ref	Expression
1		cmulc 33132	. 2 class ·_ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 33102	. . . . 5 class ℂ̅
4	3, 3	cxp 5112	. . . 4 class (ℂ̅ × ℂ̅)
5		ccchat 33119	. . . . 5 class ℂ̂
6	5, 5	cxp 5112	. . . 4 class (ℂ̂ × ℂ̂)
7	4, 6	cun 3572	. . 3 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
8	2	cv 1482	. . . . . . 7 class 𝑥
9		c1st 7166	. . . . . . 7 class 1^st
10	8, 9	cfv 5888	. . . . . 6 class (1^st ‘𝑥)
11		cc0 9936	. . . . . 6 class 0
12	10, 11	wceq 1483	. . . . 5 wff (1^st ‘𝑥) = 0
13		c2nd 7167	. . . . . . 7 class 2^nd
14	8, 13	cfv 5888	. . . . . 6 class (2^nd ‘𝑥)
15	14, 11	wceq 1483	. . . . 5 wff (2^nd ‘𝑥) = 0
16	12, 15	wo 383	. . . 4 wff ((1^st ‘𝑥) = 0 ∨ (2^nd ‘𝑥) = 0)
17		cinfty 33117	. . . . . . 7 class ∞
18	10, 17	wceq 1483	. . . . . 6 wff (1^st ‘𝑥) = ∞
19	14, 17	wceq 1483	. . . . . 6 wff (2^nd ‘𝑥) = ∞
20	18, 19	wo 383	. . . . 5 wff ((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞)
21		cc 9934	. . . . . . . 8 class ℂ
22	21, 21	cxp 5112	. . . . . . 7 class (ℂ × ℂ)
23	8, 22	wcel 1990	. . . . . 6 wff 𝑥 ∈ (ℂ × ℂ)
24		cmul 9941	. . . . . . 7 class ·
25	10, 14, 24	co 6650	. . . . . 6 class ((1^st ‘𝑥) · (2^nd ‘𝑥))
26		carg 33130	. . . . . . . . . 10 class Arg
27	10, 26	cfv 5888	. . . . . . . . 9 class (Arg‘(1^st ‘𝑥))
28	14, 26	cfv 5888	. . . . . . . . 9 class (Arg‘(2^nd ‘𝑥))
29		caddc 9939	. . . . . . . . 9 class +
30	27, 28, 29	co 6650	. . . . . . . 8 class ((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))
31		cprcpal 33128	. . . . . . . 8 class prcpal
32	30, 31	cfv 5888	. . . . . . 7 class (prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥))))
33		cinftyexpi 33093	. . . . . . 7 class inftyexpi
34	32, 33	cfv 5888	. . . . . 6 class (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))))
35	23, 25, 34	cif 4086	. . . . 5 class if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥))))))
36	20, 17, 35	cif 4086	. . . 4 class if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))))))
37	16, 11, 36	cif 4086	. . 3 class if(((1^st ‘𝑥) = 0 ∨ (2^nd ‘𝑥) = 0), 0, if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥))))))))
38	2, 7, 37	cmpt 4729	. 2 class (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1^st ‘𝑥) = 0 ∨ (2^nd ‘𝑥) = 0), 0, if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))))))))
39	1, 38	wceq 1483	1 wff ·_ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1^st ‘𝑥) = 0 ∨ (2^nd ‘𝑥) = 0), 0, if(((1^st ‘𝑥) = ∞ ∨ (2^nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1^st ‘𝑥) · (2^nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1^st ‘𝑥)) + (Arg‘(2^nd ‘𝑥)))))))))

Colors of variables: wff setvar class

This definition is referenced by: (None)

W3C validator