Theorem volicofmpt

Description: ( ( vol o. [,) ) o. F ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	volicofmpt.1	$$⊢\underset{\_}{Ⅎ}xF$$
	volicofmpt.2	$$⊢\phi \to F:A⟶ℝ\times {ℝ}^{*}$$
Assertion	volicofmpt	$$⊢\phi \to \left(vol\circ \left[.\right)\right)\circ F=\left(x\in A⟼vol\left(\left[1^{st}\left(F\left(x\right)\right),2^{nd}\left(F\left(x\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		volicofmpt.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		volicofmpt.2	$$⊢\phi \to F:A⟶ℝ\times {ℝ}^{*}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(vol\circ \left[.\right)\right)$$
5	4 1	nfco	$$⊢\underset{\_}{Ⅎ}x\left(\left(vol\circ \left[.\right)\right)\circ F\right)$$
6	2	volicoff	$$⊢\phi \to \left(\left(vol\circ \left[.\right)\right)\circ F\right):A⟶\left[0,\mathrm{+\infty }\right]$$
7	3 5 6	feqmptdf	$$⊢\phi \to \left(vol\circ \left[.\right)\right)\circ F=\left(x\in A⟼\left(\left(vol\circ \left[.\right)\right)\circ F\right)\left(x\right)\right)$$
8		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
9		xpss1	$$⊢ℝ\subseteq {ℝ}^{*}\to ℝ\times {ℝ}^{*}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
10	8 9	ax-mp	$$⊢ℝ\times {ℝ}^{*}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
11	10	a1i	$$⊢\phi \to ℝ\times {ℝ}^{*}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
12	2 11	fssd	$$⊢\phi \to F:A⟶{ℝ}^{*}\times {ℝ}^{*}$$
13	12	adantr	$$⊢\left(\phi \wedge x\in A\right)\to F:A⟶{ℝ}^{*}\times {ℝ}^{*}$$
14		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
15	13 14	fvvolicof	$$⊢\left(\phi \wedge x\in A\right)\to \left(\left(vol\circ \left[.\right)\right)\circ F\right)\left(x\right)=vol\left(\left[1^{st}\left(F\left(x\right)\right),2^{nd}\left(F\left(x\right)\right)\right)\right)$$
16	15	mpteq2dva	$$⊢\phi \to \left(x\in A⟼\left(\left(vol\circ \left[.\right)\right)\circ F\right)\left(x\right)\right)=\left(x\in A⟼vol\left(\left[1^{st}\left(F\left(x\right)\right),2^{nd}\left(F\left(x\right)\right)\right)\right)\right)$$
17	7 16	eqtrd	$$⊢\phi \to \left(vol\circ \left[.\right)\right)\circ F=\left(x\in A⟼vol\left(\left[1^{st}\left(F\left(x\right)\right),2^{nd}\left(F\left(x\right)\right)\right)\right)\right)$$