Theorem sitmfval

Description: Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitmval.d	$$⊢D=\mathrm{dist}\left(W\right)$$
	sitmval.1	$$⊢\phi \to W\in V$$
	sitmval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	sitmfval.1	$$⊢\phi \to F\in {\Im }_M^W$$
	sitmfval.2	$$⊢\phi \to G\in {\Im }_M^W$$
Assertion	sitmfval	$$⊢\phi \to {|G-F|}_M^W={\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(F{D}_{f}G\right)dM$$

Proof

Step	Hyp	Ref	Expression
1		sitmval.d	$$⊢D=\mathrm{dist}\left(W\right)$$
2		sitmval.1	$$⊢\phi \to W\in V$$
3		sitmval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
4		sitmfval.1	$$⊢\phi \to F\in {\Im }_M^W$$
5		sitmfval.2	$$⊢\phi \to G\in {\Im }_M^W$$
6	1 2 3	sitmval	$$⊢\phi \to W\mathrm{sitm}M=\left(f\in {\Im }_M^W,g\in {\Im }_M^W⟼{\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(f{D}_{f}g\right)dM\right)$$
7		simprl	$$⊢\left(\phi \wedge \left(f=F\wedge g=G\right)\right)\to f=F$$
8		simprr	$$⊢\left(\phi \wedge \left(f=F\wedge g=G\right)\right)\to g=G$$
9	7 8	oveq12d	$$⊢\left(\phi \wedge \left(f=F\wedge g=G\right)\right)\to f{D}_{f}g=F{D}_{f}G$$
10	9	fveq2d	$$⊢\left(\phi \wedge \left(f=F\wedge g=G\right)\right)\to {\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(f{D}_{f}g\right)dM={\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(F{D}_{f}G\right)dM$$
11		fvexd	$$⊢\phi \to {\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(F{D}_{f}G\right)dM\in \mathrm{V}$$
12	6 10 4 5 11	ovmpod	$$⊢\phi \to {|G-F|}_M^W={\int }_{\Im }^{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}\left(F{D}_{f}G\right)dM$$