Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 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 29739 |
. 2
⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) =
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝐹 ∘𝑓
(dist‘𝑊)𝐺))) |
7 | | xrge0base 29016 |
. . 3
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
8 | | xrge0topn 29317 |
. . . 4
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
9 | 8 | eqcomi 2619 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
10 | | eqid 2610 |
. . 3
⊢
(sigaGen‘((ordTop‘ ≤ ) ↾t
(0[,]+∞))) = (sigaGen‘((ordTop‘ ≤ ) ↾t
(0[,]+∞))) |
11 | | xrge00 29017 |
. . 3
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
12 | | ovex 6577 |
. . . 4
⊢
(0[,]+∞) ∈ V |
13 | | eqid 2610 |
. . . . 5
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
14 | | ax-xrsvsca 29005 |
. . . . 5
⊢
·e = ( ·𝑠
‘ℝ*𝑠) |
15 | 13, 14 | ressvsca 15855 |
. . . 4
⊢
((0[,]+∞) ∈ V → ·e = (
·𝑠
‘(ℝ*𝑠 ↾s
(0[,]+∞)))) |
16 | 12, 15 | ax-mp 5 |
. . 3
⊢
·e = ( ·𝑠
‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
17 | | ax-xrssca 29004 |
. . . . . 6
⊢
ℝfld =
(Scalar‘ℝ*𝑠) |
18 | 13, 17 | resssca 15854 |
. . . . 5
⊢
((0[,]+∞) ∈ V → ℝfld =
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞)))) |
19 | 12, 18 | ax-mp 5 |
. . . 4
⊢
ℝfld =
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
20 | 19 | fveq2i 6106 |
. . 3
⊢
(ℝHom‘ℝfld) =
(ℝHom‘(Scalar‘(ℝ*𝑠
↾s (0[,]+∞)))) |
21 | | ovex 6577 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ V |
22 | 21 | a1i 11 |
. . 3
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ V) |
23 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
24 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘𝑊) =
(TopOpen‘𝑊) |
25 | | eqid 2610 |
. . . . . . 7
⊢
(sigaGen‘(TopOpen‘𝑊)) = (sigaGen‘(TopOpen‘𝑊)) |
26 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
27 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
28 | | eqid 2610 |
. . . . . . 7
⊢
(ℝHom‘(Scalar‘𝑊)) = (ℝHom‘(Scalar‘𝑊)) |
29 | 23, 24, 25, 26, 27, 28, 2, 3, 4 | sibff 29725 |
. . . . . 6
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)) |
30 | | xmstps 22068 |
. . . . . . . 8
⊢ (𝑊 ∈ ∞MetSp →
𝑊 ∈
TopSp) |
31 | 23, 24 | tpsuni 20553 |
. . . . . . . 8
⊢ (𝑊 ∈ TopSp →
(Base‘𝑊) = ∪ (TopOpen‘𝑊)) |
32 | 2, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑊) = ∪
(TopOpen‘𝑊)) |
33 | | feq3 5941 |
. . . . . . 7
⊢
((Base‘𝑊) =
∪ (TopOpen‘𝑊) → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
35 | 29, 34 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶(Base‘𝑊)) |
36 | 23, 24, 25, 26, 27, 28, 2, 3, 5 | sibff 29725 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)) |
37 | | feq3 5941 |
. . . . . . 7
⊢
((Base‘𝑊) =
∪ (TopOpen‘𝑊) → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
38 | 32, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))) |
39 | 36, 38 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶(Base‘𝑊)) |
40 | | dmexg 6989 |
. . . . . 6
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V) |
41 | | uniexg 6853 |
. . . . . 6
⊢ (dom
𝑀 ∈ V → ∪ dom 𝑀 ∈ V) |
42 | 3, 40, 41 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝑀 ∈ V) |
43 | 35, 39, 42 | ofresid 28824 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓
(dist‘𝑊)𝐺) = (𝐹 ∘𝑓
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊)))𝐺)) |
44 | 2, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ TopSp) |
45 | | eqid 2610 |
. . . . . . . 8
⊢
((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊))) =
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊))) |
46 | 23, 45 | xmsxmet 22071 |
. . . . . . 7
⊢ (𝑊 ∈ ∞MetSp →
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊))) ∈
(∞Met‘(Base‘𝑊))) |
47 | | xmetpsmet 21963 |
. . . . . . 7
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (PsMet‘(Base‘𝑊))) |
48 | 2, 46, 47 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈
(PsMet‘(Base‘𝑊))) |
49 | | psmetxrge0 21928 |
. . . . . 6
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (PsMet‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞)) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞)) |
51 | | xrge0tps 29316 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopSp |
52 | 51 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ TopSp) |
53 | 24, 23, 45 | xmstopn 22066 |
. . . . . . . 8
⊢ (𝑊 ∈ ∞MetSp →
(TopOpen‘𝑊) =
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) |
54 | 2, 53 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (TopOpen‘𝑊) =
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) |
55 | | eqid 2610 |
. . . . . . . . 9
⊢
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) |
56 | 55 | methaus 22135 |
. . . . . . . 8
⊢
(((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) → (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈
Haus) |
57 | 2, 46, 56 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 →
(MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈ Haus) |
58 | 54, 57 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → (TopOpen‘𝑊) ∈ Haus) |
59 | | haust1 20966 |
. . . . . 6
⊢
((TopOpen‘𝑊)
∈ Haus → (TopOpen‘𝑊) ∈ Fre) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ (𝜑 → (TopOpen‘𝑊) ∈ Fre) |
61 | 2, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈
(∞Met‘(Base‘𝑊))) |
62 | | sitmcl.0 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Mnd) |
63 | 23, 26 | mndidcl 17131 |
. . . . . . . 8
⊢ (𝑊 ∈ Mnd →
(0g‘𝑊)
∈ (Base‘𝑊)) |
64 | 62, 63 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑊) ∈ (Base‘𝑊)) |
65 | | xmet0 21957 |
. . . . . . 7
⊢
((((dist‘𝑊)
↾ ((Base‘𝑊)
× (Base‘𝑊)))
∈ (∞Met‘(Base‘𝑊)) ∧ (0g‘𝑊) ∈ (Base‘𝑊)) →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) = 0) |
66 | 61, 64, 65 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) = 0) |
67 | 66, 11 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0g‘𝑊)) =
(0g‘(ℝ*𝑠
↾s (0[,]+∞)))) |
68 | 23, 24, 25, 26, 27, 28, 2, 3, 4,
7, 44, 50, 5, 52, 60, 67 | sibfof 29729 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓
((dist‘𝑊) ↾
((Base‘𝑊) ×
(Base‘𝑊)))𝐺) ∈ dom
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)) |
69 | 43, 68 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓
(dist‘𝑊)𝐺) ∈ dom
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)) |
70 | | rebase 19771 |
. . . . 5
⊢ ℝ =
(Base‘ℝfld) |
71 | 70, 70 | xpeq12i 5061 |
. . . 4
⊢ (ℝ
× ℝ) = ((Base‘ℝfld) ×
(Base‘ℝfld)) |
72 | 71 | reseq2i 5314 |
. . 3
⊢
((dist‘ℝfld) ↾ (ℝ × ℝ)) =
((dist‘ℝfld) ↾ ((Base‘ℝfld)
× (Base‘ℝfld))) |
73 | | xrge0cmn 19607 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
74 | 73 | a1i 11 |
. . 3
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) |
75 | | rerrext 29381 |
. . . . 5
⊢
ℝfld ∈ ℝExt |
76 | 19, 75 | eqeltrri 2685 |
. . . 4
⊢
(Scalar‘(ℝ*𝑠
↾s (0[,]+∞))) ∈ ℝExt |
77 | 76 | a1i 11 |
. . 3
⊢ (𝜑 →
(Scalar‘(ℝ*𝑠 ↾s
(0[,]+∞))) ∈ ℝExt ) |
78 | | rrhre 29393 |
. . . . . . . . 9
⊢
(ℝHom‘ℝfld) = ( I ↾
ℝ) |
79 | 78 | imaeq1i 5382 |
. . . . . . . 8
⊢
((ℝHom‘ℝfld) “ (0[,)+∞)) = (( I
↾ ℝ) “ (0[,)+∞)) |
80 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
81 | | pnfxr 9971 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
82 | | icossre 12125 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (0[,)+∞)
⊆ ℝ) |
83 | 80, 81, 82 | mp2an 704 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
84 | | resiima 5399 |
. . . . . . . . 9
⊢
((0[,)+∞) ⊆ ℝ → (( I ↾ ℝ) “
(0[,)+∞)) = (0[,)+∞)) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . 8
⊢ (( I
↾ ℝ) “ (0[,)+∞)) = (0[,)+∞) |
86 | 79, 85 | eqtri 2632 |
. . . . . . 7
⊢
((ℝHom‘ℝfld) “ (0[,)+∞)) =
(0[,)+∞) |
87 | | icossicc 12131 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
88 | 86, 87 | eqsstri 3598 |
. . . . . 6
⊢
((ℝHom‘ℝfld) “ (0[,)+∞))
⊆ (0[,]+∞) |
89 | 88 | sseli 3564 |
. . . . 5
⊢ (𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) → 𝑚 ∈
(0[,]+∞)) |
90 | 89 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑚 ∈
(0[,]+∞)) |
91 | | simp3 1056 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
92 | | ge0xmulcl 12158 |
. . . 4
⊢ ((𝑚 ∈ (0[,]+∞) ∧
𝑥 ∈ (0[,]+∞))
→ (𝑚
·e 𝑥)
∈ (0[,]+∞)) |
93 | 90, 91, 92 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈
((ℝHom‘ℝfld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(𝑚 ·e
𝑥) ∈
(0[,]+∞)) |
94 | 7, 9, 10, 11, 16, 20, 22, 3, 69, 19, 72, 52, 74, 77, 93 | sitgclg 29731 |
. 2
⊢ (𝜑 →
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑀)‘(𝐹 ∘𝑓
(dist‘𝑊)𝐺)) ∈
(0[,]+∞)) |
95 | 6, 94 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞)) |