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	|- ( ph -> W e. Mnd )
	sitmcl.1	|- ( ph -> W e. *MetSp )
	sitmcl.2	|- ( ph -> M e. U. ran measures )
	sitmcl.3	|- ( ph -> F e. dom ( W sitg M ) )
	sitmcl.4	|- ( ph -> G e. dom ( W sitg M ) )
Assertion	sitmcl	|- ( ph -> ( F ( W sitm M ) G ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		sitmcl.0	|- ( ph -> W e. Mnd )
2		sitmcl.1	|- ( ph -> W e. *MetSp )
3		sitmcl.2	|- ( ph -> M e. U. ran measures )
4		sitmcl.3	|- ( ph -> F e. dom ( W sitg M ) )
5		sitmcl.4	|- ( ph -> G e. dom ( W sitg M ) )
6		eqid	|- ( dist ` W ) = ( dist ` W )
7	6 2 3 4 5	sitmfval	|- ( ph -> ( F ( W sitm M ) G ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF ( dist ` W ) G ) ) )
8		xrge0base	|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
9		xrge0topn	|- ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
10	9	eqcomi	|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
11		eqid	|- ( sigaGen ` ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) = ( sigaGen ` ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
12		xrge00	|- 0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
13		ovex	|- ( 0 [,] +oo ) e. _V
14		eqid	|- ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
15		ax-xrsvsca	|- *e = ( .s ` RR*s )
16	14 15	ressvsca	|- ( ( 0 [,] +oo ) e. _V -> *e = ( .s ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
17	13 16	ax-mp	|- *e = ( .s ` ( RR*s |`s ( 0 [,] +oo ) ) )
18		ax-xrssca	|- RRfld = ( Scalar ` RR*s )
19	14 18	resssca	|- ( ( 0 [,] +oo ) e. _V -> RRfld = ( Scalar ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
20	13 19	ax-mp	|- RRfld = ( Scalar ` ( RR*s |`s ( 0 [,] +oo ) ) )
21	20	fveq2i	|- ( RRHom ` RRfld ) = ( RRHom ` ( Scalar ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
22		ovexd	|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. _V )
23		eqid	|- ( Base ` W ) = ( Base ` W )
24		eqid	|- ( TopOpen ` W ) = ( TopOpen ` W )
25		eqid	|- ( sigaGen ` ( TopOpen ` W ) ) = ( sigaGen ` ( TopOpen ` W ) )
26		eqid	|- ( 0g ` W ) = ( 0g ` W )
27		eqid	|- ( .s ` W ) = ( .s ` W )
28		eqid	|- ( RRHom ` ( Scalar ` W ) ) = ( RRHom ` ( Scalar ` W ) )
29	23 24 25 26 27 28 2 3 4	sibff	|- ( ph -> F : U. dom M --> U. ( TopOpen ` W ) )
30		xmstps	|- ( W e. *MetSp -> W e. TopSp )
31	23 24	tpsuni	|- ( W e. TopSp -> ( Base ` W ) = U. ( TopOpen ` W ) )
32	2 30 31	3syl	|- ( ph -> ( Base ` W ) = U. ( TopOpen ` W ) )
33		feq3	|- ( ( Base ` W ) = U. ( TopOpen ` W ) -> ( F : U. dom M --> ( Base ` W ) <-> F : U. dom M --> U. ( TopOpen ` W ) ) )
34	32 33	syl	|- ( ph -> ( F : U. dom M --> ( Base ` W ) <-> F : U. dom M --> U. ( TopOpen ` W ) ) )
35	29 34	mpbird	|- ( ph -> F : U. dom M --> ( Base ` W ) )
36	23 24 25 26 27 28 2 3 5	sibff	|- ( ph -> G : U. dom M --> U. ( TopOpen ` W ) )
37		feq3	|- ( ( Base ` W ) = U. ( TopOpen ` W ) -> ( G : U. dom M --> ( Base ` W ) <-> G : U. dom M --> U. ( TopOpen ` W ) ) )
38	32 37	syl	|- ( ph -> ( G : U. dom M --> ( Base ` W ) <-> G : U. dom M --> U. ( TopOpen ` W ) ) )
39	36 38	mpbird	|- ( ph -> G : U. dom M --> ( Base ` W ) )
40		dmexg	|- ( M e. U. ran measures -> dom M e. _V )
41		uniexg	|- ( dom M e. _V -> U. dom M e. _V )
42	3 40 41	3syl	|- ( ph -> U. dom M e. _V )
43	35 39 42	ofresid	|- ( ph -> ( F oF ( dist ` W ) G ) = ( F oF ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) G ) )
44	2 30	syl	|- ( ph -> W e. TopSp )
45		eqid	|- ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) )
46	23 45	xmsxmet	|- ( W e. *MetSp -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
47		xmetpsmet	|- ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( PsMet ` ( Base ` W ) ) )
48	2 46 47	3syl	|- ( ph -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( PsMet ` ( Base ` W ) ) )
49		psmetxrge0	|- ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( PsMet ` ( Base ` W ) ) -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) : ( ( Base ` W ) X. ( Base ` W ) ) --> ( 0 [,] +oo ) )
50	48 49	syl	|- ( ph -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) : ( ( Base ` W ) X. ( Base ` W ) ) --> ( 0 [,] +oo ) )
51		xrge0tps	|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
52	51	a1i	|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
53	24 23 45	xmstopn	|- ( W e. *MetSp -> ( TopOpen ` W ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
54	2 53	syl	|- ( ph -> ( TopOpen ` W ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
55		eqid	|- ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) )
56	55	methaus	|- ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) -> ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) e. Haus )
57	2 46 56	3syl	|- ( ph -> ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) e. Haus )
58	54 57	eqeltrd	|- ( ph -> ( TopOpen ` W ) e. Haus )
59		haust1	|- ( ( TopOpen ` W ) e. Haus -> ( TopOpen ` W ) e. Fre )
60	58 59	syl	|- ( ph -> ( TopOpen ` W ) e. Fre )
61	2 46	syl	|- ( ph -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
62	23 26	mndidcl	|- ( W e. Mnd -> ( 0g ` W ) e. ( Base ` W ) )
63	1 62	syl	|- ( ph -> ( 0g ` W ) e. ( Base ` W ) )
64		xmet0	|- ( ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) /\ ( 0g ` W ) e. ( Base ` W ) ) -> ( ( 0g ` W ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( 0g ` W ) ) = 0 )
65	61 63 64	syl2anc	|- ( ph -> ( ( 0g ` W ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( 0g ` W ) ) = 0 )
66	65 12	eqtrdi	|- ( ph -> ( ( 0g ` W ) ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ( 0g ` W ) ) = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
67	23 24 25 26 27 28 2 3 4 8 44 50 5 52 60 66	sibfof	|- ( ph -> ( F oF ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) G ) e. dom ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) )
68	43 67	eqeltrd	|- ( ph -> ( F oF ( dist ` W ) G ) e. dom ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) )
69		rebase	|- RR = ( Base ` RRfld )
70	69 69	xpeq12i	|- ( RR X. RR ) = ( ( Base ` RRfld ) X. ( Base ` RRfld ) )
71	70	reseq2i	|- ( ( dist ` RRfld ) |` ( RR X. RR ) ) = ( ( dist ` RRfld ) |` ( ( Base ` RRfld ) X. ( Base ` RRfld ) ) )
72		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
73	72	a1i	|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
74		rerrext	|- RRfld e. RRExt
75	20 74	eqeltrri	|- ( Scalar ` ( RR*s |`s ( 0 [,] +oo ) ) ) e. RRExt
76	75	a1i	|- ( ph -> ( Scalar ` ( RR*s |`s ( 0 [,] +oo ) ) ) e. RRExt )
77		rrhre	|- ( RRHom ` RRfld ) = ( _I |` RR )
78	77	imaeq1i	|- ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) = ( ( _I |` RR ) " ( 0 [,) +oo ) )
79		0re	|- 0 e. RR
80		pnfxr	|- +oo e. RR*
81		icossre	|- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
82	79 80 81	mp2an	|- ( 0 [,) +oo ) C_ RR
83		resiima	|- ( ( 0 [,) +oo ) C_ RR -> ( ( _I |` RR ) " ( 0 [,) +oo ) ) = ( 0 [,) +oo ) )
84	82 83	ax-mp	|- ( ( _I |` RR ) " ( 0 [,) +oo ) ) = ( 0 [,) +oo )
85	78 84	eqtri	|- ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) = ( 0 [,) +oo )
86		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
87	85 86	eqsstri	|- ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) C_ ( 0 [,] +oo )
88	87	sseli	|- ( m e. ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) -> m e. ( 0 [,] +oo ) )
89	88	3ad2ant2	|- ( ( ph /\ m e. ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> m e. ( 0 [,] +oo ) )
90		simp3	|- ( ( ph /\ m e. ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> x e. ( 0 [,] +oo ) )
91		ge0xmulcl	|- ( ( m e. ( 0 [,] +oo ) /\ x e. ( 0 [,] +oo ) ) -> ( m *e x ) e. ( 0 [,] +oo ) )
92	89 90 91	syl2anc	|- ( ( ph /\ m e. ( ( RRHom ` RRfld ) " ( 0 [,) +oo ) ) /\ x e. ( 0 [,] +oo ) ) -> ( m *e x ) e. ( 0 [,] +oo ) )
93	8 10 11 12 17 21 22 3 68 20 71 52 73 76 92	sitgclg	|- ( ph -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF ( dist ` W ) G ) ) e. ( 0 [,] +oo ) )
94	7 93	eqeltrd	|- ( ph -> ( F ( W sitm M ) G ) e. ( 0 [,] +oo ) )