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

Proof

Step	Hyp	Ref	Expression
1		fvvolioof.f	$⊢ φ \to F : A ⟶ ℝ^{} \times ℝ^{}$
2		fvvolioof.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		ioof	$⊢ (.) : ℝ^{} \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 fvvolioof

Proof