Theorem 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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ ) )
Assertion	voliooicof	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) = ( ( vol ∘ [,) ) ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		voliooicof.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ ) )
2		volioof	⊢ ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ )
3	2	a1i	⊢ ( 𝜑 → ( vol ∘ (,) ) : ( ℝ* × ℝ* ) ⟶ ( 0 [,] +∞ ) )
4		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
5	4	a1i	⊢ ( 𝜑 → ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) )
6	3 5 1	fcoss	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
7	6	ffnd	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) Fn 𝐴 )
8		volf	⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
9	8	a1i	⊢ ( 𝜑 → vol : dom vol ⟶ ( 0 [,] +∞ ) )
10		icof	⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
11	10	a1i	⊢ ( 𝜑 → [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
12	11 5 1	fcoss	⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : 𝐴 ⟶ 𝒫 ℝ* )
13	12	ffnd	⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) Fn 𝐴 )
14	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ( ℝ × ℝ ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
16	14 15	fvovco	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
17	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) )
18		xp1st	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
20		xp2nd	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
21	17 20	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
22	21	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* )
23		icombl	⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol )
24	19 22 23	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ dom vol )
25	16 24	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
26	25	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol )
27	13 26	jca	⊢ ( 𝜑 → ( ( [,) ∘ 𝐹 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ) )
28		ffnfv	⊢ ( ( [,) ∘ 𝐹 ) : 𝐴 ⟶ dom vol ↔ ( ( [,) ∘ 𝐹 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( [,) ∘ 𝐹 ) ‘ 𝑥 ) ∈ dom vol ) )
29	27 28	sylibr	⊢ ( 𝜑 → ( [,) ∘ 𝐹 ) : 𝐴 ⟶ dom vol )
30		fco	⊢ ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ ( [,) ∘ 𝐹 ) : 𝐴 ⟶ dom vol ) → ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
31	9 29 30	syl2anc	⊢ ( 𝜑 → ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
32		coass	⊢ ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( vol ∘ ( [,) ∘ 𝐹 ) )
33	32	a1i	⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) = ( vol ∘ ( [,) ∘ 𝐹 ) ) )
34	33	feq1d	⊢ ( 𝜑 → ( ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ↔ ( vol ∘ ( [,) ∘ 𝐹 ) ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) )
35	31 34	mpbird	⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
36	35	ffnd	⊢ ( 𝜑 → ( ( vol ∘ [,) ) ∘ 𝐹 ) Fn 𝐴 )
37	19 21	voliooico	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
38	1 5	fssd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ( ℝ* × ℝ* ) )
40	39 15	fvvolioof	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
41	39 15	fvvolicof	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( vol ∘ [,) ) ∘ 𝐹 ) ‘ 𝑥 ) = ( vol ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) [,) ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
42	37 40 41	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( vol ∘ (,) ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( ( vol ∘ [,) ) ∘ 𝐹 ) ‘ 𝑥 ) )
43	7 36 42	eqfnfvd	⊢ ( 𝜑 → ( ( vol ∘ (,) ) ∘ 𝐹 ) = ( ( vol ∘ [,) ) ∘ 𝐹 ) )