Metamath Proof Explorer

Theorem ismtyima

Description: The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014)

Ref Expression
Assertion ismtyima ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 imassrn ⊢ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ⊆ ran 𝐹
2 isismty ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
3 2 biimp3a ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
4 3 adantr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
5 4 simpld ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
6 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
7 5 6 syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
8 7 frnd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ran 𝐹 ⊆ 𝑌 )
9 1 8 sstrid ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ⊆ 𝑌 )
10 9 sseld ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) → 𝑥 ∈ 𝑌 ) )
11 simpl2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
12 simprl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝑃 ∈ 𝑋 )
13 ffvelcdm ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
14 7 12 13 syl2anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
15 simprr ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝑅 ∈ ℝ* )
16 blssm ⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ 𝑅 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ⊆ 𝑌 )
17 11 14 15 16 syl3anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ⊆ 𝑌 )
18 17 sseld ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) → 𝑥 ∈ 𝑌 ) )
19 simpl1 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
20 19 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
21 simplrr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ∈ ℝ* )
22 simplrl ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑃 ∈ 𝑋 )
23 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
24 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
25 5 23 24 3syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
26 ffvelcdm ⊢ ( ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
27 25 26 sylan ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
28 elbl2 ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑃 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ↔ ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑅 ) )
29 20 21 22 27 28 syl22anc ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ↔ ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑅 ) )
30 4 simprd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) )
31 oveq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 𝑀 𝑦 ) = ( 𝑃 𝑀 𝑦 ) )
32 fveq2 ⊢ ( 𝑥 = 𝑃 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑃 ) )
33 32 oveq1d ⊢ ( 𝑥 = 𝑃 → ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) )
34 31 33 eqeq12d ⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑃 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
35 oveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑥 ) → ( 𝑃 𝑀 𝑦 ) = ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) )
36 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) )
37 36 oveq2d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
38 35 37 eqeq12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑥 ) → ( ( 𝑃 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
39 34 38 rspc2v ⊢ ( ( 𝑃 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
40 39 impancom ⊢ ( ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 → ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
41 12 30 40 syl2anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 → ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
42 41 imp ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) → ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
43 27 42 syldan ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
44 43 breq1d ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑃 𝑀 ( ◡ 𝐹 ‘ 𝑥 ) ) < 𝑅 ↔ ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) < 𝑅 ) )
45 29 44 bitrd ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ↔ ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) < 𝑅 ) )
46 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 )
47 5 46 syl ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
48 47 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
49 blssm ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 )
50 19 12 15 49 syl3anc ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 )
51 50 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 )
52 f1elima ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ⊆ 𝑋 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) )
53 48 27 51 52 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) )
54 11 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
55 14 adantr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
56 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
57 5 56 sylan ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
58 simpr ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑌 )
59 57 58 eqeltrd ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 )
60 elbl2 ⊢ ( ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ↔ ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) < 𝑅 ) )
61 54 21 55 59 60 syl22anc ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ↔ ( ( 𝐹 ‘ 𝑃 ) 𝑁 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) < 𝑅 ) )
62 45 53 61 3bitr4d ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ) )
63 57 eleq1d ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ 𝑥 ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ) )
64 57 eleq1d ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ) )
65 62 63 64 3bitr3d ⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ) )
66 65 ex ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝑥 ∈ 𝑌 → ( 𝑥 ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ) ) )
67 10 18 66 pm5.21ndd ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) ↔ 𝑥 ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) ) )
68 67 eqrdv ⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝑀 ) 𝑅 ) ) = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝑁 ) 𝑅 ) )