Metamath Proof Explorer

Theorem sitmf

Description: The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018)

		Ref	Expression
	Hypotheses	sitmf.0	$⊢ φ \to W \in Mnd$
		sitmf.1	$⊢ φ \to W \in ∞MetSp$
		sitmf.2	$⊢ φ \to M \in ⋃ ran measures$
	Assertion	sitmf	$⊢ φ \to {\| . - . \|}_{M}^{W} : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		sitmf.0	$⊢ φ \to W \in Mnd$
2		sitmf.1	$⊢ φ \to W \in ∞MetSp$
3		sitmf.2	$⊢ φ \to M \in ⋃ ran measures$
4		eqid	$⊢ dist (W) = dist (W)$
5	2	adantr	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to W \in ∞MetSp$
6	3	adantr	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to M \in ⋃ ran measures$
7		simprl	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to f \in ℑ_{M}^{W}$
8		simprr	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to g \in ℑ_{M}^{W}$
9	4 5 6 7 8	sitmfval	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to {\| g - f \|}_{M}^{W} = \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M$
10	1	adantr	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to W \in Mnd$
11	10 5 6 7 8	sitmcl	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to {\| g - f \|}_{M}^{W} \in [0, +∞]$
12	9 11	eqeltrrd	$⊢ (φ \land (f \in ℑ_{M}^{W} \land g \in ℑ_{M}^{W})) \to \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M \in [0, +∞]$
13	12	ralrimivva	$⊢ φ \to \forall f \in ℑ_{M}^{W} \forall g \in ℑ_{M}^{W} \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M \in [0, +∞]$
14		eqid	$⊢ (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M) = (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M)$
15	14	fmpo	$⊢ \forall f \in ℑ_{M}^{W} \forall g \in ℑ_{M}^{W} \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M \in [0, +∞] \leftrightarrow (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M) : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞]$
16	13 15	sylib	$⊢ φ \to (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M) : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞]$
17	4 2 3	sitmval	$⊢ φ \to W sitm M = (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M)$
18	17	feq1d	$⊢ φ \to ({\| . - . \|}_{M}^{W} : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞] \leftrightarrow (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d M) : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞])$
19	16 18	mpbird	$⊢ φ \to {\| . - . \|}_{M}^{W} : ℑ_{M}^{W} \times ℑ_{M}^{W} ⟶ [0, +∞]$