Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . 3
⊢
(dist‘𝑊) =
(dist‘𝑊) |
2 | | sitmcl.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ ∞MetSp) |
3 | | sitmcl.2 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
4 | | sitmcl.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) |
5 | | sitmcl.4 |
. . 3
⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) |
6 | 1, 2, 3, 4, 5 | sitmfval 32061 |
. 2
⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) =
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝐹 ∘f (dist‘𝑊)𝐺))) |
7 | | xrge0base 31045 |
. . 3
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
8 | | xrge0topn 31639 |
. . . 4
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
9 | 8 | eqcomi 2748 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
10 | | eqid 2739 |
. . 3
⊢
(sigaGen‘((ordTop‘ ≤ ) ↾t
(0[,]+∞))) = (sigaGen‘((ordTop‘ ≤ ) ↾t
(0[,]+∞))) |
11 | | xrge00 31046 |
. . 3
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
12 | | ovex 7268 |
. . . 4
⊢
(0[,]+∞) ∈ V |
13 | | eqid 2739 |
. . . . 5
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
14 | | ax-xrsvsca 31034 |
. . . . 5
⊢
·e = ( ·𝑠
‘ℝ*𝑠) |
15 | 13, 14 | ressvsca 16910 |
. . . 4
⊢
((0[,]+∞) ∈ V → ·e = (
·𝑠
‘(ℝ*𝑠 ↾s
(0[,]+∞)))) |
16 | 12, 15 | ax-mp 5 |
. . 3
⊢
·e = ( ·𝑠
‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
17 | | ax-xrssca 31033 |
. . . . . 6
⊢
ℝfld =
(Scalar‘ℝ*𝑠) |
18 | 13, 17 | resssca 16909 |
. . . . 5
⊢
((0[,]+∞) ∈ V → ℝfld =
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞)))) |
19 | 12, 18 | ax-mp 5 |
. . . 4
⊢
ℝfld =
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
20 | 19 | fveq2i 6742 |
. . 3
⊢
(ℝHom‘ℝfld) =
(ℝHom‘(Scalar‘(ℝ*𝑠
↾s (0[,]+∞)))) |
21 | | ovexd 7270 |
. . 3
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ V) |
22 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
23 | | eqid 2739 |
. . . . . . 7
⊢
(TopOpen‘𝑊) =
(TopOpen‘𝑊) |
24 | | eqid 2739 |
. . . . . . 7
⊢
(sigaGen‘(TopOpen‘𝑊)) = (sigaGen‘(TopOpen‘𝑊)) |
25 | | eqid 2739 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
26 | | eqid 2739 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
27 | | eqid 2739 |
. . . . . . 7
⊢
(ℝHom‘(Scalar‘𝑊)) = (ℝHom‘(Scalar‘𝑊)) |
28 | 22, 23, 24, 25, 26, 27, 2, 3, 4 | sibff 32047 |
. . . . . 6
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)) |
29 | | xmstps 23383 |
. . . . . . . 8
⊢ (𝑊 ∈ ∞MetSp →
𝑊 ∈
TopSp) |
30 | 22, 23 | tpsuni 21865 |
. . . . . . . 8
⊢ (𝑊 ∈ TopSp →
(Base‘𝑊) = ∪ (TopOpen‘𝑊)) |
31 | 2, 29, 30 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑊) = ∪
(TopOpen‘𝑊)) |
32 | | feq3 6550 |
. . . . . . 7
⊢
((Base‘𝑊) =
∪ (TopOpen‘𝑊) → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
34 | 28, 33 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶(Base‘𝑊)) |
35 | 22, 23, 24, 25, 26, 27, 2, 3, 5 | sibff 32047 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)) |
36 | | feq3 6550 |
. . . . . . 7
⊢
((Base‘𝑊) =
∪ (TopOpen‘𝑊) → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
37 | 31, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
38 | 35, 37 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶(Base‘𝑊)) |
39 | | dmexg 7703 |
. . . . . 6
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V) |
40 | | uniexg 7550 |
. . . . . 6
⊢ (dom
𝑀 ∈ V → ∪ dom 𝑀 ∈ V) |
41 | 3, 39, 40 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝑀 ∈ V) |
42 | 34, 38, 41 | ofresid 30730 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f (dist‘𝑊)𝐺) = (𝐹 ∘f ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝐺)) |
43 | 2, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ TopSp) |
44 | | eqid 2739 |
. . . . . . . 8
⊢
((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊))) =
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊))) |
45 | 22, 44 | xmsxmet 23386 |
. . . . . . 7
⊢ (𝑊 ∈ ∞MetSp →
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊))) ∈
(∞Met‘(Base‘𝑊))) |
46 | | xmetpsmet 23278 |
. . . . . . 7
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (PsMet‘(Base‘𝑊))) |
47 | 2, 45, 46 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈
(PsMet‘(Base‘𝑊))) |
48 | | psmetxrge0 23243 |
. . . . . 6
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (PsMet‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞)) |
49 | 47, 48 | syl 17 |
. . . . 5
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞)) |
50 | | xrge0tps 31638 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopSp |
51 | 50 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ TopSp) |
52 | 23, 22, 44 | xmstopn 23381 |
. . . . . . . 8
⊢ (𝑊 ∈ ∞MetSp →
(TopOpen‘𝑊) =
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) |
53 | 2, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (TopOpen‘𝑊) =
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) |
54 | | eqid 2739 |
. . . . . . . . 9
⊢
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) |
55 | 54 | methaus 23450 |
. . . . . . . 8
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) → (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈
Haus) |
56 | 2, 45, 55 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 →
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈ Haus) |
57 | 53, 56 | eqeltrd 2840 |
. . . . . 6
⊢ (𝜑 → (TopOpen‘𝑊) ∈ Haus) |
58 | | haust1 22281 |
. . . . . 6
⊢
((TopOpen‘𝑊)
∈ Haus → (TopOpen‘𝑊) ∈ Fre) |
59 | 57, 58 | syl 17 |
. . . . 5
⊢ (𝜑 → (TopOpen‘𝑊) ∈ Fre) |
60 | 2, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈
(∞Met‘(Base‘𝑊))) |
61 | | sitmcl.0 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Mnd) |
62 | 22, 25 | mndidcl 18221 |
. . . . . . . 8
⊢ (𝑊 ∈ Mnd →
(0g‘𝑊)
∈ (Base‘𝑊)) |
63 | 61, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑊) ∈ (Base‘𝑊)) |
64 | | xmet0 23272 |
. . . . . . 7
⊢
((((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) ∧ (0g‘𝑊) ∈ (Base‘𝑊)) →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) = 0) |
65 | 60, 63, 64 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) = 0) |
66 | 65, 11 | eqtrdi 2796 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) =
(0g‘(ℝ*𝑠
↾s (0[,]+∞)))) |
67 | 22, 23, 24, 25, 26, 27, 2, 3, 4,
7, 43, 49, 5, 51, 59, 66 | sibfof 32051 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝐺) ∈ dom
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)) |
68 | 42, 67 | eqeltrd 2840 |
. . 3
⊢ (𝜑 → (𝐹 ∘f (dist‘𝑊)𝐺) ∈ dom
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)) |
69 | | rebase 20601 |
. . . . 5
⊢ ℝ =
(Base‘ℝfld) |
70 | 69, 69 | xpeq12i 5597 |
. . . 4
⊢ (ℝ
× ℝ) = ((Base‘ℝfld) ×
(Base‘ℝfld)) |
71 | 70 | reseq2i 5866 |
. . 3
⊢
((dist‘ℝfld) ↾ (ℝ × ℝ)) =
((dist‘ℝfld) ↾ ((Base‘ℝfld)
× (Base‘ℝfld))) |
72 | | xrge0cmn 20438 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
73 | 72 | a1i 11 |
. . 3
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) |
74 | | rerrext 31703 |
. . . . 5
⊢
ℝfld ∈ ℝExt |
75 | 19, 74 | eqeltrri 2837 |
. . . 4
⊢
(Scalar‘(ℝ*𝑠
↾s (0[,]+∞))) ∈ ℝExt |
76 | 75 | a1i 11 |
. . 3
⊢ (𝜑 →
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞))) ∈ ℝExt ) |
77 | | rrhre 31715 |
. . . . . . . . 9
⊢
(ℝHom‘ℝfld) = ( I ↾
ℝ) |
78 | 77 | imaeq1i 5944 |
. . . . . . . 8
⊢
((ℝHom‘ℝfld) “ (0[,)+∞)) = (( I
↾ ℝ) “ (0[,)+∞)) |
79 | | 0re 10865 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
80 | | pnfxr 10917 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
81 | | icossre 13046 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (0[,)+∞)
⊆ ℝ) |
82 | 79, 80, 81 | mp2an 692 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
83 | | resiima 5962 |
. . . . . . . . 9
⊢
((0[,)+∞) ⊆ ℝ → (( I ↾ ℝ) “
(0[,)+∞)) = (0[,)+∞)) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . 8
⊢ (( I
↾ ℝ) “ (0[,)+∞)) = (0[,)+∞) |
85 | 78, 84 | eqtri 2767 |
. . . . . . 7
⊢
((ℝHom‘ℝfld) “ (0[,)+∞)) =
(0[,)+∞) |
86 | | icossicc 13054 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
87 | 85, 86 | eqsstri 3952 |
. . . . . 6
⊢
((ℝHom‘ℝfld) “ (0[,)+∞))
⊆ (0[,]+∞) |
88 | 87 | sseli 3913 |
. . . . 5
⊢ (𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) → 𝑚 ∈
(0[,]+∞)) |
89 | 88 | 3ad2ant2 1136 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑚 ∈
(0[,]+∞)) |
90 | | simp3 1140 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
91 | | ge0xmulcl 13081 |
. . . 4
⊢ ((𝑚 ∈ (0[,]+∞) ∧
𝑥 ∈ (0[,]+∞))
→ (𝑚
·e 𝑥)
∈ (0[,]+∞)) |
92 | 89, 90, 91 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(𝑚 ·e
𝑥) ∈
(0[,]+∞)) |
93 | 7, 9, 10, 11, 16, 20, 21, 3, 68, 19, 71, 51, 73, 76, 92 | sitgclg 32053 |
. 2
⊢ (𝜑 →
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝐹 ∘f (dist‘𝑊)𝐺)) ∈ (0[,]+∞)) |
94 | 6, 93 | eqeltrd 2840 |
1
⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞)) |