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

Proof

Step	Hyp	Ref	Expression
1		fvvolicof.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ^* × ℝ^* ) )
2		fvvolicof.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		icof	⊢ [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*
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	⊢ ( ( 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 fvvolicof

Proof