This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ × ℝ ) )
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 ∘ [,) ) ∘ 𝐹 ) )