nghmcn

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

	Ref	Expression
Hypotheses	nghmcn.j	$⊢ J = TopOpen (S)$
	nghmcn.k	$⊢ K = TopOpen (T)$
Assertion	nghmcn	$⊢ F \in (S NGHom T) \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		nghmcn.j	$⊢ J = TopOpen (S)$
2		nghmcn.k	$⊢ K = TopOpen (T)$
3		nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5		eqid	$⊢ {Base}_{T} = {Base}_{T}$
6	4 5	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
7	3 6	syl	$⊢ F \in (S NGHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
8		simprr	$⊢ (F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \to r \in ℝ^{+}$
9		eqid	$⊢ S normOp T = S normOp T$
10	9	nghmcl	$⊢ F \in (S NGHom T) \to (S normOp T) (F) \in ℝ$
11		nghmrcl1	$⊢ F \in (S NGHom T) \to S \in NrmGrp$
12		nghmrcl2	$⊢ F \in (S NGHom T) \to T \in NrmGrp$
13	9	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq (S normOp T) (F)$
14	11 12 3 13	syl3anc	$⊢ F \in (S NGHom T) \to 0 \leq (S normOp T) (F)$
15	10 14	ge0p1rpd	$⊢ F \in (S NGHom T) \to (S normOp T) (F) + 1 \in ℝ^{+}$
16	15	adantr	$⊢ (F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \to (S normOp T) (F) + 1 \in ℝ^{+}$
17	8 16	rpdivcld	$⊢ (F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \to \frac{r}{(S normOp T) (F) + 1} \in ℝ^{+}$
18		ngpms	$⊢ S \in NrmGrp \to S \in MetSp$
19	11 18	syl	$⊢ F \in (S NGHom T) \to S \in MetSp$
20	19	ad2antrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to S \in MetSp$
21		simplrl	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to x \in {Base}_{S}$
22		simpr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to y \in {Base}_{S}$
23		eqid	$⊢ dist (S) = dist (S)$
24	4 23	mscl	$⊢ (S \in MetSp \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x dist (S) y \in ℝ$
25	20 21 22 24	syl3anc	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to x dist (S) y \in ℝ$
26	8	adantr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to r \in ℝ^{+}$
27	26	rpred	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to r \in ℝ$
28	15	ad2antrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) + 1 \in ℝ^{+}$
29	25 27 28	ltmuldiv2d	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (((S normOp T) (F) + 1) (x dist (S) y) < r \leftrightarrow x dist (S) y < \frac{r}{(S normOp T) (F) + 1})$
30		ngpms	$⊢ T \in NrmGrp \to T \in MetSp$
31	12 30	syl	$⊢ F \in (S NGHom T) \to T \in MetSp$
32	31	ad2antrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to T \in MetSp$
33	7	ad2antrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F : {Base}_{S} ⟶ {Base}_{T}$
34	33 21	ffvelrnd	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (x) \in {Base}_{T}$
35	33 22	ffvelrnd	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (y) \in {Base}_{T}$
36		eqid	$⊢ dist (T) = dist (T)$
37	5 36	mscl	$⊢ (T \in MetSp \land F (x) \in {Base}_{T} \land F (y) \in {Base}_{T}) \to F (x) dist (T) F (y) \in ℝ$
38	32 34 35 37	syl3anc	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (x) dist (T) F (y) \in ℝ$
39	10	ad2antrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) \in ℝ$
40	39 25	remulcld	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) (x dist (S) y) \in ℝ$
41	28	rpred	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) + 1 \in ℝ$
42	41 25	remulcld	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to ((S normOp T) (F) + 1) (x dist (S) y) \in ℝ$
43	9 4 23 36	nmods	$⊢ (F \in (S NGHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x) dist (T) F (y) \leq (S normOp T) (F) (x dist (S) y)$
44	43	3expa	$⊢ ((F \in (S NGHom T) \land x \in {Base}_{S}) \land y \in {Base}_{S}) \to F (x) dist (T) F (y) \leq (S normOp T) (F) (x dist (S) y)$
45	44	adantlrr	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (x) dist (T) F (y) \leq (S normOp T) (F) (x dist (S) y)$
46		msxms	$⊢ S \in MetSp \to S \in ∞MetSp$
47	20 46	syl	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to S \in ∞MetSp$
48	4 23	xmsge0	$⊢ (S \in ∞MetSp \land x \in {Base}_{S} \land y \in {Base}_{S}) \to 0 \leq x dist (S) y$
49	47 21 22 48	syl3anc	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to 0 \leq x dist (S) y$
50	39	lep1d	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) \leq (S normOp T) (F) + 1$
51	39 41 25 49 50	lemul1ad	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (S normOp T) (F) (x dist (S) y) \leq ((S normOp T) (F) + 1) (x dist (S) y)$
52	38 40 42 45 51	letrd	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (x) dist (T) F (y) \leq ((S normOp T) (F) + 1) (x dist (S) y)$
53		lelttr	$⊢ (F (x) dist (T) F (y) \in ℝ \land ((S normOp T) (F) + 1) (x dist (S) y) \in ℝ \land r \in ℝ) \to ((F (x) dist (T) F (y) \leq ((S normOp T) (F) + 1) (x dist (S) y) \land ((S normOp T) (F) + 1) (x dist (S) y) < r) \to F (x) dist (T) F (y) < r)$
54	38 42 27 53	syl3anc	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to ((F (x) dist (T) F (y) \leq ((S normOp T) (F) + 1) (x dist (S) y) \land ((S normOp T) (F) + 1) (x dist (S) y) < r) \to F (x) dist (T) F (y) < r)$
55	52 54	mpand	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (((S normOp T) (F) + 1) (x dist (S) y) < r \to F (x) dist (T) F (y) < r)$
56	29 55	sylbird	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (x dist (S) y < \frac{r}{(S normOp T) (F) + 1} \to F (x) dist (T) F (y) < r)$
57	21 22	ovresd	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y = x dist (S) y$
58	57	breq1d	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < \frac{r}{(S normOp T) (F) + 1} \leftrightarrow x dist (S) y < \frac{r}{(S normOp T) (F) + 1})$
59	34 35	ovresd	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) = F (x) dist (T) F (y)$
60	59	breq1d	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r \leftrightarrow F (x) dist (T) F (y) < r)$
61	56 58 60	3imtr4d	$⊢ ((F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \land y \in {Base}_{S}) \to (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < \frac{r}{(S normOp T) (F) + 1} \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)$
62	61	ralrimiva	$⊢ (F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \to \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < \frac{r}{(S normOp T) (F) + 1} \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)$
63		breq2	$⊢ s = \frac{r}{(S normOp T) (F) + 1} \to (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \leftrightarrow x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < \frac{r}{(S normOp T) (F) + 1})$
64	63	rspceaimv	$⊢ (\frac{r}{(S normOp T) (F) + 1} \in ℝ^{+} \land \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < \frac{r}{(S normOp T) (F) + 1} \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)) \to \exists s \in ℝ^{+} \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)$
65	17 62 64	syl2anc	$⊢ (F \in (S NGHom T) \land (x \in {Base}_{S} \land r \in ℝ^{+})) \to \exists s \in ℝ^{+} \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)$
66	65	ralrimivva	$⊢ F \in (S NGHom T) \to \forall x \in {Base}_{S} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)$
67		eqid	$⊢ {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} = {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}$
68	4 67	xmsxmet	$⊢ S \in ∞MetSp \to {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S})$
69	19 46 68	3syl	$⊢ F \in (S NGHom T) \to {dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S})$
70		msxms	$⊢ T \in MetSp \to T \in ∞MetSp$
71		eqid	$⊢ {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} = {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}$
72	5 71	xmsxmet	$⊢ T \in ∞MetSp \to {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})$
73	31 70 72	3syl	$⊢ F \in (S NGHom T) \to {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})$
74		eqid	$⊢ MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
75		eqid	$⊢ MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
76	74 75	metcn	$⊢ ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})} \in ∞Met ({Base}_{S}) \land {dist (T) ↾}_{({Base}_{T} \times {Base}_{T})} \in ∞Met ({Base}_{T})) \to (F \in (MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) Cn MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})) \leftrightarrow (F : {Base}_{S} ⟶ {Base}_{T} \land \forall x \in {Base}_{S} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)))$
77	69 73 76	syl2anc	$⊢ F \in (S NGHom T) \to (F \in (MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) Cn MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})) \leftrightarrow (F : {Base}_{S} ⟶ {Base}_{T} \land \forall x \in {Base}_{S} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall y \in {Base}_{S} (x ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) y < s \to F (x) ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}) F (y) < r)))$
78	7 66 77	mpbir2and	$⊢ F \in (S NGHom T) \to F \in (MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) Cn MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})}))$
79	1 4 67	mstopn	$⊢ S \in MetSp \to J = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
80	19 79	syl	$⊢ F \in (S NGHom T) \to J = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})})$
81	2 5 71	mstopn	$⊢ T \in MetSp \to K = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
82	31 81	syl	$⊢ F \in (S NGHom T) \to K = MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
83	80 82	oveq12d	$⊢ F \in (S NGHom T) \to J Cn K = MetOpen ({dist (S) ↾}_{({Base}_{S} \times {Base}_{S})}) Cn MetOpen ({dist (T) ↾}_{({Base}_{T} \times {Base}_{T})})$
84	78 83	eleqtrrd	$⊢ F \in (S NGHom T) \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem nghmcn

Proof