Definition df-bj-mulc

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

Note that this definition uses x. 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)

	Ref	Expression
Assertion	df-bj-mulc	$$⊢{\cdot }_{\overline{ℂ}}=\left(x\in \left(\left(\overline{ℂ}\times \overline{ℂ}\right)\cup \left(\widehat{ℂ}\times \widehat{ℂ}\right)\right)⟼if\left(\left(1^{st}\left(x\right)=0\vee 2^{nd}\left(x\right)=0\right),0,if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmulc	$$class{\cdot }_{\overline{ℂ}}$$
1		vx	$$setvarx$$
2		cccbar	$$class\overline{ℂ}$$
3	2 2	cxp	$$class\left(\overline{ℂ}\times \overline{ℂ}\right)$$
4		ccchat	$$class\widehat{ℂ}$$
5	4 4	cxp	$$class\left(\widehat{ℂ}\times \widehat{ℂ}\right)$$
6	3 5	cun	$$class\left(\left(\overline{ℂ}\times \overline{ℂ}\right)\cup \left(\widehat{ℂ}\times \widehat{ℂ}\right)\right)$$
7		c1st	$$class{1}^{st}$$
8	1	cv	$$setvarx$$
9	8 7	cfv	$$class{1}^{st}\left(x\right)$$
10		cc0	$$class0$$
11	9 10	wceq	$$wff{1}^{st}\left(x\right)=0$$
12		c2nd	$$class{2}^{nd}$$
13	8 12	cfv	$$class{2}^{nd}\left(x\right)$$
14	13 10	wceq	$$wff{2}^{nd}\left(x\right)=0$$
15	11 14	wo	$$wff\left(1^{st}\left(x\right)=0\vee 2^{nd}\left(x\right)=0\right)$$
16		cinfty	$$class\infty$$
17	9 16	wceq	$$wff{1}^{st}\left(x\right)=\infty$$
18	13 16	wceq	$$wff{2}^{nd}\left(x\right)=\infty$$
19	17 18	wo	$$wff\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right)$$
20		cc	$$classℂ$$
21	20 20	cxp	$$class\left(ℂ\times ℂ\right)$$
22	8 21	wcel	$$wffx\in \left(ℂ\times ℂ\right)$$
23		cmul	$$class\times$$
24	9 13 23	co	$$class{1}^{st}\left(x\right)2^{nd}\left(x\right)$$
25		cinftyexpitau	$$class{\mathrm{+\infty e}}^{i\tau }$$
26		carg	$$class\mathrm{Arg}$$
27	9 26	cfv	$$class\mathrm{Arg}\left(1^{st}\left(x\right)\right)$$
28		caddcc	$$class{+}_{\overline{ℂ}}$$
29	13 26	cfv	$$class\mathrm{Arg}\left(2^{nd}\left(x\right)\right)$$
30	27 29 28	co	$$class\left(\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)\right)$$
31		cdiv	$$class÷$$
32		ctau	$$class\mathrm{\tau }$$
33	30 32 31	co	$$class\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)$$
34	33 25	cfv	$$class{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)$$
35	22 24 34	cif	$$classif\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)$$
36	19 16 35	cif	$$classif\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)\right)$$
37	15 10 36	cif	$$classif\left(\left(1^{st}\left(x\right)=0\vee 2^{nd}\left(x\right)=0\right),0,if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)\right)\right)$$
38	1 6 37	cmpt	$$class\left(x\in \left(\left(\overline{ℂ}\times \overline{ℂ}\right)\cup \left(\widehat{ℂ}\times \widehat{ℂ}\right)\right)⟼if\left(\left(1^{st}\left(x\right)=0\vee 2^{nd}\left(x\right)=0\right),0,if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)\right)\right)\right)$$
39	0 38	wceq	$$wff{\cdot }_{\overline{ℂ}}=\left(x\in \left(\left(\overline{ℂ}\times \overline{ℂ}\right)\cup \left(\widehat{ℂ}\times \widehat{ℂ}\right)\right)⟼if\left(\left(1^{st}\left(x\right)=0\vee 2^{nd}\left(x\right)=0\right),0,if\left(\left(1^{st}\left(x\right)=\infty \vee 2^{nd}\left(x\right)=\infty \right),\infty ,if\left(x\in \left(ℂ\times ℂ\right),1^{st}\left(x\right)2^{nd}\left(x\right),{\mathrm{+\infty e}}^{i\tau }\left(\frac{\mathrm{Arg}\left(1^{st}\left(x\right)\right){+}_{\overline{ℂ}}\mathrm{Arg}\left(2^{nd}\left(x\right)\right)}{\mathrm{\tau }}\right)\right)\right)\right)\right)$$