# Metamath Proof Explorer

## Theorem volicoff

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

Ref Expression
Hypothesis volicoff.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ×{ℝ}^{*}$
Assertion volicoff ${⊢}{\phi }\to \left(\left(vol\circ \left[.\right)\right)\circ {F}\right):{A}⟶\left[0,\mathrm{+\infty }\right]$

### Proof

Step Hyp Ref Expression
1 volicoff.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ×{ℝ}^{*}$
2 volf ${⊢}vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$
3 2 a1i ${⊢}{\phi }\to vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$
4 icof ${⊢}\left[.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
5 4 a1i ${⊢}{\phi }\to \left[.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
6 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
7 xpss1 ${⊢}ℝ\subseteq {ℝ}^{*}\to ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
8 6 7 ax-mp ${⊢}ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
9 8 a1i ${⊢}{\phi }\to ℝ×{ℝ}^{*}\subseteq {ℝ}^{*}×{ℝ}^{*}$
10 5 9 1 fcoss ${⊢}{\phi }\to \left(\left[.\right)\circ {F}\right):{A}⟶𝒫{ℝ}^{*}$
11 10 ffnd ${⊢}{\phi }\to \left(\left[.\right)\circ {F}\right)Fn{A}$
12 1 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}:{A}⟶ℝ×{ℝ}^{*}$
13 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
14 12 13 fvovco ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left[.\right)\circ {F}\right)\left({x}\right)=\left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)$
15 1 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in \left(ℝ×{ℝ}^{*}\right)$
16 xp1st ${⊢}{F}\left({x}\right)\in \left(ℝ×{ℝ}^{*}\right)\to {1}^{st}\left({F}\left({x}\right)\right)\in ℝ$
17 15 16 syl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {1}^{st}\left({F}\left({x}\right)\right)\in ℝ$
18 xp2nd ${⊢}{F}\left({x}\right)\in \left(ℝ×{ℝ}^{*}\right)\to {2}^{nd}\left({F}\left({x}\right)\right)\in {ℝ}^{*}$
19 15 18 syl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {2}^{nd}\left({F}\left({x}\right)\right)\in {ℝ}^{*}$
20 icombl ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in {ℝ}^{*}\right)\to \left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\in \mathrm{dom}vol$
21 17 19 20 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\in \mathrm{dom}vol$
22 14 21 eqeltrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left[.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
23 22 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left[.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
24 fnfvrnss ${⊢}\left(\left(\left[.\right)\circ {F}\right)Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left[.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\right)\to \mathrm{ran}\left(\left[.\right)\circ {F}\right)\subseteq \mathrm{dom}vol$
25 11 23 24 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left(\left[.\right)\circ {F}\right)\subseteq \mathrm{dom}vol$
26 ffrn ${⊢}\left(\left[.\right)\circ {F}\right):{A}⟶𝒫{ℝ}^{*}\to \left(\left[.\right)\circ {F}\right):{A}⟶\mathrm{ran}\left(\left[.\right)\circ {F}\right)$
27 10 26 syl ${⊢}{\phi }\to \left(\left[.\right)\circ {F}\right):{A}⟶\mathrm{ran}\left(\left[.\right)\circ {F}\right)$
28 3 25 27 fcoss ${⊢}{\phi }\to \left(vol\circ \left(\left[.\right)\circ {F}\right)\right):{A}⟶\left[0,\mathrm{+\infty }\right]$
29 coass ${⊢}\left(vol\circ \left[.\right)\right)\circ {F}=vol\circ \left(\left[.\right)\circ {F}\right)$
30 29 feq1i ${⊢}\left(\left(vol\circ \left[.\right)\right)\circ {F}\right):{A}⟶\left[0,\mathrm{+\infty }\right]↔\left(vol\circ \left(\left[.\right)\circ {F}\right)\right):{A}⟶\left[0,\mathrm{+\infty }\right]$
31 30 a1i ${⊢}{\phi }\to \left(\left(\left(vol\circ \left[.\right)\right)\circ {F}\right):{A}⟶\left[0,\mathrm{+\infty }\right]↔\left(vol\circ \left(\left[.\right)\circ {F}\right)\right):{A}⟶\left[0,\mathrm{+\infty }\right]\right)$
32 28 31 mpbird ${⊢}{\phi }\to \left(\left(vol\circ \left[.\right)\right)\circ {F}\right):{A}⟶\left[0,\mathrm{+\infty }\right]$