Metamath Proof Explorer

Theorem sitmcl

Description: Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018)

Ref Expression
Hypotheses sitmcl.0 ⊢ φ → W ∈ Mnd
sitmcl.1 ⊢ φ → W ∈ ∞MetSp
sitmcl.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
sitmcl.3 ⊢ φ → F ∈ ℑ M W
sitmcl.4 ⊢ φ → G ∈ ℑ M W
Assertion sitmcl ⊢ φ → |G - F| M W ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 sitmcl.0 ⊢ φ → W ∈ Mnd
2 sitmcl.1 ⊢ φ → W ∈ ∞MetSp
3 sitmcl.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
4 sitmcl.3 ⊢ φ → F ∈ ℑ M W
5 sitmcl.4 ⊢ φ → G ∈ ℑ M W
6 eqid ⊢ dist ⁡ W = dist ⁡ W
7 6 2 3 4 5 sitmfval ⊢ φ → |G - F| M W = ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F dist ⁡ W f G dM
8 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
9 xrge0topn ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
10 9 eqcomi ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
11 eqid ⊢ 𝛔 ⁡ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = 𝛔 ⁡ ordTop ⁡ ≤ ↾ 𝑡 0 +∞
12 xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
13 ovex ⊢ 0 +∞ ∈ V
14 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
15 ax-xrsvsca ⊢ ⋅ 𝑒 = ⋅ ℝ 𝑠 *
16 14 15 ressvsca ⊢ 0 +∞ ∈ V → ⋅ 𝑒 = ⋅ ℝ 𝑠 * ↾ 𝑠 0 +∞
17 13 16 ax-mp ⊢ ⋅ 𝑒 = ⋅ ℝ 𝑠 * ↾ 𝑠 0 +∞
18 ax-xrssca ⊢ ℝ fld = Scalar ⁡ ℝ 𝑠 *
19 14 18 resssca ⊢ 0 +∞ ∈ V → ℝ fld = Scalar ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
20 13 19 ax-mp ⊢ ℝ fld = Scalar ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
21 20 fveq2i ⊢ ℝHom ⁡ ℝ fld = ℝHom ⁡ Scalar ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
22 ovexd ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ V
23 eqid ⊢ Base W = Base W
24 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
25 eqid ⊢ 𝛔 ⁡ TopOpen ⁡ W = 𝛔 ⁡ TopOpen ⁡ W
26 eqid ⊢ 0 W = 0 W
27 eqid ⊢ ⋅ W = ⋅ W
28 eqid ⊢ ℝHom ⁡ Scalar ⁡ W = ℝHom ⁡ Scalar ⁡ W
29 23 24 25 26 27 28 2 3 4 sibff ⊢ φ → F : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
30 xmstps ⊢ W ∈ ∞MetSp → W ∈ TopSp
31 23 24 tpsuni ⊢ W ∈ TopSp → Base W = ⋃ TopOpen ⁡ W
32 2 30 31 3syl ⊢ φ → Base W = ⋃ TopOpen ⁡ W
33 feq3 ⊢ Base W = ⋃ TopOpen ⁡ W → F : ⋃ dom ⁡ M ⟶ Base W ↔ F : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
34 32 33 syl ⊢ φ → F : ⋃ dom ⁡ M ⟶ Base W ↔ F : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
35 29 34 mpbird ⊢ φ → F : ⋃ dom ⁡ M ⟶ Base W
36 23 24 25 26 27 28 2 3 5 sibff ⊢ φ → G : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
37 feq3 ⊢ Base W = ⋃ TopOpen ⁡ W → G : ⋃ dom ⁡ M ⟶ Base W ↔ G : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
38 32 37 syl ⊢ φ → G : ⋃ dom ⁡ M ⟶ Base W ↔ G : ⋃ dom ⁡ M ⟶ ⋃ TopOpen ⁡ W
39 36 38 mpbird ⊢ φ → G : ⋃ dom ⁡ M ⟶ Base W
40 dmexg ⊢ M ∈ ⋃ ran ⁡ measures → dom ⁡ M ∈ V
41 uniexg ⊢ dom ⁡ M ∈ V → ⋃ dom ⁡ M ∈ V
42 3 40 41 3syl ⊢ φ → ⋃ dom ⁡ M ∈ V
43 35 39 42 ofresid ⊢ φ → F dist ⁡ W f G = F dist ⁡ W ↾ Base W × Base W f G
44 2 30 syl ⊢ φ → W ∈ TopSp
45 eqid ⊢ dist ⁡ W ↾ Base W × Base W = dist ⁡ W ↾ Base W × Base W
46 23 45 xmsxmet ⊢ W ∈ ∞MetSp → dist ⁡ W ↾ Base W × Base W ∈ ∞Met ⁡ Base W
47 xmetpsmet ⊢ dist ⁡ W ↾ Base W × Base W ∈ ∞Met ⁡ Base W → dist ⁡ W ↾ Base W × Base W ∈ PsMet ⁡ Base W
48 2 46 47 3syl ⊢ φ → dist ⁡ W ↾ Base W × Base W ∈ PsMet ⁡ Base W
49 psmetxrge0 ⊢ dist ⁡ W ↾ Base W × Base W ∈ PsMet ⁡ Base W → dist ⁡ W ↾ Base W × Base W : Base W × Base W ⟶ 0 +∞
50 48 49 syl ⊢ φ → dist ⁡ W ↾ Base W × Base W : Base W × Base W ⟶ 0 +∞
51 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
52 51 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
53 24 23 45 xmstopn ⊢ W ∈ ∞MetSp → TopOpen ⁡ W = MetOpen ⁡ dist ⁡ W ↾ Base W × Base W
54 2 53 syl ⊢ φ → TopOpen ⁡ W = MetOpen ⁡ dist ⁡ W ↾ Base W × Base W
55 eqid ⊢ MetOpen ⁡ dist ⁡ W ↾ Base W × Base W = MetOpen ⁡ dist ⁡ W ↾ Base W × Base W
56 55 methaus ⊢ dist ⁡ W ↾ Base W × Base W ∈ ∞Met ⁡ Base W → MetOpen ⁡ dist ⁡ W ↾ Base W × Base W ∈ Haus
57 2 46 56 3syl ⊢ φ → MetOpen ⁡ dist ⁡ W ↾ Base W × Base W ∈ Haus
58 54 57 eqeltrd ⊢ φ → TopOpen ⁡ W ∈ Haus
59 haust1 ⊢ TopOpen ⁡ W ∈ Haus → TopOpen ⁡ W ∈ Fre
60 58 59 syl ⊢ φ → TopOpen ⁡ W ∈ Fre
61 2 46 syl ⊢ φ → dist ⁡ W ↾ Base W × Base W ∈ ∞Met ⁡ Base W
62 23 26 mndidcl ⊢ W ∈ Mnd → 0 W ∈ Base W
63 1 62 syl ⊢ φ → 0 W ∈ Base W
64 xmet0 ⊢ dist ⁡ W ↾ Base W × Base W ∈ ∞Met ⁡ Base W ∧ 0 W ∈ Base W → 0 W dist ⁡ W ↾ Base W × Base W 0 W = 0
65 61 63 64 syl2anc ⊢ φ → 0 W dist ⁡ W ↾ Base W × Base W 0 W = 0
66 65 12 eqtrdi ⊢ φ → 0 W dist ⁡ W ↾ Base W × Base W 0 W = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
67 23 24 25 26 27 28 2 3 4 8 44 50 5 52 60 66 sibfof ⊢ φ → F dist ⁡ W ↾ Base W × Base W f G ∈ ℑ M ℝ 𝑠 * ↾ 𝑠 0 +∞
68 43 67 eqeltrd ⊢ φ → F dist ⁡ W f G ∈ ℑ M ℝ 𝑠 * ↾ 𝑠 0 +∞
69 rebase ⊢ ℝ = Base ℝ fld
70 69 69 xpeq12i ⊢ ℝ 2 = Base ℝ fld × Base ℝ fld
71 70 reseq2i ⊢ dist ⁡ ℝ fld ↾ ℝ 2 = dist ⁡ ℝ fld ↾ Base ℝ fld × Base ℝ fld
72 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
73 72 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
74 rerrext ⊢ ℝ fld ∈ ℝExt
75 20 74 eqeltrri ⊢ Scalar ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ ℝExt
76 75 a1i ⊢ φ → Scalar ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ ℝExt
77 rrhre ⊢ ℝHom ⁡ ℝ fld = I ↾ ℝ
78 77 imaeq1i ⊢ ℝHom ⁡ ℝ fld 0 +∞ = I ↾ ℝ 0 +∞
79 0re ⊢ 0 ∈ ℝ
80 pnfxr ⊢ +∞ ∈ ℝ *
81 icossre ⊢ 0 ∈ ℝ ∧ +∞ ∈ ℝ * → 0 +∞ ⊆ ℝ
82 79 80 81 mp2an ⊢ 0 +∞ ⊆ ℝ
83 resiima ⊢ 0 +∞ ⊆ ℝ → I ↾ ℝ 0 +∞ = 0 +∞
84 82 83 ax-mp ⊢ I ↾ ℝ 0 +∞ = 0 +∞
85 78 84 eqtri ⊢ ℝHom ⁡ ℝ fld 0 +∞ = 0 +∞
86 icossicc ⊢ 0 +∞ ⊆ 0 +∞
87 85 86 eqsstri ⊢ ℝHom ⁡ ℝ fld 0 +∞ ⊆ 0 +∞
88 87 sseli ⊢ m ∈ ℝHom ⁡ ℝ fld 0 +∞ → m ∈ 0 +∞
89 88 3ad2ant2 ⊢ φ ∧ m ∈ ℝHom ⁡ ℝ fld 0 +∞ ∧ x ∈ 0 +∞ → m ∈ 0 +∞
90 simp3 ⊢ φ ∧ m ∈ ℝHom ⁡ ℝ fld 0 +∞ ∧ x ∈ 0 +∞ → x ∈ 0 +∞
91 ge0xmulcl ⊢ m ∈ 0 +∞ ∧ x ∈ 0 +∞ → m ⋅ 𝑒 x ∈ 0 +∞
92 89 90 91 syl2anc ⊢ φ ∧ m ∈ ℝHom ⁡ ℝ fld 0 +∞ ∧ x ∈ 0 +∞ → m ⋅ 𝑒 x ∈ 0 +∞
93 8 10 11 12 17 21 22 3 68 20 71 52 73 76 92 sitgclg ⊢ φ → ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F dist ⁡ W f G dM ∈ 0 +∞
94 7 93 eqeltrd ⊢ φ → |G - F| M W ∈ 0 +∞