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

Metamath Proof Explorer

Theorem ovolfsval

Description: The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis ovolfs.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
Assertion ovolfsval ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolfs.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2 1 fveq1i ⊢ ( 𝐺 ‘ 𝑁 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑁 )
3 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑁 ) = ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) )
4 2 3 eqtrid ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) )
5 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
6 5 elin2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) )
7 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
8 6 7 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
9 8 fveq2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ) )
10 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
11 9 10 eqtr4di ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
12 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
13 12 simp1d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
15 12 simp2d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
17 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
18 17 cnmetdval ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
19 14 16 18 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
20 abssuble0 ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) → ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
21 12 20 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( abs ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
22 19 21 eqtrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
23 11 22 eqtrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
24 4 23 eqtrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )