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

Metamath Proof Explorer

Theorem cnbl0

Description: Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis cnblcld.1 ⊢ 𝐷 = ( abs ∘ − )
Assertion cnbl0 ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ 𝐷 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cnblcld.1 ⊢ 𝐷 = ( abs ∘ − )
2 df-3an ⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) ↔ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) )
3 abscl ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ )
4 absge0 ⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( abs ‘ 𝑥 ) )
5 3 4 jca ⊢ ( 𝑥 ∈ ℂ → ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) )
6 5 adantl ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) )
7 6 biantrurd ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) < 𝑅 ↔ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) ) )
8 2 7 bitr4id ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) ↔ ( abs ‘ 𝑥 ) < 𝑅 ) )
9 0re ⊢ 0 ∈ ℝ
10 simpl ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → 𝑅 ∈ ℝ* )
11 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) ) )
12 9 10 11 sylancr ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) < 𝑅 ) ) )
13 0cn ⊢ 0 ∈ ℂ
14 1 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 0 − 𝑥 ) ) )
15 abssub ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) )
16 14 15 eqtrd ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
17 13 16 mpan ⊢ ( 𝑥 ∈ ℂ → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
18 subid1 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
19 18 fveq2d ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ 𝑥 ) )
20 17 19 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 0 𝐷 𝑥 ) = ( abs ‘ 𝑥 ) )
21 20 adantl ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ 𝑥 ) )
22 21 breq1d ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( 0 𝐷 𝑥 ) < 𝑅 ↔ ( abs ‘ 𝑥 ) < 𝑅 ) )
23 8 12 22 3bitr4d ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( 0 𝐷 𝑥 ) < 𝑅 ) )
24 23 pm5.32da ⊢ ( 𝑅 ∈ ℝ* → ( ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) < 𝑅 ) ) )
25 absf ⊢ abs : ℂ ⟶ ℝ
26 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
27 25 26 ax-mp ⊢ abs Fn ℂ
28 elpreima ⊢ ( abs Fn ℂ → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ) ) )
29 27 28 mp1i ⊢ ( 𝑅 ∈ ℝ* → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,) 𝑅 ) ) ) )
30 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
31 1 30 eqeltri ⊢ 𝐷 ∈ ( ∞Met ‘ ℂ )
32 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 0 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) < 𝑅 ) ) )
33 31 13 32 mp3an12 ⊢ ( 𝑅 ∈ ℝ* → ( 𝑥 ∈ ( 0 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) < 𝑅 ) ) )
34 24 29 33 3bitr4d ⊢ ( 𝑅 ∈ ℝ* → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ 𝑥 ∈ ( 0 ( ball ‘ 𝐷 ) 𝑅 ) ) )
35 34 eqrdv ⊢ ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ 𝐷 ) 𝑅 ) )