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	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
	sitmcl.1	⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
	sitmcl.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sitmcl.3	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sitmcl.4	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
Assertion	sitmcl	⊢ ( 𝜑 → ( 𝐹 ( 𝑊 sitm 𝑀 ) 𝐺 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sitmcl.0	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
2		sitmcl.1	⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
3		sitmcl.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
4		sitmcl.3	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
5		sitmcl.4	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
6		eqid	⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
7	6 2 3 4 5	sitmfval	⊢ ( 𝜑 → ( 𝐹 ( 𝑊 sitm 𝑀 ) 𝐺 ) = ( ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘_f ( dist ‘ 𝑊 ) 𝐺 ) ) )
8		xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
9		xrge0topn	⊢ ( TopOpen ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) )
10	9	eqcomi	⊢ ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
11		eqid	⊢ ( sigaGen ‘ ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) ) ) = ( sigaGen ‘ ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) ) )
12		xrge00	⊢ 0 = ( 0_g ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
13		ovex	⊢ ( 0 [,] +∞ ) ∈ V
14		eqid	⊢ ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) = ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) )
15		ax-xrsvsca	⊢ ·_e = ( ·_𝑠 ‘ ℝ^*_𝑠 )
16	14 15	ressvsca	⊢ ( ( 0 [,] +∞ ) ∈ V → ·_e = ( ·_𝑠 ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
17	13 16	ax-mp	⊢ ·_e = ( ·_𝑠 ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
18		ax-xrssca	⊢ ℝ_fld = ( Scalar ‘ ℝ^*_𝑠 )
19	14 18	resssca	⊢ ( ( 0 [,] +∞ ) ∈ V → ℝ_fld = ( Scalar ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
20	13 19	ax-mp	⊢ ℝ_fld = ( Scalar ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
21	20	fveq2i	⊢ ( ℝHom ‘ ℝ_fld ) = ( ℝHom ‘ ( Scalar ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
22		ovexd	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ V )
23		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
24		eqid	⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
25		eqid	⊢ ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) )
26		eqid	⊢ ( 0_g ‘ 𝑊 ) = ( 0_g ‘ 𝑊 )
27		eqid	⊢ ( ·_𝑠 ‘ 𝑊 ) = ( ·_𝑠 ‘ 𝑊 )
28		eqid	⊢ ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
29	23 24 25 26 27 28 2 3 4	sibff	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) )
30		xmstps	⊢ ( 𝑊 ∈ ∞MetSp → 𝑊 ∈ TopSp )
31	23 24	tpsuni	⊢ ( 𝑊 ∈ TopSp → ( Base ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) )
32	2 30 31	3syl	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) )
33		feq3	⊢ ( ( Base ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) → ( 𝐹 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) ↔ 𝐹 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) ) )
34	32 33	syl	⊢ ( 𝜑 → ( 𝐹 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) ↔ 𝐹 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) ) )
35	29 34	mpbird	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) )
36	23 24 25 26 27 28 2 3 5	sibff	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) )
37		feq3	⊢ ( ( Base ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) → ( 𝐺 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) ↔ 𝐺 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) ) )
38	32 37	syl	⊢ ( 𝜑 → ( 𝐺 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) ↔ 𝐺 : ∪ dom 𝑀 ⟶ ∪ ( TopOpen ‘ 𝑊 ) ) )
39	36 38	mpbird	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ ( Base ‘ 𝑊 ) )
40		dmexg	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V )
41		uniexg	⊢ ( dom 𝑀 ∈ V → ∪ dom 𝑀 ∈ V )
42	3 40 41	3syl	⊢ ( 𝜑 → ∪ dom 𝑀 ∈ V )
43	35 39 42	ofresid	⊢ ( 𝜑 → ( 𝐹 ∘_f ( dist ‘ 𝑊 ) 𝐺 ) = ( 𝐹 ∘_f ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝐺 ) )
44	2 30	syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
45		eqid	⊢ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) = ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) )
46	23 45	xmsxmet	⊢ ( 𝑊 ∈ ∞MetSp → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
47		xmetpsmet	⊢ ( ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( PsMet ‘ ( Base ‘ 𝑊 ) ) )
48	2 46 47	3syl	⊢ ( 𝜑 → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( PsMet ‘ ( Base ‘ 𝑊 ) ) )
49		psmetxrge0	⊢ ( ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( PsMet ‘ ( Base ‘ 𝑊 ) ) → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ( 0 [,] +∞ ) )
50	48 49	syl	⊢ ( 𝜑 → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ( 0 [,] +∞ ) )
51		xrge0tps	⊢ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ TopSp
52	51	a1i	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ TopSp )
53	24 23 45	xmstopn	⊢ ( 𝑊 ∈ ∞MetSp → ( TopOpen ‘ 𝑊 ) = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
54	2 53	syl	⊢ ( 𝜑 → ( TopOpen ‘ 𝑊 ) = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
55		eqid	⊢ ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) )
56	55	methaus	⊢ ( ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) → ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ∈ Haus )
57	2 46 56	3syl	⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ∈ Haus )
58	54 57	eqeltrd	⊢ ( 𝜑 → ( TopOpen ‘ 𝑊 ) ∈ Haus )
59		haust1	⊢ ( ( TopOpen ‘ 𝑊 ) ∈ Haus → ( TopOpen ‘ 𝑊 ) ∈ Fre )
60	58 59	syl	⊢ ( 𝜑 → ( TopOpen ‘ 𝑊 ) ∈ Fre )
61	2 46	syl	⊢ ( 𝜑 → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
62	23 26	mndidcl	⊢ ( 𝑊 ∈ Mnd → ( 0_g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
63	1 62	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
64		xmet0	⊢ ( ( ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) ∧ ( 0_g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 0_g ‘ 𝑊 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 0_g ‘ 𝑊 ) ) = 0 )
65	61 63 64	syl2anc	⊢ ( 𝜑 → ( ( 0_g ‘ 𝑊 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 0_g ‘ 𝑊 ) ) = 0 )
66	65 12	eqtrdi	⊢ ( 𝜑 → ( ( 0_g ‘ 𝑊 ) ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ( 0_g ‘ 𝑊 ) ) = ( 0_g ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
67	23 24 25 26 27 28 2 3 4 8 44 50 5 52 60 66	sibfof	⊢ ( 𝜑 → ( 𝐹 ∘_f ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝐺 ) ∈ dom ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) sitg 𝑀 ) )
68	43 67	eqeltrd	⊢ ( 𝜑 → ( 𝐹 ∘_f ( dist ‘ 𝑊 ) 𝐺 ) ∈ dom ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) sitg 𝑀 ) )
69		rebase	⊢ ℝ = ( Base ‘ ℝ_fld )
70	69 69	xpeq12i	⊢ ( ℝ × ℝ ) = ( ( Base ‘ ℝ_fld ) × ( Base ‘ ℝ_fld ) )
71	70	reseq2i	⊢ ( ( dist ‘ ℝ_fld ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝ_fld ) ↾ ( ( Base ‘ ℝ_fld ) × ( Base ‘ ℝ_fld ) ) )
72		xrge0cmn	⊢ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ CMnd
73	72	a1i	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ CMnd )
74		rerrext	⊢ ℝ_fld ∈ ℝExt
75	20 74	eqeltrri	⊢ ( Scalar ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) ∈ ℝExt
76	75	a1i	⊢ ( 𝜑 → ( Scalar ‘ ( ℝ^*_𝑠 ↾_s ( 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	⊢ ( 𝑚 ∈ ( ( ℝHom ‘ ℝ_fld ) “ ( 0 [,) +∞ ) ) → 𝑚 ∈ ( 0 [,] +∞ ) )
89	88	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ℝHom ‘ ℝ_fld ) “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝑚 ∈ ( 0 [,] +∞ ) )
90		simp3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ℝHom ‘ ℝ_fld ) “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
91		ge0xmulcl	⊢ ( ( 𝑚 ∈ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑚 ·_e 𝑥 ) ∈ ( 0 [,] +∞ ) )
92	89 90 91	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ℝHom ‘ ℝ_fld ) “ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑚 ·_e 𝑥 ) ∈ ( 0 [,] +∞ ) )
93	8 10 11 12 17 21 22 3 68 20 71 52 73 76 92	sitgclg	⊢ ( 𝜑 → ( ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) sitg 𝑀 ) ‘ ( 𝐹 ∘_f ( dist ‘ 𝑊 ) 𝐺 ) ) ∈ ( 0 [,] +∞ ) )
94	7 93	eqeltrd	⊢ ( 𝜑 → ( 𝐹 ( 𝑊 sitm 𝑀 ) 𝐺 ) ∈ ( 0 [,] +∞ ) )

Metamath Proof Explorer

Theorem sitmcl

Proof