Theorem sitgfval

Description: Value of the Bochner integral for a simple function F . (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitgval.b	$$⊢B={\mathrm{Base}}_W$$
	sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	sitgval.s	$$⊢S=𝛔\left(J\right)$$
	sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
	sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
	sitgval.1	$$⊢\phi \to W\in V$$
	sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
Assertion	sitgfval	$$⊢\phi \to {\int }_{\Im }^{W}FdM=\underset{x\in \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$$⊢B={\mathrm{Base}}_W$$
2		sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		sitgval.s	$$⊢S=𝛔\left(J\right)$$
4		sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
7		sitgval.1	$$⊢\phi \to W\in V$$
8		sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
9		sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
10	1 2 3 4 5 6 7 8	sitgval	$$⊢\phi \to W\mathrm{sitg}M=\left(f\in \left\{g\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)|\left(\mathrm{ran}g\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right\}⟼\underset{x\in \mathrm{ran}f\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(f^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)\right)$$
11		simpr	$$⊢\left(\phi \wedge f=F\right)\to f=F$$
12	11	rneqd	$$⊢\left(\phi \wedge f=F\right)\to \mathrm{ran}f=\mathrm{ran}F$$
13	12	difeq1d	$$⊢\left(\phi \wedge f=F\right)\to \mathrm{ran}f\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}$$
14	11	cnveqd	$$⊢\left(\phi \wedge f=F\right)\to f^{-1}=F^{-1}$$
15	14	imaeq1d	$$⊢\left(\phi \wedge f=F\right)\to f^{-1}\left[\left\{x\right\}\right]=F^{-1}\left[\left\{x\right\}\right]$$
16	15	fveq2d	$$⊢\left(\phi \wedge f=F\right)\to M\left(f^{-1}\left[\left\{x\right\}\right]\right)=M\left(F^{-1}\left[\left\{x\right\}\right]\right)$$
17	16	fveq2d	$$⊢\left(\phi \wedge f=F\right)\to H\left(M\left(f^{-1}\left[\left\{x\right\}\right]\right)\right)=H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)$$
18	17	oveq1d	$$⊢\left(\phi \wedge f=F\right)\to H\left(M\left(f^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x=H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x$$
19	13 18	mpteq12dv	$$⊢\left(\phi \wedge f=F\right)\to \left(x\in \left(\mathrm{ran}f\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼H\left(M\left(f^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\left(x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$
20	19	oveq2d	$$⊢\left(\phi \wedge f=F\right)\to \underset{x\in \mathrm{ran}f\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(f^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)=\underset{x\in \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$
21	1 2 3 4 5 6 7 8 9	sibfmbl	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)$$
22	1 2 3 4 5 6 7 8 9	sibfrn	$$⊢\phi \to \mathrm{ran}F\in \mathrm{Fin}$$
23	1 2 3 4 5 6 7 8 9	sibfima	$$⊢\left(\phi \wedge x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
24	23	ralrimiva	$$⊢\phi \to \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)$$
25	21 22 24	jca32	$$⊢\phi \to \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \left(\mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
26		rneq	$$⊢g=F\to \mathrm{ran}g=\mathrm{ran}F$$
27	26	eleq1d	$$⊢g=F\to \left(\mathrm{ran}g\in \mathrm{Fin}\leftrightarrow \mathrm{ran}F\in \mathrm{Fin}\right)$$
28	26	difeq1d	$$⊢g=F\to \mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}$$
29		cnveq	$$⊢g=F\to g^{-1}=F^{-1}$$
30	29	imaeq1d	$$⊢g=F\to g^{-1}\left[\left\{x\right\}\right]=F^{-1}\left[\left\{x\right\}\right]$$
31	30	fveq2d	$$⊢g=F\to M\left(g^{-1}\left[\left\{x\right\}\right]\right)=M\left(F^{-1}\left[\left\{x\right\}\right]\right)$$
32	31	eleq1d	$$⊢g=F\to \left(M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
33	28 32	raleqbidv	$$⊢g=F\to \left(\forall x\in \left(\mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
34	27 33	anbi12d	$$⊢g=F\to \left(\left(\mathrm{ran}g\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\leftrightarrow \left(\mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
35	34	elrab	$$⊢F\in \left\{g\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)|\left(\mathrm{ran}g\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right\}\leftrightarrow \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \left(\mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
36	25 35	sylibr	$$⊢\phi \to F\in \left\{g\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)|\left(\mathrm{ran}g\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}g\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(g^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right\}$$
37		ovexd	$$⊢\phi \to \underset{x\in \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)\in \mathrm{V}$$
38	10 20 36 37	fvmptd	$$⊢\phi \to {\int }_{\Im }^{W}FdM=\underset{x\in \mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}}{{\sum }_W}\left(H\left(M\left(F^{-1}\left[\left\{x\right\}\right]\right)\right)\underset{\dot{}}{·}x\right)$$