Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 0 ↔ 𝑦 = 0 ) ) |
2 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( log ‘ 𝑥 ) = ( log ‘ 𝑦 ) ) |
3 |
2
|
negeqd |
⊢ ( 𝑥 = 𝑦 → - ( log ‘ 𝑥 ) = - ( log ‘ 𝑦 ) ) |
4 |
1 3
|
ifbieq2d |
⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) ) |
5 |
4
|
cbvmptv |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) ) |
6 |
|
xrge0topn |
⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) |
7 |
5 6
|
xrge0iifmhm |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) MndHom ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
8 |
5 6
|
xrge0iifhmeo |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( II Homeo ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) |
9 |
|
cnfldex |
⊢ ℂfld ∈ V |
10 |
|
ovex |
⊢ ( 0 [,] 1 ) ∈ V |
11 |
|
eqid |
⊢ ( ℂfld ↾s ( 0 [,] 1 ) ) = ( ℂfld ↾s ( 0 [,] 1 ) ) |
12 |
|
eqid |
⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld ) |
13 |
11 12
|
mgpress |
⊢ ( ( ℂfld ∈ V ∧ ( 0 [,] 1 ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) ) |
14 |
9 10 13
|
mp2an |
⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) |
15 |
11
|
dfii4 |
⊢ II = ( TopOpen ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) |
16 |
14 15
|
mgptopn |
⊢ II = ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) |
17 |
16
|
oveq1i |
⊢ ( II Homeo ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) = ( ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) |
18 |
8 17
|
eleqtri |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) |
19 |
|
eqid |
⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) |
20 |
19
|
iistmd |
⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd |
21 |
|
xrge0tps |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp |
22 |
7 18 20 21
|
mhmhmeotmd |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd |