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 𝐾 ) )