Metamath Proof Explorer

Theorem imasf1obl

Description: The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses imasf1obl.u ⊢ φ → U = F “ 𝑠 R
imasf1obl.v ⊢ φ → V = Base R
imasf1obl.f ⊢ φ → F : V ⟶ 1-1 onto B
imasf1obl.r ⊢ φ → R ∈ Z
imasf1obl.e ⊢ E = dist ⁡ R ↾ V × V
imasf1obl.d ⊢ D = dist ⁡ U
imasf1obl.m ⊢ φ → E ∈ ∞Met ⁡ V
imasf1obl.x ⊢ φ → P ∈ V
imasf1obl.s ⊢ φ → S ∈ ℝ *
Assertion imasf1obl ⊢ φ → F ⁡ P ball ⁡ D S = F P ball ⁡ E S

Proof

Step Hyp Ref Expression
1 imasf1obl.u ⊢ φ → U = F “ 𝑠 R
2 imasf1obl.v ⊢ φ → V = Base R
3 imasf1obl.f ⊢ φ → F : V ⟶ 1-1 onto B
4 imasf1obl.r ⊢ φ → R ∈ Z
5 imasf1obl.e ⊢ E = dist ⁡ R ↾ V × V
6 imasf1obl.d ⊢ D = dist ⁡ U
7 imasf1obl.m ⊢ φ → E ∈ ∞Met ⁡ V
8 imasf1obl.x ⊢ φ → P ∈ V
9 imasf1obl.s ⊢ φ → S ∈ ℝ *
10 f1ocnvfv2 ⊢ F : V ⟶ 1-1 onto B ∧ x ∈ B → F ⁡ F -1 ⁡ x = x
11 3 10 sylan ⊢ φ ∧ x ∈ B → F ⁡ F -1 ⁡ x = x
12 11 oveq2d ⊢ φ ∧ x ∈ B → F ⁡ P D F ⁡ F -1 ⁡ x = F ⁡ P D x
13 1 adantr ⊢ φ ∧ x ∈ B → U = F “ 𝑠 R
14 2 adantr ⊢ φ ∧ x ∈ B → V = Base R
15 3 adantr ⊢ φ ∧ x ∈ B → F : V ⟶ 1-1 onto B
16 4 adantr ⊢ φ ∧ x ∈ B → R ∈ Z
17 7 adantr ⊢ φ ∧ x ∈ B → E ∈ ∞Met ⁡ V
18 8 adantr ⊢ φ ∧ x ∈ B → P ∈ V
19 f1ocnv ⊢ F : V ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto V
20 3 19 syl ⊢ φ → F -1 : B ⟶ 1-1 onto V
21 f1of ⊢ F -1 : B ⟶ 1-1 onto V → F -1 : B ⟶ V
22 20 21 syl ⊢ φ → F -1 : B ⟶ V
23 22 ffvelcdmda ⊢ φ ∧ x ∈ B → F -1 ⁡ x ∈ V
24 13 14 15 16 5 6 17 18 23 imasdsf1o ⊢ φ ∧ x ∈ B → F ⁡ P D F ⁡ F -1 ⁡ x = P E F -1 ⁡ x
25 12 24 eqtr3d ⊢ φ ∧ x ∈ B → F ⁡ P D x = P E F -1 ⁡ x
26 25 breq1d ⊢ φ ∧ x ∈ B → F ⁡ P D x < S ↔ P E F -1 ⁡ x < S
27 9 adantr ⊢ φ ∧ x ∈ B → S ∈ ℝ *
28 elbl2 ⊢ E ∈ ∞Met ⁡ V ∧ S ∈ ℝ * ∧ P ∈ V ∧ F -1 ⁡ x ∈ V → F -1 ⁡ x ∈ P ball ⁡ E S ↔ P E F -1 ⁡ x < S
29 17 27 18 23 28 syl22anc ⊢ φ ∧ x ∈ B → F -1 ⁡ x ∈ P ball ⁡ E S ↔ P E F -1 ⁡ x < S
30 26 29 bitr4d ⊢ φ ∧ x ∈ B → F ⁡ P D x < S ↔ F -1 ⁡ x ∈ P ball ⁡ E S
31 30 pm5.32da ⊢ φ → x ∈ B ∧ F ⁡ P D x < S ↔ x ∈ B ∧ F -1 ⁡ x ∈ P ball ⁡ E S
32 1 2 3 4 5 6 7 imasf1oxmet ⊢ φ → D ∈ ∞Met ⁡ B
33 f1of ⊢ F : V ⟶ 1-1 onto B → F : V ⟶ B
34 3 33 syl ⊢ φ → F : V ⟶ B
35 34 8 ffvelcdmd ⊢ φ → F ⁡ P ∈ B
36 elbl ⊢ D ∈ ∞Met ⁡ B ∧ F ⁡ P ∈ B ∧ S ∈ ℝ * → x ∈ F ⁡ P ball ⁡ D S ↔ x ∈ B ∧ F ⁡ P D x < S
37 32 35 9 36 syl3anc ⊢ φ → x ∈ F ⁡ P ball ⁡ D S ↔ x ∈ B ∧ F ⁡ P D x < S
38 f1ofn ⊢ F -1 : B ⟶ 1-1 onto V → F -1 Fn B
39 elpreima ⊢ F -1 Fn B → x ∈ F -1 -1 P ball ⁡ E S ↔ x ∈ B ∧ F -1 ⁡ x ∈ P ball ⁡ E S
40 20 38 39 3syl ⊢ φ → x ∈ F -1 -1 P ball ⁡ E S ↔ x ∈ B ∧ F -1 ⁡ x ∈ P ball ⁡ E S
41 31 37 40 3bitr4d ⊢ φ → x ∈ F ⁡ P ball ⁡ D S ↔ x ∈ F -1 -1 P ball ⁡ E S
42 41 eqrdv ⊢ φ → F ⁡ P ball ⁡ D S = F -1 -1 P ball ⁡ E S
43 imacnvcnv ⊢ F -1 -1 P ball ⁡ E S = F P ball ⁡ E S
44 42 43 eqtrdi ⊢ φ → F ⁡ P ball ⁡ D S = F P ball ⁡ E S