sitmval

Description: Value of the simple function integral metric for a given space W and measure M . (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitmval.d	$⊢ D = dist (W)$
	sitmval.1	$⊢ φ \to W \in V$
	sitmval.2	$⊢ φ \to M \in ⋃ ran measures$
Assertion	sitmval	$⊢ φ \to W sitm M = (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f D_{f} g) d M)$

Proof

Step	Hyp	Ref	Expression
1		sitmval.d	$⊢ D = dist (W)$
2		sitmval.1	$⊢ φ \to W \in V$
3		sitmval.2	$⊢ φ \to M \in ⋃ ran measures$
4		elex	$⊢ W \in V \to W \in V$
5	2 4	syl	$⊢ φ \to W \in V$
6		oveq1	$⊢ w = W \to w sitg m = W sitg m$
7	6	dmeqd	$⊢ w = W \to ℑ_{m}^{w} = ℑ_{m}^{W}$
8		fveq2	$⊢ w = W \to dist (w) = dist (W)$
9	8	ofeqd	$⊢ w = W \to \circ_{f} dist (w) = \circ_{f} dist (W)$
10	9	oveqd	$⊢ w = W \to f {dist (w)}_{f} g = f {dist (W)}_{f} g$
11	10	fveq2d	$⊢ w = W \to \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m = \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d m$
12	7 7 11	mpoeq123dv	$⊢ w = W \to (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)$
13		oveq2	$⊢ m = M \to W sitg m = W sitg M$
14	13	dmeqd	$⊢ m = M \to ℑ_{m}^{W} = ℑ_{M}^{W}$
15		oveq2	$⊢ m = M \to (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) sitg m = (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) sitg M$
16	1	eqcomi	$⊢ dist (W) = D$
17		ofeq	$⊢ dist (W) = D \to \circ_{f} dist (W) = \circ_{f} D$
18	16 17	mp1i	$⊢ m = M \to \circ_{f} dist (W) = \circ_{f} D$
19	18	oveqd	$⊢ m = M \to f {dist (W)}_{f} g = f D_{f} g$
20	15 19	fveq12d	$⊢ m = M \to \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f {dist (W)}_{f} g) d m = \int_{ℑ}^{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])} (f D_{f} g) d M$
21	14 14 20	mpoeq123dv	$⊢ m = M \to (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 D_{f} g) d M)$
22		df-sitm	$⊢ sitm = (w \in V, m \in ⋃ ran measures ⟼ (f \in ℑ_{m}^{w}, g \in ℑ_{m}^{w} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m))$
23		ovex	$⊢ W sitg M \in V$
24	23	dmex	$⊢ ℑ_{M}^{W} \in V$
25	24 24	mpoex	$⊢ (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f D_{f} g) d M) \in V$
26	12 21 22 25	ovmpo	$⊢ (W \in V \land M \in ⋃ ran measures) \to W sitm M = (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f D_{f} g) d M)$
27	5 3 26	syl2anc	$⊢ φ \to W sitm M = (f \in ℑ_{M}^{W}, g \in ℑ_{M}^{W} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f D_{f} g) d M)$

Metamath Proof Explorer

Theorem sitmval

Proof