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 Unicode 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

. (Contributed by BJ, 22-Jun-2019.)

**Assertion**
Ref	Expression
df-bj-mulc	.cc CCbar CCbar CChat CChat $\/$ infty $\/$ infty infty inftyexpi prcpalArg Arg

**Detailed syntax breakdown of Definition df-bj-mulc**
Step	Hyp	Ref	Expression
1		cmulc 33132	. 2 .cc
2		vx	. . 3
3		cccbar 33102	. . . . 5 CCbar
4	3, 3	cxp 5112	. . . 4 CCbar CCbar
5		ccchat 33119	. . . . 5 CChat
6	5, 5	cxp 5112	. . . 4 CChat CChat
7	4, 6	cun 3572	. . 3 CCbar CCbar CChat CChat
8	2	cv 1482	. . . . . . 7
9		c1st 7166	. . . . . . 7
10	8, 9	cfv 5888	. . . . . 6
11		cc0 9936	. . . . . 6
12	10, 11	wceq 1483	. . . . 5
13		c2nd 7167	. . . . . . 7
14	8, 13	cfv 5888	. . . . . 6
15	14, 11	wceq 1483	. . . . 5
16	12, 15	wo 383	. . . 4 $\/$
17		cinfty 33117	. . . . . . 7 infty
18	10, 17	wceq 1483	. . . . . 6 infty
19	14, 17	wceq 1483	. . . . . 6 infty
20	18, 19	wo 383	. . . . 5 infty $\/$ infty
21		cc 9934	. . . . . . . 8
22	21, 21	cxp 5112	. . . . . . 7
23	8, 22	wcel 1990	. . . . . 6
24		cmul 9941	. . . . . . 7
25	10, 14, 24	co 6650	. . . . . 6
26		carg 33130	. . . . . . . . . 10 Arg
27	10, 26	cfv 5888	. . . . . . . . 9 Arg
28	14, 26	cfv 5888	. . . . . . . . 9 Arg
29		caddc 9939	. . . . . . . . 9
30	27, 28, 29	co 6650	. . . . . . . 8 Arg Arg
31		cprcpal 33128	. . . . . . . 8 prcpal
32	30, 31	cfv 5888	. . . . . . 7 prcpalArg Arg
33		cinftyexpi 33093	. . . . . . 7 inftyexpi
34	32, 33	cfv 5888	. . . . . 6 inftyexpi prcpalArg Arg
35	23, 25, 34	cif 4086	. . . . 5 inftyexpi prcpalArg Arg
36	20, 17, 35	cif 4086	. . . 4 infty $\/$ infty infty inftyexpi prcpalArg Arg
37	16, 11, 36	cif 4086	. . 3 $\/$ infty $\/$ infty infty inftyexpi prcpalArg Arg
38	2, 7, 37	cmpt 4729	. 2 CCbar CCbar CChat CChat $\/$ infty $\/$ infty infty inftyexpi prcpalArg Arg
39	1, 38	wceq 1483	1 .cc CCbar CCbar CChat CChat $\/$ infty $\/$ infty infty inftyexpi prcpalArg Arg

Colors of variables: wff setvar class

This definition is referenced by: (None)

W3C validator