df-bj-addc

Description: Define the additions on the extended complex numbers (on the subset of ( CCbar X. CCbar ) where it makes sense) and on the complex projective line (Riemann sphere). We use the plural in "additions" since these are two different operations, even though +cc is overloaded. (Contributed by BJ, 22-Jun-2019)

		Ref	Expression
	Assertion	df-bj-addc	$⊢ +_{\overline{ℂ}} = (x \in (((ℂ \times \overline{ℂ}) \cup (\overline{ℂ} \times ℂ)) \cup ((\hat{ℂ} \times \hat{ℂ}) \cup ({I ↾}_{ℂ_{\infty}}))) ⟼ if ((1^{st} (x) = \infty \lor 2^{nd} (x) = \infty), \infty, if (1^{st} (x) \in ℂ, if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x)), 1^{st} (x))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caddcc	$class +_{\overline{ℂ}}$
1		vx	$setvar x$
2		cc	$class ℂ$
3		cccbar	$class \overline{ℂ}$
4	2 3	cxp	$class (ℂ \times \overline{ℂ})$
5	3 2	cxp	$class (\overline{ℂ} \times ℂ)$
6	4 5	cun	$class ((ℂ \times \overline{ℂ}) \cup (\overline{ℂ} \times ℂ))$
7		ccchat	$class \hat{ℂ}$
8	7 7	cxp	$class (\hat{ℂ} \times \hat{ℂ})$
9		cid	$class I$
10		cccinfty	$class ℂ_{\infty}$
11	9 10	cres	$class ({I ↾}_{ℂ_{\infty}})$
12	8 11	cun	$class ((\hat{ℂ} \times \hat{ℂ}) \cup ({I ↾}_{ℂ_{\infty}}))$
13	6 12	cun	$class (((ℂ \times \overline{ℂ}) \cup (\overline{ℂ} \times ℂ)) \cup ((\hat{ℂ} \times \hat{ℂ}) \cup ({I ↾}_{ℂ_{\infty}})))$
14		c1st	$class 1^{st}$
15	1	cv	$setvar x$
16	15 14	cfv	$class 1^{st} (x)$
17		cinfty	$class \infty$
18	16 17	wceq	$wff 1^{st} (x) = \infty$
19		c2nd	$class 2^{nd}$
20	15 19	cfv	$class 2^{nd} (x)$
21	20 17	wceq	$wff 2^{nd} (x) = \infty$
22	18 21	wo	$wff (1^{st} (x) = \infty \lor 2^{nd} (x) = \infty)$
23	16 2	wcel	$wff 1^{st} (x) \in ℂ$
24	20 2	wcel	$wff 2^{nd} (x) \in ℂ$
25	16 14	cfv	$class 1^{st} (1^{st} (x))$
26		cplr	$class +_{𝑹}$
27	20 14	cfv	$class 1^{st} (2^{nd} (x))$
28	25 27 26	co	$class (1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)))$
29	16 19	cfv	$class 2^{nd} (1^{st} (x))$
30	20 19	cfv	$class 2^{nd} (2^{nd} (x))$
31	29 30 26	co	$class (2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x)))$
32	28 31	cop	$class ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩$
33	24 32 20	cif	$class if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x))$
34	23 33 16	cif	$class if (1^{st} (x) \in ℂ, if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x)), 1^{st} (x))$
35	22 17 34	cif	$class if ((1^{st} (x) = \infty \lor 2^{nd} (x) = \infty), \infty, if (1^{st} (x) \in ℂ, if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x)), 1^{st} (x)))$
36	1 13 35	cmpt	$class (x \in (((ℂ \times \overline{ℂ}) \cup (\overline{ℂ} \times ℂ)) \cup ((\hat{ℂ} \times \hat{ℂ}) \cup ({I ↾}_{ℂ_{\infty}}))) ⟼ if ((1^{st} (x) = \infty \lor 2^{nd} (x) = \infty), \infty, if (1^{st} (x) \in ℂ, if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x)), 1^{st} (x))))$
37	0 36	wceq	$wff +_{\overline{ℂ}} = (x \in (((ℂ \times \overline{ℂ}) \cup (\overline{ℂ} \times ℂ)) \cup ((\hat{ℂ} \times \hat{ℂ}) \cup ({I ↾}_{ℂ_{\infty}}))) ⟼ if ((1^{st} (x) = \infty \lor 2^{nd} (x) = \infty), \infty, if (1^{st} (x) \in ℂ, if (2^{nd} (x) \in ℂ, ⟨1^{st} (1^{st} (x)) +_{𝑹} 1^{st} (2^{nd} (x)), 2^{nd} (1^{st} (x)) +_{𝑹} 2^{nd} (2^{nd} (x))⟩, 2^{nd} (x)), 1^{st} (x))))$

Metamath Proof Explorer

Definition df-bj-addc

Detailed syntax breakdown