# Metamath Proof Explorer

## Theorem fvvolioof

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

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