Theorem volioofmpt

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

	Ref	Expression
Hypotheses	volioofmpt.x	$$⊢\underset{\_}{Ⅎ}xF$$
	volioofmpt.f	$$⊢\phi \to F:A⟶{ℝ}^{*}\times {ℝ}^{*}$$
Assertion	volioofmpt	$$⊢\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		volioofmpt.x	$$⊢\underset{\_}{Ⅎ}xF$$
2		volioofmpt.f	$$⊢\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		volioof	$$⊢\left(vol\circ \left(.\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]$$
7	6	a1i	$$⊢\phi \to \left(vol\circ \left(.\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]$$
8		fco	$$⊢\left(\left(vol\circ \left(.\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]\wedge F:A⟶{ℝ}^{*}\times {ℝ}^{*}\right)\to \left(\left(vol\circ \left(.\right)\right)\circ F\right):A⟶\left[0,\mathrm{+\infty }\right]$$
9	7 2 8	syl2anc	$$⊢\phi \to \left(\left(vol\circ \left(.\right)\right)\circ F\right):A⟶\left[0,\mathrm{+\infty }\right]$$
10	3 5 9	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)$$
11	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to F:A⟶{ℝ}^{*}\times {ℝ}^{*}$$
12		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
13	11 12	fvvolioof	$$⊢\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)$$
14	13	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)$$
15	10 14	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)$$