![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-invc | Structured version Visualization version GIF version |
Description: Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality (-1ℂ̅‘0) = ∞ is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as (-1ℂ̅‘0) ∉ ℂ̅. Note that this definition relies on df-bj-mulc 36122, which does not bypass ordinary complex multiplication, but defines extended complex multiplication on top of it. Therefore, we could have used directly / instead of (℩... ·ℂ̅ ...). (Contributed by BJ, 22-Jun-2019.) |
Ref | Expression |
---|---|
df-bj-invc | ⊢ -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cinvc 36123 | . 2 class -1ℂ̅ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cccbar 36091 | . . . 4 class ℂ̅ | |
4 | ccchat 36108 | . . . 4 class ℂ̂ | |
5 | 3, 4 | cun 3946 | . . 3 class (ℂ̅ ∪ ℂ̂) |
6 | 2 | cv 1540 | . . . . 5 class 𝑥 |
7 | cc0 11109 | . . . . 5 class 0 | |
8 | 6, 7 | wceq 1541 | . . . 4 wff 𝑥 = 0 |
9 | cinfty 36106 | . . . 4 class ∞ | |
10 | cc 11107 | . . . . . 6 class ℂ | |
11 | 6, 10 | wcel 2106 | . . . . 5 wff 𝑥 ∈ ℂ |
12 | vy | . . . . . . . . 9 setvar 𝑦 | |
13 | 12 | cv 1540 | . . . . . . . 8 class 𝑦 |
14 | cmulc 36121 | . . . . . . . 8 class ·ℂ̅ | |
15 | 6, 13, 14 | co 7408 | . . . . . . 7 class (𝑥 ·ℂ̅ 𝑦) |
16 | c1 11110 | . . . . . . 7 class 1 | |
17 | 15, 16 | wceq 1541 | . . . . . 6 wff (𝑥 ·ℂ̅ 𝑦) = 1 |
18 | 17, 12, 10 | crio 7363 | . . . . 5 class (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1) |
19 | 11, 18, 7 | cif 4528 | . . . 4 class if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0) |
20 | 8, 9, 19 | cif 4528 | . . 3 class if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0)) |
21 | 2, 5, 20 | cmpt 5231 | . 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))) |
22 | 1, 21 | wceq 1541 | 1 wff -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))) |
Colors of variables: wff setvar class |
This definition is referenced by: (None) |
Copyright terms: Public domain | W3C validator |