qqhucn

Description: The QQHom homomorphism is uniformly continuous. (Contributed by Thierry Arnoux, 28-Jan-2018)

	Ref	Expression
Hypotheses	qqhucn.b	$⊢ B = {Base}_{R}$
	qqhucn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qqhucn.u	$⊢ U = UnifSt (Q)$
	qqhucn.v	$⊢ V = metUnif ({dist (R) ↾}_{(B \times B)})$
	qqhucn.z	$⊢ Z = ℤMod (R)$
	qqhucn.1	$⊢ φ \to R \in NrmRing$
	qqhucn.2	$⊢ φ \to R \in DivRing$
	qqhucn.3	$⊢ φ \to Z \in NrmMod$
	qqhucn.4	$⊢ φ \to chr (R) = 0$
Assertion	qqhucn	$⊢ φ \to ℚHom (R) \in (U uCn V)$

Proof

Step	Hyp	Ref	Expression
1		qqhucn.b	$⊢ B = {Base}_{R}$
2		qqhucn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
3		qqhucn.u	$⊢ U = UnifSt (Q)$
4		qqhucn.v	$⊢ V = metUnif ({dist (R) ↾}_{(B \times B)})$
5		qqhucn.z	$⊢ Z = ℤMod (R)$
6		qqhucn.1	$⊢ φ \to R \in NrmRing$
7		qqhucn.2	$⊢ φ \to R \in DivRing$
8		qqhucn.3	$⊢ φ \to Z \in NrmMod$
9		qqhucn.4	$⊢ φ \to chr (R) = 0$
10		eqid	$⊢ /_{r} (R) = /_{r} (R)$
11		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
12	1 10 11	qqhf	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$
13	7 9 12	syl2anc	$⊢ φ \to ℚHom (R) : ℚ ⟶ B$
14		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
15		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
16	6 15	syl	$⊢ φ \to R \in NrmGrp$
17	16	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to R \in NrmGrp$
18	13	ffvelrnda	$⊢ (φ \land p \in ℚ) \to ℚHom (R) (p) \in B$
19	18	adantr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (p) \in B$
20	13	adantr	$⊢ (φ \land p \in ℚ) \to ℚHom (R) : ℚ ⟶ B$
21	20	ffvelrnda	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (q) \in B$
22		eqid	$⊢ norm (R) = norm (R)$
23		eqid	$⊢ -_{R} = -_{R}$
24		eqid	$⊢ dist (R) = dist (R)$
25	22 1 23 24	ngpdsr	$⊢ (R \in NrmGrp \land ℚHom (R) (p) \in B \land ℚHom (R) (q) \in B) \to ℚHom (R) (p) dist (R) ℚHom (R) (q) = norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (p))$
26	17 19 21 25	syl3anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (p) dist (R) ℚHom (R) (q) = norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (p))$
27		simpr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to q \in ℚ$
28		simplr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p \in ℚ$
29		qsubdrg	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
30	29	simpli	$⊢ ℚ \in SubRing (ℂ_{fld})$
31		subrgsubg	$⊢ ℚ \in SubRing (ℂ_{fld}) \to ℚ \in SubGrp (ℂ_{fld})$
32	30 31	ax-mp	$⊢ ℚ \in SubGrp (ℂ_{fld})$
33		cnfldsub	$⊢ - = -_{ℂ_{fld}}$
34		eqid	$⊢ -_{Q} = -_{Q}$
35	33 2 34	subgsub	$⊢ (ℚ \in SubGrp (ℂ_{fld}) \land q \in ℚ \land p \in ℚ) \to q - p = q -_{Q} p$
36	32 35	mp3an1	$⊢ (q \in ℚ \land p \in ℚ) \to q - p = q -_{Q} p$
37	27 28 36	syl2anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to q - p = q -_{Q} p$
38	37	fveq2d	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (q - p) = ℚHom (R) (q -_{Q} p)$
39	1 10 11 2	qqhghm	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) \in (Q GrpHom R)$
40	7 9 39	syl2anc	$⊢ φ \to ℚHom (R) \in (Q GrpHom R)$
41	40	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) \in (Q GrpHom R)$
42	2	qrngbas	$⊢ ℚ = {Base}_{Q}$
43	42 34 23	ghmsub	$⊢ (ℚHom (R) \in (Q GrpHom R) \land q \in ℚ \land p \in ℚ) \to ℚHom (R) (q -_{Q} p) = ℚHom (R) (q) -_{R} ℚHom (R) (p)$
44	41 27 28 43	syl3anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (q -_{Q} p) = ℚHom (R) (q) -_{R} ℚHom (R) (p)$
45	38 44	eqtr2d	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (q) -_{R} ℚHom (R) (p) = ℚHom (R) (q - p)$
46	45	fveq2d	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (p)) = norm (R) (ℚHom (R) (q - p))$
47	6 7	elind	$⊢ φ \to R \in (NrmRing \cap DivRing)$
48	47	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to R \in (NrmRing \cap DivRing)$
49	8	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to Z \in NrmMod$
50	9	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to chr (R) = 0$
51		qsubcl	$⊢ (q \in ℚ \land p \in ℚ) \to q - p \in ℚ$
52	27 28 51	syl2anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to q - p \in ℚ$
53	22 5	qqhnm	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land q - p \in ℚ) \to norm (R) (ℚHom (R) (q - p)) = \|q - p\|$
54	48 49 50 52 53	syl31anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to norm (R) (ℚHom (R) (q - p)) = \|q - p\|$
55	26 46 54	3eqtrd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (p) dist (R) ℚHom (R) (q) = \|q - p\|$
56	19 21	ovresd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) = ℚHom (R) (p) dist (R) ℚHom (R) (q)$
57		qsscn	$⊢ ℚ \subseteq ℂ$
58	57 28	sselid	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p \in ℂ$
59	57 27	sselid	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to q \in ℂ$
60		eqid	$⊢ abs \circ - = abs \circ -$
61	60	cnmetdval	$⊢ (p \in ℂ \land q \in ℂ) \to p (abs \circ -) q = \|p - q\|$
62	58 59 61	syl2anc	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p (abs \circ -) q = \|p - q\|$
63	28 27	ovresd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = p (abs \circ -) q$
64	59 58	abssubd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to \|q - p\| = \|p - q\|$
65	62 63 64	3eqtr4d	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = \|q - p\|$
66	55 56 65	3eqtr4rd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q)$
67	66	breq1d	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \leftrightarrow ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
68	67	biimpd	$⊢ ((φ \land p \in ℚ) \land q \in ℚ) \to (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
69	68	ralrimiva	$⊢ (φ \land p \in ℚ) \to \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
70	69	ralrimiva	$⊢ φ \to \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
71	70	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
72		breq2	$⊢ d = e \to (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \leftrightarrow p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e)$
73	72	imbi1d	$⊢ d = e \to ((p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e) \leftrightarrow (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e))$
74	73	2ralbidv	$⊢ d = e \to (\forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e) \leftrightarrow \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e))$
75	74	rspcev	$⊢ (e \in ℝ^{+} \land \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)) \to \exists d \in ℝ^{+} \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
76	14 71 75	syl2anc	$⊢ (φ \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
77	76	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)$
78		eqid	$⊢ metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
79		0z	$⊢ 0 \in ℤ$
80		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
81		ne0i	$⊢ 0 \in ℚ \to ℚ \neq \emptyset$
82	79 80 81	mp2b	$⊢ ℚ \neq \emptyset$
83	82	a1i	$⊢ φ \to ℚ \neq \emptyset$
84		drngring	$⊢ R \in DivRing \to R \in Ring$
85		eqid	$⊢ 1_{R} = 1_{R}$
86	1 85	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
87		ne0i	$⊢ 1_{R} \in B \to B \neq \emptyset$
88	7 84 86 87	4syl	$⊢ φ \to B \neq \emptyset$
89		cnfldxms	$⊢ ℂ_{fld} \in ∞MetSp$
90		qex	$⊢ ℚ \in V$
91		ressxms	$⊢ (ℂ_{fld} \in ∞MetSp \land ℚ \in V) \to ℂ_{fld} ↾_{𝑠} ℚ \in ∞MetSp$
92	89 90 91	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in ∞MetSp$
93	2 92	eqeltri	$⊢ Q \in ∞MetSp$
94		cnfldds	$⊢ abs \circ - = dist (ℂ_{fld})$
95	2 94	ressds	$⊢ ℚ \in V \to abs \circ - = dist (Q)$
96	90 95	ax-mp	$⊢ abs \circ - = dist (Q)$
97	42 96	xmsxmet2	$⊢ Q \in ∞MetSp \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ)$
98	93 97	mp1i	$⊢ φ \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ)$
99		xmetpsmet	$⊢ {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ) \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in PsMet (ℚ)$
100	98 99	syl	$⊢ φ \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in PsMet (ℚ)$
101		ngpxms	$⊢ R \in NrmGrp \to R \in ∞MetSp$
102	1 24	xmsxmet2	$⊢ R \in ∞MetSp \to {dist (R) ↾}_{(B \times B)} \in ∞Met (B)$
103	6 15 101 102	4syl	$⊢ φ \to {dist (R) ↾}_{(B \times B)} \in ∞Met (B)$
104		xmetpsmet	$⊢ {dist (R) ↾}_{(B \times B)} \in ∞Met (B) \to {dist (R) ↾}_{(B \times B)} \in PsMet (B)$
105	103 104	syl	$⊢ φ \to {dist (R) ↾}_{(B \times B)} \in PsMet (B)$
106	78 4 83 88 100 105	metucn	$⊢ φ \to (ℚHom (R) \in (metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) uCn V) \leftrightarrow (ℚHom (R) : ℚ ⟶ B \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall p \in ℚ \forall q \in ℚ (p ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (p) ({dist (R) ↾}_{(B \times B)}) ℚHom (R) (q) < e)))$
107	13 77 106	mpbir2and	$⊢ φ \to ℚHom (R) \in (metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) uCn V)$
108	2	fveq2i	$⊢ UnifSt (Q) = UnifSt (ℂ_{fld} ↾_{𝑠} ℚ)$
109		ressuss	$⊢ ℚ \in V \to UnifSt (ℂ_{fld} ↾_{𝑠} ℚ) = UnifSt (ℂ_{fld}) ↾_{𝑡} (ℚ \times ℚ)$
110	90 109	ax-mp	$⊢ UnifSt (ℂ_{fld} ↾_{𝑠} ℚ) = UnifSt (ℂ_{fld}) ↾_{𝑡} (ℚ \times ℚ)$
111	3 108 110	3eqtri	$⊢ U = UnifSt (ℂ_{fld}) ↾_{𝑡} (ℚ \times ℚ)$
112		eqid	$⊢ UnifSt (ℂ_{fld}) = UnifSt (ℂ_{fld})$
113	112	cnflduss	$⊢ UnifSt (ℂ_{fld}) = metUnif (abs \circ -)$
114	113	oveq1i	$⊢ UnifSt (ℂ_{fld}) ↾_{𝑡} (ℚ \times ℚ) = metUnif (abs \circ -) ↾_{𝑡} (ℚ \times ℚ)$
115		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
116		xmetpsmet	$⊢ abs \circ - \in ∞Met (ℂ) \to abs \circ - \in PsMet (ℂ)$
117	115 116	ax-mp	$⊢ abs \circ - \in PsMet (ℂ)$
118		restmetu	$⊢ (ℚ \neq \emptyset \land abs \circ - \in PsMet (ℂ) \land ℚ \subseteq ℂ) \to metUnif (abs \circ -) ↾_{𝑡} (ℚ \times ℚ) = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
119	82 117 57 118	mp3an	$⊢ metUnif (abs \circ -) ↾_{𝑡} (ℚ \times ℚ) = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
120	111 114 119	3eqtri	$⊢ U = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
121	120	a1i	$⊢ φ \to U = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
122	121	oveq1d	$⊢ φ \to U uCn V = metUnif ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) uCn V$
123	107 122	eleqtrrd	$⊢ φ \to ℚHom (R) \in (U uCn V)$

Metamath Proof Explorer

Theorem qqhucn

Proof