df-bj-addc - Mathbox for BJ

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

Definition df-bj-addc 33125

Description: Define the additions on the extended complex numbers (on the subset of

CCbar

where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)

**Assertion**
Ref	Expression
df-bj-addc	+cc CCbar CCbar CChat CChat DiagCCinfty infty $\/$ infty infty

**Detailed syntax breakdown of Definition df-bj-addc**
Step	Hyp	Ref	Expression
1		caddcc 33124	. 2 +cc
2		vx	. . 3
3		cc 9934	. . . . . 6
4		cccbar 33102	. . . . . 6 CCbar
5	3, 4	cxp 5112	. . . . 5 CCbar
6	4, 3	cxp 5112	. . . . 5 CCbar
7	5, 6	cun 3572	. . . 4 CCbar CCbar
8		ccchat 33119	. . . . . 6 CChat
9	8, 8	cxp 5112	. . . . 5 CChat CChat
10		cccinfty 33098	. . . . . 6 CCinfty
11		cdiag2 33088	. . . . . 6 Diag
12	10, 11	cfv 5888	. . . . 5 DiagCCinfty
13	9, 12	cun 3572	. . . 4 CChat CChat DiagCCinfty
14	7, 13	cun 3572	. . 3 CCbar CCbar CChat CChat DiagCCinfty
15	2	cv 1482	. . . . . . 7
16		c1st 7166	. . . . . . 7
17	15, 16	cfv 5888	. . . . . 6
18		cinfty 33117	. . . . . 6 infty
19	17, 18	wceq 1483	. . . . 5 infty
20		c2nd 7167	. . . . . . 7
21	15, 20	cfv 5888	. . . . . 6
22	21, 18	wceq 1483	. . . . 5 infty
23	19, 22	wo 383	. . . 4 infty $\/$ infty
24	17, 3	wcel 1990	. . . . 5
25	21, 3	wcel 1990	. . . . . 6
26		caddc 9939	. . . . . . 7
27	17, 21, 26	co 6650	. . . . . 6
28	25, 27, 21	cif 4086	. . . . 5
29	24, 28, 17	cif 4086	. . . 4
30	23, 18, 29	cif 4086	. . 3 infty $\/$ infty infty
31	2, 14, 30	cmpt 4729	. 2 CCbar CCbar CChat CChat DiagCCinfty infty $\/$ infty infty
32	1, 31	wceq 1483	1 +cc CCbar CCbar CChat CChat DiagCCinfty infty $\/$ infty infty

Colors of variables: wff setvar class

This definition is referenced by: (None)