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 | |- .cc = ( x e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) |-> if ( ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) , 0 , if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmulc | |- .cc |
|
| 1 | vx | |- x |
|
| 2 | cccbar | |- CCbar |
|
| 3 | 2 2 | cxp | |- ( CCbar X. CCbar ) |
| 4 | ccchat | |- CChat |
|
| 5 | 4 4 | cxp | |- ( CChat X. CChat ) |
| 6 | 3 5 | cun | |- ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) |
| 7 | c1st | |- 1st |
|
| 8 | 1 | cv | |- x |
| 9 | 8 7 | cfv | |- ( 1st ` x ) |
| 10 | cc0 | |- 0 |
|
| 11 | 9 10 | wceq | |- ( 1st ` x ) = 0 |
| 12 | c2nd | |- 2nd |
|
| 13 | 8 12 | cfv | |- ( 2nd ` x ) |
| 14 | 13 10 | wceq | |- ( 2nd ` x ) = 0 |
| 15 | 11 14 | wo | |- ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) |
| 16 | cinfty | |- infty |
|
| 17 | 9 16 | wceq | |- ( 1st ` x ) = infty |
| 18 | 13 16 | wceq | |- ( 2nd ` x ) = infty |
| 19 | 17 18 | wo | |- ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) |
| 20 | cc | |- CC |
|
| 21 | 20 20 | cxp | |- ( CC X. CC ) |
| 22 | 8 21 | wcel | |- x e. ( CC X. CC ) |
| 23 | cmul | |- x. |
|
| 24 | 9 13 23 | co | |- ( ( 1st ` x ) x. ( 2nd ` x ) ) |
| 25 | cinftyexpitau | |- inftyexpitau |
|
| 26 | carg | |- Arg |
|
| 27 | 9 26 | cfv | |- ( Arg ` ( 1st ` x ) ) |
| 28 | caddcc | |- +cc |
|
| 29 | 13 26 | cfv | |- ( Arg ` ( 2nd ` x ) ) |
| 30 | 27 29 28 | co | |- ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) |
| 31 | cdiv | |- / |
|
| 32 | ctau | |- _tau |
|
| 33 | 30 32 31 | co | |- ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) |
| 34 | 33 25 | cfv | |- ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) |
| 35 | 22 24 34 | cif | |- if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) |
| 36 | 19 16 35 | cif | |- if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) ) |
| 37 | 15 10 36 | cif | |- if ( ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) , 0 , if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) ) ) |
| 38 | 1 6 37 | cmpt | |- ( x e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) |-> if ( ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) , 0 , if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) ) ) ) |
| 39 | 0 38 | wceq | |- .cc = ( x e. ( ( CCbar X. CCbar ) u. ( CChat X. CChat ) ) |-> if ( ( ( 1st ` x ) = 0 \/ ( 2nd ` x ) = 0 ) , 0 , if ( ( ( 1st ` x ) = infty \/ ( 2nd ` x ) = infty ) , infty , if ( x e. ( CC X. CC ) , ( ( 1st ` x ) x. ( 2nd ` x ) ) , ( inftyexpitau ` ( ( ( Arg ` ( 1st ` x ) ) +cc ( Arg ` ( 2nd ` x ) ) ) / _tau ) ) ) ) ) ) |