Metamath Proof Explorer


Theorem nghmcn

Description: A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nghmcn.j 𝐽 = ( TopOpen ‘ 𝑆 )
nghmcn.k 𝐾 = ( TopOpen ‘ 𝑇 )
Assertion nghmcn ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 nghmcn.j 𝐽 = ( TopOpen ‘ 𝑆 )
2 nghmcn.k 𝐾 = ( TopOpen ‘ 𝑇 )
3 nghmghm ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
4 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
6 4 5 ghmf ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
7 3 6 syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
8 simprr ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ )
9 eqid ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 )
10 9 nghmcl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ )
11 nghmrcl1 ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
12 nghmrcl2 ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp )
13 9 nmoge0 ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) )
14 11 12 3 13 syl3anc ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 0 ≤ ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) )
15 10 14 ge0p1rpd ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ∈ ℝ+ )
16 15 adantr ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ∈ ℝ+ )
17 8 16 rpdivcld ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ∈ ℝ+ )
18 ngpms ( 𝑆 ∈ NrmGrp → 𝑆 ∈ MetSp )
19 11 18 syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ MetSp )
20 19 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑆 ∈ MetSp )
21 simplrl ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
22 simpr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
23 eqid ( dist ‘ 𝑆 ) = ( dist ‘ 𝑆 )
24 4 23 mscl ( ( 𝑆 ∈ MetSp ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ∈ ℝ )
25 20 21 22 24 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ∈ ℝ )
26 8 adantr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑟 ∈ ℝ+ )
27 26 rpred ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑟 ∈ ℝ )
28 15 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ∈ ℝ+ )
29 25 27 28 ltmuldiv2d ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) < 𝑟 ↔ ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ) )
30 ngpms ( 𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp )
31 12 30 syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ MetSp )
32 31 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑇 ∈ MetSp )
33 7 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
34 33 21 ffvelrnd ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) )
35 33 22 ffvelrnd ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹𝑦 ) ∈ ( Base ‘ 𝑇 ) )
36 eqid ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
37 5 36 mscl ( ( 𝑇 ∈ MetSp ∧ ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐹𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ∈ ℝ )
38 32 34 35 37 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ∈ ℝ )
39 10 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ )
40 39 25 remulcld ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ∈ ℝ )
41 28 rpred ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ∈ ℝ )
42 41 25 remulcld ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ∈ ℝ )
43 9 4 23 36 nmods ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) )
44 43 3expa ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) )
45 44 adantlrr ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) )
46 msxms ( 𝑆 ∈ MetSp → 𝑆 ∈ ∞MetSp )
47 20 46 syl ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑆 ∈ ∞MetSp )
48 4 23 xmsge0 ( ( 𝑆 ∈ ∞MetSp ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 0 ≤ ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) )
49 47 21 22 48 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 0 ≤ ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) )
50 39 lep1d ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) )
51 39 41 25 49 50 lemul1ad ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ≤ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) )
52 38 40 42 45 51 letrd ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) )
53 lelttr ( ( ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ∈ ℝ ∧ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ∧ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) < 𝑟 ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) < 𝑟 ) )
54 38 42 27 53 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) ≤ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) ∧ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) < 𝑟 ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) < 𝑟 ) )
55 52 54 mpand ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) · ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) ) < 𝑟 → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) < 𝑟 ) )
56 29 55 sylbird ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) → ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) < 𝑟 ) )
57 21 22 ovresd ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) = ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) )
58 57 breq1d ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ↔ ( 𝑥 ( dist ‘ 𝑆 ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ) )
59 34 35 ovresd ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) = ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) )
60 59 breq1d ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ↔ ( ( 𝐹𝑥 ) ( dist ‘ 𝑇 ) ( 𝐹𝑦 ) ) < 𝑟 ) )
61 56 58 60 3imtr4d ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) )
62 61 ralrimiva ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) )
63 breq2 ( 𝑠 = ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) → ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 ↔ ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ) )
64 63 rspceaimv ( ( ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < ( 𝑟 / ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + 1 ) ) → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) )
65 17 62 64 syl2anc ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) → ∃ 𝑠 ∈ ℝ+𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) )
66 65 ralrimivva ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) )
67 eqid ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) = ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) )
68 4 67 xmsxmet ( 𝑆 ∈ ∞MetSp → ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑆 ) ) )
69 19 46 68 3syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑆 ) ) )
70 msxms ( 𝑇 ∈ MetSp → 𝑇 ∈ ∞MetSp )
71 eqid ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) = ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) )
72 5 71 xmsxmet ( 𝑇 ∈ ∞MetSp → ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑇 ) ) )
73 31 70 72 3syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑇 ) ) )
74 eqid ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) )
75 eqid ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) )
76 74 75 metcn ( ( ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑆 ) ) ∧ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑇 ) ) ) → ( 𝐹 ∈ ( ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) ) ↔ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) ) ) )
77 69 73 76 syl2anc ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝐹 ∈ ( ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) ) ↔ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝑥 ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) 𝑦 ) < 𝑠 → ( ( 𝐹𝑥 ) ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ( 𝐹𝑦 ) ) < 𝑟 ) ) ) )
78 7 66 77 mpbir2and ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) ) )
79 1 4 67 mstopn ( 𝑆 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) )
80 19 79 syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) )
81 2 5 71 mstopn ( 𝑇 ∈ MetSp → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) )
82 31 81 syl ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) )
83 80 82 oveq12d ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝐽 Cn 𝐾 ) = ( ( MetOpen ‘ ( ( dist ‘ 𝑆 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) ) Cn ( MetOpen ‘ ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) ) )
84 78 83 eleqtrrd ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )