This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
fvvolioof.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion fvvolioof ( 𝜑 → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑋 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fvvolioof.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
2 fvvolioof.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3 1 ffund ⊢ ( 𝜑 → Fun 𝐹 )
4 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5 4 eqcomd ⊢ ( 𝜑 → 𝐴 = dom 𝐹 )
6 2 5 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ dom 𝐹 )
7 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑋 ) = ( ( vol ∘ (,) ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
8 3 6 7 syl2anc ⊢ ( 𝜑 → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑋 ) = ( ( vol ∘ (,) ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
9 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
10 ffun ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
11 9 10 ax-mp ⊢ Fun (,)
12 11 a1i ⊢ ( 𝜑 → Fun (,) )
13 1 2 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ℝ* × ℝ* ) )
14 9 fdmi ⊢ dom (,) = ( ℝ* × ℝ* )
15 13 14 eleqtrrdi ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ dom (,) )
16 fvco ⊢ ( ( Fun (,) ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom (,) ) → ( ( vol ∘ (,) ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( vol ‘ ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
17 12 15 16 syl2anc ⊢ ( 𝜑 → ( ( vol ∘ (,) ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( vol ‘ ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
18 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
19 18 a1i ⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ) )
20 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( ℝ* × ℝ* ) → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
21 13 20 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
22 21 eqcomd ⊢ ( 𝜑 → ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ = ( 𝐹 ‘ 𝑋 ) )
23 22 fveq2d ⊢ ( 𝜑 → ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ) = ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) )
24 19 23 eqtr2d ⊢ ( 𝜑 → ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
26 8 17 25 3eqtrd ⊢ ( 𝜑 → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑋 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )