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 ‘ 𝐷 ) 𝑅 ) )