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	⊢ ·_ℂ̅ = ( 𝑥 ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ↦ if ( ( ( 1^st ‘ 𝑥 ) = 0 ∨ ( 2^nd ‘ 𝑥 ) = 0 ) , 0 , if ( ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ ) , ∞ , if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmulc	⊢ ·_ℂ̅
1		vx	⊢ 𝑥
2		cccbar	⊢ ℂ̅
3	2 2	cxp	⊢ ( ℂ̅ × ℂ̅ )
4		ccchat	⊢ ℂ̂
5	4 4	cxp	⊢ ( ℂ̂ × ℂ̂ )
6	3 5	cun	⊢ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) )
7		c1st	⊢ 1^st
8	1	cv	⊢ 𝑥
9	8 7	cfv	⊢ ( 1^st ‘ 𝑥 )
10		cc0	⊢ 0
11	9 10	wceq	⊢ ( 1^st ‘ 𝑥 ) = 0
12		c2nd	⊢ 2^nd
13	8 12	cfv	⊢ ( 2^nd ‘ 𝑥 )
14	13 10	wceq	⊢ ( 2^nd ‘ 𝑥 ) = 0
15	11 14	wo	⊢ ( ( 1^st ‘ 𝑥 ) = 0 ∨ ( 2^nd ‘ 𝑥 ) = 0 )
16		cinfty	⊢ ∞
17	9 16	wceq	⊢ ( 1^st ‘ 𝑥 ) = ∞
18	13 16	wceq	⊢ ( 2^nd ‘ 𝑥 ) = ∞
19	17 18	wo	⊢ ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ )
20		cc	⊢ ℂ
21	20 20	cxp	⊢ ( ℂ × ℂ )
22	8 21	wcel	⊢ 𝑥 ∈ ( ℂ × ℂ )
23		cmul	⊢ ·
24	9 13 23	co	⊢ ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) )
25		cinftyexpitau	⊢ +∞e^iτ
26		carg	⊢ Arg
27	9 26	cfv	⊢ ( Arg ‘ ( 1^st ‘ 𝑥 ) )
28		caddcc	⊢ +_ℂ̅
29	13 26	cfv	⊢ ( Arg ‘ ( 2^nd ‘ 𝑥 ) )
30	27 29 28	co	⊢ ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) )
31		cdiv	⊢ /
32		ctau	⊢ τ
33	30 32 31	co	⊢ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ )
34	33 25	cfv	⊢ ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) )
35	22 24 34	cif	⊢ if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) )
36	19 16 35	cif	⊢ if ( ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ ) , ∞ , if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) ) )
37	15 10 36	cif	⊢ if ( ( ( 1^st ‘ 𝑥 ) = 0 ∨ ( 2^nd ‘ 𝑥 ) = 0 ) , 0 , if ( ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ ) , ∞ , if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) ) ) )
38	1 6 37	cmpt	⊢ ( 𝑥 ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ↦ if ( ( ( 1^st ‘ 𝑥 ) = 0 ∨ ( 2^nd ‘ 𝑥 ) = 0 ) , 0 , if ( ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ ) , ∞ , if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) ) ) ) )
39	0 38	wceq	⊢ ·_ℂ̅ = ( 𝑥 ∈ ( ( ℂ̅ × ℂ̅ ) ∪ ( ℂ̂ × ℂ̂ ) ) ↦ if ( ( ( 1^st ‘ 𝑥 ) = 0 ∨ ( 2^nd ‘ 𝑥 ) = 0 ) , 0 , if ( ( ( 1^st ‘ 𝑥 ) = ∞ ∨ ( 2^nd ‘ 𝑥 ) = ∞ ) , ∞ , if ( 𝑥 ∈ ( ℂ × ℂ ) , ( ( 1^st ‘ 𝑥 ) · ( 2^nd ‘ 𝑥 ) ) , ( +∞e^iτ ‘ ( ( ( Arg ‘ ( 1^st ‘ 𝑥 ) ) +_ℂ̅ ( Arg ‘ ( 2^nd ‘ 𝑥 ) ) ) / τ ) ) ) ) ) )

Metamath Proof Explorer

Definition df-bj-mulc

Detailed syntax breakdown