voliooicof

Description: The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypothesis	voliooicof.1	$⊢ φ \to F : A ⟶ ℝ^{2}$
	Assertion	voliooicof	$⊢ φ \to (vol \circ (.)) \circ F = (vol \circ [.)) \circ F$

Proof

Step	Hyp	Ref	Expression
1		voliooicof.1	$⊢ φ \to F : A ⟶ ℝ^{2}$
2		volioof	$⊢ (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
3	2	a1i	$⊢ φ \to (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
4		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
5	4	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
6	3 5 1	fcoss	$⊢ φ \to ((vol \circ (.)) \circ F) : A ⟶ [0, +∞]$
7	6	ffnd	$⊢ φ \to ((vol \circ (.)) \circ F) Fn A$
8		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
9	8	a1i	$⊢ φ \to vol : dom vol ⟶ [0, +∞]$
10		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
11	10	a1i	$⊢ φ \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
12	11 5 1	fcoss	$⊢ φ \to ([.) \circ F) : A ⟶ 𝒫 ℝ^{*}$
13	12	ffnd	$⊢ φ \to ([.) \circ F) Fn A$
14	1	adantr	$⊢ (φ \land x \in A) \to F : A ⟶ ℝ^{2}$
15		simpr	$⊢ (φ \land x \in A) \to x \in A$
16	14 15	fvovco	$⊢ (φ \land x \in A) \to ([.) \circ F) (x) = [1^{st} (F (x)), 2^{nd} (F (x)))$
17	1	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in ℝ^{2}$
18		xp1st	$⊢ F (x) \in ℝ^{2} \to 1^{st} (F (x)) \in ℝ$
19	17 18	syl	$⊢ (φ \land x \in A) \to 1^{st} (F (x)) \in ℝ$
20		xp2nd	$⊢ F (x) \in ℝ^{2} \to 2^{nd} (F (x)) \in ℝ$
21	17 20	syl	$⊢ (φ \land x \in A) \to 2^{nd} (F (x)) \in ℝ$
22	21	rexrd	$⊢ (φ \land x \in A) \to 2^{nd} (F (x)) \in ℝ^{*}$
23		icombl	$⊢ (1^{st} (F (x)) \in ℝ \land 2^{nd} (F (x)) \in ℝ^{*}) \to [1^{st} (F (x)), 2^{nd} (F (x))) \in dom vol$
24	19 22 23	syl2anc	$⊢ (φ \land x \in A) \to [1^{st} (F (x)), 2^{nd} (F (x))) \in dom vol$
25	16 24	eqeltrd	$⊢ (φ \land x \in A) \to ([.) \circ F) (x) \in dom vol$
26	25	ralrimiva	$⊢ φ \to \forall x \in A ([.) \circ F) (x) \in dom vol$
27	13 26	jca	$⊢ φ \to (([.) \circ F) Fn A \land \forall x \in A ([.) \circ F) (x) \in dom vol)$
28		ffnfv	$⊢ ([.) \circ F) : A ⟶ dom vol \leftrightarrow (([.) \circ F) Fn A \land \forall x \in A ([.) \circ F) (x) \in dom vol)$
29	27 28	sylibr	$⊢ φ \to ([.) \circ F) : A ⟶ dom vol$
30		fco	$⊢ (vol : dom vol ⟶ [0, +∞] \land ([.) \circ F) : A ⟶ dom vol) \to (vol \circ ([.) \circ F)) : A ⟶ [0, +∞]$
31	9 29 30	syl2anc	$⊢ φ \to (vol \circ ([.) \circ F)) : A ⟶ [0, +∞]$
32		coass	$⊢ (vol \circ [.)) \circ F = vol \circ ([.) \circ F)$
33	32	a1i	$⊢ φ \to (vol \circ [.)) \circ F = vol \circ ([.) \circ F)$
34	33	feq1d	$⊢ φ \to (((vol \circ [.)) \circ F) : A ⟶ [0, +∞] \leftrightarrow (vol \circ ([.) \circ F)) : A ⟶ [0, +∞])$
35	31 34	mpbird	$⊢ φ \to ((vol \circ [.)) \circ F) : A ⟶ [0, +∞]$
36	35	ffnd	$⊢ φ \to ((vol \circ [.)) \circ F) Fn A$
37	19 21	voliooico	$⊢ (φ \land x \in A) \to vol ((1^{st} (F (x)), 2^{nd} (F (x)))) = vol ([1^{st} (F (x)), 2^{nd} (F (x))))$
38	1 5	fssd	$⊢ φ \to F : A ⟶ ℝ^{} \times ℝ^{}$
39	38	adantr	$⊢ (φ \land x \in A) \to F : A ⟶ ℝ^{} \times ℝ^{}$
40	39 15	fvvolioof	$⊢ (φ \land x \in A) \to ((vol \circ (.)) \circ F) (x) = vol ((1^{st} (F (x)), 2^{nd} (F (x))))$
41	39 15	fvvolicof	$⊢ (φ \land x \in A) \to ((vol \circ [.)) \circ F) (x) = vol ([1^{st} (F (x)), 2^{nd} (F (x))))$
42	37 40 41	3eqtr4d	$⊢ (φ \land x \in A) \to ((vol \circ (.)) \circ F) (x) = ((vol \circ [.)) \circ F) (x)$
43	7 36 42	eqfnfvd	$⊢ φ \to (vol \circ (.)) \circ F = (vol \circ [.)) \circ F$

Metamath Proof Explorer

Theorem voliooicof

Proof