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 ffvelrn ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
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 ffvelrnda ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ℝ* × ℝ* ) ) → ( (,) ‘ 𝑥 ) ∈ 𝒫 ℝ )
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* ∘ (,) ) ∘ 𝐹 ) )