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 ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasf1obl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasf1obl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasf1obl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasf1obl.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
imasf1obl.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
imasf1obl.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
imasf1obl.x ⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
imasf1obl.s ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
Assertion imasf1obl ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) = ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 imasf1obl.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasf1obl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasf1obl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasf1obl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasf1obl.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 imasf1obl.d ⊢ 𝐷 = ( dist ‘ 𝑈 )
7 imasf1obl.m ⊢ ( 𝜑 → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
8 imasf1obl.x ⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
9 imasf1obl.s ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
10 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
11 3 10 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
12 11 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑉 = ( Base ‘ 𝑅 ) )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ 𝑍 )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
18 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑃 ∈ 𝑉 )
19 f1ocnv ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝑉 )
20 3 19 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝑉 )
21 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝑉 → ◡ 𝐹 : 𝐵 ⟶ 𝑉 )
22 20 21 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 ⟶ 𝑉 )
23 22 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑉 )
24 13 14 15 16 5 6 17 18 23 imasdsf1o ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) = ( 𝑃 𝐸 ( ◡ 𝐹 ‘ 𝑥 ) ) )
25 12 24 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) = ( 𝑃 𝐸 ( ◡ 𝐹 ‘ 𝑥 ) ) )
26 25 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) < 𝑆 ↔ ( 𝑃 𝐸 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑆 ) )
27 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ ℝ* )
28 elbl2 ⊢ ( ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑆 ∈ ℝ* ) ∧ ( 𝑃 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ↔ ( 𝑃 𝐸 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑆 ) )
29 17 27 18 23 28 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ↔ ( 𝑃 𝐸 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑆 ) )
30 26 29 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) < 𝑆 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) )
31 30 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) < 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ) )
32 1 2 3 4 5 6 7 imasf1oxmet ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
33 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
34 3 33 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
35 34 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ 𝐵 )
36 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐵 ∧ 𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) < 𝑆 ) ) )
37 32 35 9 36 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑃 ) 𝐷 𝑥 ) < 𝑆 ) ) )
38 f1ofn ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝑉 → ◡ 𝐹 Fn 𝐵 )
39 elpreima ⊢ ( ◡ 𝐹 Fn 𝐵 → ( 𝑥 ∈ ( ◡ ◡ 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ) )
40 20 38 39 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ◡ 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ) )
41 31 37 40 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) ↔ 𝑥 ∈ ( ◡ ◡ 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) ) )
42 41 eqrdv ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) = ( ◡ ◡ 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) )
43 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) = ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) )
44 42 43 eqtrdi ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑆 ) = ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐸 ) 𝑆 ) ) )