# Metamath Proof Explorer

## Theorem fvvolicof

Description: The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses fvvolicof.f ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}$
fvvolicof.x ${⊢}{\phi }\to {X}\in {A}$
Assertion fvvolicof ${⊢}{\phi }\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)$

### Proof

Step Hyp Ref Expression
1 fvvolicof.f ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{*}×{ℝ}^{*}$
2 fvvolicof.x ${⊢}{\phi }\to {X}\in {A}$
3 1 ffund ${⊢}{\phi }\to \mathrm{Fun}{F}$
4 1 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
5 4 eqcomd ${⊢}{\phi }\to {A}=\mathrm{dom}{F}$
6 2 5 eleqtrd ${⊢}{\phi }\to {X}\in \mathrm{dom}{F}$
7 fvco ${⊢}\left(\mathrm{Fun}{F}\wedge {X}\in \mathrm{dom}{F}\right)\to \left(\left(vol\circ \left[.\right)\right)\circ {F}\right)\left({X}\right)=\left(vol\circ \left[.\right)\right)\left({F}\left({X}\right)\right)$
8 3 6 7 syl2anc ${⊢}{\phi }\to \left(\left(vol\circ \left[.\right)\right)\circ {F}\right)\left({X}\right)=\left(vol\circ \left[.\right)\right)\left({F}\left({X}\right)\right)$
9 icof ${⊢}\left[.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
10 ffun ${⊢}\left[.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}\to \mathrm{Fun}\left[.\right)$
11 9 10 ax-mp ${⊢}\mathrm{Fun}\left[.\right)$
12 11 a1i ${⊢}{\phi }\to \mathrm{Fun}\left[.\right)$
13 1 2 ffvelrnd ${⊢}{\phi }\to {F}\left({X}\right)\in \left({ℝ}^{*}×{ℝ}^{*}\right)$
14 9 fdmi ${⊢}\mathrm{dom}\left[.\right)={ℝ}^{*}×{ℝ}^{*}$
15 13 14 eleqtrrdi ${⊢}{\phi }\to {F}\left({X}\right)\in \mathrm{dom}\left[.\right)$
16 fvco ${⊢}\left(\mathrm{Fun}\left[.\right)\wedge {F}\left({X}\right)\in \mathrm{dom}\left[.\right)\right)\to \left(vol\circ \left[.\right)\right)\left({F}\left({X}\right)\right)=vol\left(\left[.\right)\left({F}\left({X}\right)\right)\right)$
17 12 15 16 syl2anc ${⊢}{\phi }\to \left(vol\circ \left[.\right)\right)\left({F}\left({X}\right)\right)=vol\left(\left[.\right)\left({F}\left({X}\right)\right)\right)$
18 df-ov ${⊢}\left[{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)\right)=\left[.\right)\left(⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩\right)$
19 18 a1i ${⊢}{\phi }\to \left[{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)\right)=\left[.\right)\left(⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩\right)$
20 1st2nd2 ${⊢}{F}\left({X}\right)\in \left({ℝ}^{*}×{ℝ}^{*}\right)\to {F}\left({X}\right)=⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩$
21 13 20 syl ${⊢}{\phi }\to {F}\left({X}\right)=⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩$
22 21 eqcomd ${⊢}{\phi }\to ⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩={F}\left({X}\right)$
23 22 fveq2d ${⊢}{\phi }\to \left[.\right)\left(⟨{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)⟩\right)=\left[.\right)\left({F}\left({X}\right)\right)$
24 19 23 eqtr2d ${⊢}{\phi }\to \left[.\right)\left({F}\left({X}\right)\right)=\left[{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)\right)$
25 24 fveq2d ${⊢}{\phi }\to vol\left(\left[.\right)\left({F}\left({X}\right)\right)\right)=vol\left(\left[{1}^{st}\left({F}\left({X}\right)\right),{2}^{nd}\left({F}\left({X}\right)\right)\right)\right)$
26 8 17 25 3eqtrd ${⊢}{\phi }\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)$