Step |
Hyp |
Ref |
Expression |
1 |
|
xrge0cmn |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd |
2 |
|
cmnmnd |
⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ) |
3 |
1 2
|
ax-mp |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd |
4 |
|
xrge0tps |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp |
5 |
|
eqeq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 0 ↔ 𝑥 = 0 ) ) |
6 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( log ‘ 𝑦 ) = ( log ‘ 𝑥 ) ) |
7 |
6
|
negeqd |
⊢ ( 𝑦 = 𝑥 → - ( log ‘ 𝑦 ) = - ( log ‘ 𝑥 ) ) |
8 |
5 7
|
ifbieq2d |
⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) |
9 |
8
|
cbvmptv |
⊢ ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) |
10 |
|
eqid |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) |
11 |
|
eqid |
⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) |
12 |
9 10 11
|
xrge0pluscn |
⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ∈ ( ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ×t ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) |
13 |
|
xrsbas |
⊢ ℝ* = ( Base ‘ ℝ*𝑠 ) |
14 |
|
eqid |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) |
15 |
|
xrsadd |
⊢ +𝑒 = ( +g ‘ ℝ*𝑠 ) |
16 |
|
xaddf |
⊢ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* |
17 |
|
ffn |
⊢ ( +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* → +𝑒 Fn ( ℝ* × ℝ* ) ) |
18 |
16 17
|
ax-mp |
⊢ +𝑒 Fn ( ℝ* × ℝ* ) |
19 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
20 |
13 14 15 18 19
|
ressplusf |
⊢ ( +𝑓 ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) |
21 |
20
|
eqcomi |
⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( +𝑓 ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
22 |
|
xrge0base |
⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
23 |
|
ovex |
⊢ ( 0 [,] +∞ ) ∈ V |
24 |
|
xrstset |
⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 ) |
25 |
14 24
|
resstset |
⊢ ( ( 0 [,] +∞ ) ∈ V → ( ordTop ‘ ≤ ) = ( TopSet ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) |
26 |
23 25
|
ax-mp |
⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
27 |
22 26
|
topnval |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
28 |
21 27
|
istmd |
⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd ↔ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp ∧ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ∈ ( ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ×t ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) ) ) |
29 |
3 4 12 28
|
mpbir3an |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd |