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

Metamath Proof Explorer

Theorem ovolfsf

Description: Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis ovolfs.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
Assertion ovolfsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )

Proof

Step Hyp Ref Expression
1 ovolfs.1 ⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2 absf ⊢ abs : ℂ ⟶ ℝ
3 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
4 fco ⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
5 2 3 4 mp2an ⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
6 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
7 ax-resscn ⊢ ℝ ⊆ ℂ
8 xpss12 ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
9 7 7 8 mp2an ⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
10 6 9 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℂ × ℂ )
11 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℂ × ℂ ) ) → 𝐹 : ℕ ⟶ ( ℂ × ℂ ) )
12 10 11 mpan2 ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℂ × ℂ ) )
13 fco ⊢ ( ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ ∧ 𝐹 : ℕ ⟶ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
14 5 12 13 sylancr ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
15 1 feq1i ⊢ ( 𝐺 : ℕ ⟶ ℝ ↔ ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
16 14 15 sylibr ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ℝ )
17 16 ffnd ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 Fn ℕ )
18 16 ffvelcdmda ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
19 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
20 subge0 ⊢ ( ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
21 20 ancoms ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
22 21 biimp3ar ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 0 ≤ ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
23 19 22 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
24 1 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
25 23 24 breqtrrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ ( 𝐺 ‘ 𝑥 ) )
26 elrege0 ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐺 ‘ 𝑥 ) ) )
27 18 25 26 sylanbrc ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
28 27 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑥 ∈ ℕ ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
29 ffnfv ⊢ ( 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐺 Fn ℕ ∧ ∀ 𝑥 ∈ ℕ ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
30 17 28 29 sylanbrc ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )