# Metamath Proof Explorer

## 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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
volicofmpt.2 ${⊢}{\phi }\to {F}:{A}⟶ℝ×{ℝ}^{*}$
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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 volicofmpt.2 ${⊢}{\phi }\to {F}:{A}⟶ℝ×{ℝ}^{*}$
3 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(vol\circ \left[.\right)\right)$
5 4 1 nfco ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\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 ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
10 8 9 ax-mp ${⊢}ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
11 10 a1i ${⊢}{\phi }\to ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
12 2 11 fssd ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}$
13 12 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}$
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)$