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

Metamath Proof Explorer

Theorem ovolfs2

Description: Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis ovolfs2.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
Assertion ovolfs2 ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( ( vol* ∘ (,) ) ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ovolfs2.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
3 ovolioo ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
4 2 3 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
5 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
7 5 6 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
8 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
9 7 8 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ* × ℝ* ) )
10 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ* × ℝ* ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
11 9 10 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
12 11 fveq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
13 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
14 12 13 eqtr4di ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
15 14 fveq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
16 1 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
17 4 15 16 3eqtr4rd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
18 17 mpteq2dva ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝐺 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
19 1 ovolfsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )
20 19 feqmptd ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝐺 ‘ 𝑛 ) ) )
21 id ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
22 21 feqmptd ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) )
23 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
24 23 a1i ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ )
25 24 ffvelcdmda ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ℝ* × ℝ* ) ) → ( (,) ‘ 𝑥 ) ∈ 𝒫 ℝ )
26 24 feqmptd ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → (,) = ( 𝑥 ∈ ( ℝ* × ℝ* ) ↦ ( (,) ‘ 𝑥 ) ) )
27 ovolf ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
28 27 a1i ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) )
29 28 feqmptd ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → vol* = ( 𝑦 ∈ 𝒫 ℝ ↦ ( vol* ‘ 𝑦 ) ) )
30 fveq2 ⊢ ( 𝑦 = ( (,) ‘ 𝑥 ) → ( vol* ‘ 𝑦 ) = ( vol* ‘ ( (,) ‘ 𝑥 ) ) )
31 25 26 29 30 fmptco ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( vol* ∘ (,) ) = ( 𝑥 ∈ ( ℝ* × ℝ* ) ↦ ( vol* ‘ ( (,) ‘ 𝑥 ) ) ) )
32 2fveq3 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( vol* ‘ ( (,) ‘ 𝑥 ) ) = ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
33 9 22 31 32 fmptco ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( vol* ∘ (,) ) ∘ 𝐹 ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
34 18 20 33 3eqtr4d ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( ( vol* ∘ (,) ) ∘ 𝐹 ) )