qqhcn

Description: The QQHom homomorphism is a continuous function. (Contributed by Thierry Arnoux, 9-Nov-2017)

	Ref	Expression
Hypotheses	qqhcn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qqhcn.j	$⊢ J = TopOpen (Q)$
	qqhcn.z	$⊢ Z = ℤMod (R)$
	qqhcn.k	$⊢ K = TopOpen (R)$
Assertion	qqhcn	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		qqhcn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qqhcn.j	$⊢ J = TopOpen (Q)$
3		qqhcn.z	$⊢ Z = ℤMod (R)$
4		qqhcn.k	$⊢ K = TopOpen (R)$
5		inss2	$⊢ NrmRing \cap DivRing \subseteq DivRing$
6	5	sseli	$⊢ R \in (NrmRing \cap DivRing) \to R \in DivRing$
7	6	3ad2ant1	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to R \in DivRing$
8		simp3	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to chr (R) = 0$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ /_{r} (R) = /_{r} (R)$
11		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
12	9 10 11	qqhf	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ {Base}_{R}$
13	7 8 12	syl2anc	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ {Base}_{R}$
14		simpr	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \to e \in ℝ^{+}$
15		qsscn	$⊢ ℚ \subseteq ℂ$
16		simpr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to q \in ℚ$
17	15 16	sselid	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to q \in ℂ$
18		0cn	$⊢ 0 \in ℂ$
19		eqid	$⊢ abs \circ - = abs \circ -$
20	19	cnmetdval	$⊢ (0 \in ℂ \land q \in ℂ) \to 0 (abs \circ -) q = \|0 - q\|$
21	18 20	mpan	$⊢ q \in ℂ \to 0 (abs \circ -) q = \|0 - q\|$
22		df-neg	$⊢ - q = 0 - q$
23	22	fveq2i	$⊢ \|- q\| = \|0 - q\|$
24	23	a1i	$⊢ q \in ℂ \to \|- q\| = \|0 - q\|$
25		absneg	$⊢ q \in ℂ \to \|- q\| = \|q\|$
26	21 24 25	3eqtr2d	$⊢ q \in ℂ \to 0 (abs \circ -) q = \|q\|$
27	17 26	syl	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to 0 (abs \circ -) q = \|q\|$
28		zssq	$⊢ ℤ \subseteq ℚ$
29		0z	$⊢ 0 \in ℤ$
30	28 29	sselii	$⊢ 0 \in ℚ$
31	30	a1i	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to 0 \in ℚ$
32	31 16	ovresd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to 0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = 0 (abs \circ -) q$
33		eqid	$⊢ norm (R) = norm (R)$
34	33 3	qqhnm	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land q \in ℚ) \to norm (R) (ℚHom (R) (q)) = \|q\|$
35	34	adantlr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to norm (R) (ℚHom (R) (q)) = \|q\|$
36	27 32 35	3eqtr4d	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to 0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = norm (R) (ℚHom (R) (q))$
37	13	ad2antrr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) : ℚ ⟶ {Base}_{R}$
38	37 31	ffvelcdmd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (0) \in {Base}_{R}$
39	37 16	ffvelcdmd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (q) \in {Base}_{R}$
40	38 39	ovresd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) = ℚHom (R) (0) dist (R) ℚHom (R) (q)$
41		inss1	$⊢ NrmRing \cap DivRing \subseteq NrmRing$
42	41	sseli	$⊢ R \in (NrmRing \cap DivRing) \to R \in NrmRing$
43	42	3ad2ant1	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to R \in NrmRing$
44	43	ad2antrr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to R \in NrmRing$
45		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
46	44 45	syl	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to R \in NrmGrp$
47		eqid	$⊢ -_{R} = -_{R}$
48		eqid	$⊢ dist (R) = dist (R)$
49	33 9 47 48	ngpdsr	$⊢ (R \in NrmGrp \land ℚHom (R) (0) \in {Base}_{R} \land ℚHom (R) (q) \in {Base}_{R}) \to ℚHom (R) (0) dist (R) ℚHom (R) (q) = norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (0))$
50	46 38 39 49	syl3anc	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (0) dist (R) ℚHom (R) (q) = norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (0))$
51	7	ad2antrr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to R \in DivRing$
52	8	ad2antrr	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to chr (R) = 0$
53	9 10 11	qqh0	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (0) = 0_{R}$
54	51 52 53	syl2anc	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (0) = 0_{R}$
55	54	oveq2d	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (q) -_{R} ℚHom (R) (0) = ℚHom (R) (q) -_{R} 0_{R}$
56		ngpgrp	$⊢ R \in NrmGrp \to R \in Grp$
57	46 56	syl	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to R \in Grp$
58		eqid	$⊢ 0_{R} = 0_{R}$
59	9 58 47	grpsubid1	$⊢ (R \in Grp \land ℚHom (R) (q) \in {Base}_{R}) \to ℚHom (R) (q) -_{R} 0_{R} = ℚHom (R) (q)$
60	57 39 59	syl2anc	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (q) -_{R} 0_{R} = ℚHom (R) (q)$
61	55 60	eqtrd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (q) -_{R} ℚHom (R) (0) = ℚHom (R) (q)$
62	61	fveq2d	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to norm (R) (ℚHom (R) (q) -_{R} ℚHom (R) (0)) = norm (R) (ℚHom (R) (q))$
63	40 50 62	3eqtrd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) = norm (R) (ℚHom (R) (q))$
64	36 63	eqtr4d	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to 0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q = ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q)$
65	64	breq1d	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \leftrightarrow ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
66	65	biimpd	$⊢ (((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \land q \in ℚ) \to (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
67	66	ralrimiva	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \to \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
68		breq2	$⊢ d = e \to (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \leftrightarrow 0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e)$
69	68	rspceaimv	$⊢ (e \in ℝ^{+} \land \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < e \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)) \to \exists d \in ℝ^{+} \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
70	14 67 69	syl2anc	$⊢ ((R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
71	70	ralrimiva	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)$
72		cnfldxms	$⊢ ℂ_{fld} \in ∞MetSp$
73		qex	$⊢ ℚ \in V$
74		ressxms	$⊢ (ℂ_{fld} \in ∞MetSp \land ℚ \in V) \to ℂ_{fld} ↾_{𝑠} ℚ \in ∞MetSp$
75	72 73 74	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in ∞MetSp$
76	1 75	eqeltri	$⊢ Q \in ∞MetSp$
77	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
78		cnfldds	$⊢ abs \circ - = dist (ℂ_{fld})$
79	1 78	ressds	$⊢ ℚ \in V \to abs \circ - = dist (Q)$
80	73 79	ax-mp	$⊢ abs \circ - = dist (Q)$
81	77 80	xmsxmet2	$⊢ Q \in ∞MetSp \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ)$
82	76 81	mp1i	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to {(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ)$
83		ngpxms	$⊢ R \in NrmGrp \to R \in ∞MetSp$
84	42 45 83	3syl	$⊢ R \in (NrmRing \cap DivRing) \to R \in ∞MetSp$
85	84	3ad2ant1	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to R \in ∞MetSp$
86	9 48	xmsxmet2	$⊢ R \in ∞MetSp \to {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R})$
87	85 86	syl	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R})$
88	30	a1i	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to 0 \in ℚ$
89	80	reseq1i	$⊢ {(abs \circ -) ↾}_{(ℚ \times ℚ)} = {dist (Q) ↾}_{(ℚ \times ℚ)}$
90	2 77 89	xmstopn	$⊢ Q \in ∞MetSp \to J = MetOpen ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
91	76 90	ax-mp	$⊢ J = MetOpen ({(abs \circ -) ↾}_{(ℚ \times ℚ)})$
92		eqid	$⊢ MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
93	91 92	metcnp	$⊢ ({(abs \circ -) ↾}_{(ℚ \times ℚ)} \in ∞Met (ℚ) \land {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R}) \land 0 \in ℚ) \to (ℚHom (R) \in (J CnP MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})) (0) \leftrightarrow (ℚHom (R) : ℚ ⟶ {Base}_{R} \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)))$
94	82 87 88 93	syl3anc	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to (ℚHom (R) \in (J CnP MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})) (0) \leftrightarrow (ℚHom (R) : ℚ ⟶ {Base}_{R} \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall q \in ℚ (0 ({(abs \circ -) ↾}_{(ℚ \times ℚ)}) q < d \to ℚHom (R) (0) ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) ℚHom (R) (q) < e)))$
95	13 71 94	mpbir2and	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in (J CnP MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})) (0)$
96		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
97	4 9 96	xmstopn	$⊢ R \in ∞MetSp \to K = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
98	85 97	syl	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to K = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
99	98	oveq2d	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to J CnP K = J CnP MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
100	99	fveq1d	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to (J CnP K) (0) = (J CnP MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})) (0)$
101	95 100	eleqtrrd	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in (J CnP K) (0)$
102		cnfldtgp	$⊢ ℂ_{fld} \in TopGrp$
103		qsubdrg	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
104	103	simpli	$⊢ ℚ \in SubRing (ℂ_{fld})$
105		subrgsubg	$⊢ ℚ \in SubRing (ℂ_{fld}) \to ℚ \in SubGrp (ℂ_{fld})$
106	104 105	ax-mp	$⊢ ℚ \in SubGrp (ℂ_{fld})$
107	1	subgtgp	$⊢ (ℂ_{fld} \in TopGrp \land ℚ \in SubGrp (ℂ_{fld})) \to Q \in TopGrp$
108	102 106 107	mp2an	$⊢ Q \in TopGrp$
109		tgptmd	$⊢ Q \in TopGrp \to Q \in TopMnd$
110	108 109	mp1i	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to Q \in TopMnd$
111		nrgtrg	$⊢ R \in NrmRing \to R \in TopRing$
112		trgtmd2	$⊢ R \in TopRing \to R \in TopMnd$
113	43 111 112	3syl	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to R \in TopMnd$
114	9 10 11 1	qqhghm	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) \in (Q GrpHom R)$
115	7 8 114	syl2anc	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in (Q GrpHom R)$
116	77 2 4	ghmcnp	$⊢ (Q \in TopMnd \land R \in TopMnd \land ℚHom (R) \in (Q GrpHom R)) \to (ℚHom (R) \in (J CnP K) (0) \leftrightarrow (0 \in ℚ \land ℚHom (R) \in (J Cn K)))$
117	110 113 115 116	syl3anc	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to (ℚHom (R) \in (J CnP K) (0) \leftrightarrow (0 \in ℚ \land ℚHom (R) \in (J Cn K)))$
118	101 117	mpbid	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to (0 \in ℚ \land ℚHom (R) \in (J Cn K))$
119	118	simprd	$⊢ (R \in (NrmRing \cap DivRing) \land Z \in NrmMod \land chr (R) = 0) \to ℚHom (R) \in (J Cn K)$

Metamath Proof Explorer

Theorem qqhcn

Proof