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	$⊢ φ \to F : A ⟶ ℝ^{} \times ℝ^{}$
	fvvolicof.x	$⊢ φ \to X \in A$
Assertion	fvvolicof	$⊢ φ \to ((vol \circ [.)) \circ F) (X) = vol ([1^{st} (F (X)), 2^{nd} (F (X))))$

Proof

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

Metamath Proof Explorer

Theorem fvvolicof

Proof