This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
35 33 22 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 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 𝐾 ) )