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 ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )

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	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ℝ^* × ℝ^* ) )
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	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
19	18	a1i	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ) )
20		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( ℝ^* × ℝ^* ) → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
21	13 20	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ )
22	21	eqcomd	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ = ( 𝐹 ‘ 𝑋 ) )
23	22	fveq2d	⊢ ( 𝜑 → ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ) = ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) )
24	19 23	eqtr2d	⊢ ( 𝜑 → ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
25	24	fveq2d	⊢ ( 𝜑 → ( vol ‘ ( (,) ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
26	8 17 25	3eqtrd	⊢ ( 𝜑 → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑋 ) = ( vol ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )

Metamath Proof Explorer

Theorem fvvolioof

Proof