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	$⊢ φ \to W \in Mnd$
	sitmcl.1	$⊢ φ \to W \in ∞MetSp$
	sitmcl.2	$⊢ φ \to M \in ⋃ ran measures$
	sitmcl.3	$⊢ φ \to F \in ℑ_{M}^{W}$
	sitmcl.4	$⊢ φ \to G \in ℑ_{M}^{W}$
Assertion	sitmcl	$⊢ φ \to {\| G - F \|}_{M}^{W} \in [0, +∞]$

Proof

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

Metamath Proof Explorer

Theorem sitmcl

Proof