# Metamath Proof Explorer

## 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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
volioofmpt.f ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}$
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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 volioofmpt.f ${⊢}{\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 volioof ${⊢}\left(vol\circ \left(.\right)\right):{ℝ}^{*}×{ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]$
7 6 a1i ${⊢}{\phi }\to \left(vol\circ \left(.\right)\right):{ℝ}^{*}×{ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]$
8 fco ${⊢}\left(\left(vol\circ \left(.\right)\right):{ℝ}^{*}×{ℝ}^{*}⟶\left[0,\mathrm{+\infty }\right]\wedge {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}\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}⟶{ℝ}^{*}×{ℝ}^{*}$
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)$