Theorem 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 = ( CCfld |`s QQ )
	qqhucn.u	|- U = ( UnifSt ` Q )
	qqhucn.v	|- V = ( metUnif ` ( ( dist ` R ) |` ( B X. B ) ) )
	qqhucn.z	|- Z = ( ZMod ` R )
	qqhucn.1	|- ( ph -> R e. NrmRing )
	qqhucn.2	|- ( ph -> R e. DivRing )
	qqhucn.3	|- ( ph -> Z e. NrmMod )
	qqhucn.4	|- ( ph -> ( chr ` R ) = 0 )
Assertion	qqhucn	|- ( ph -> ( QQHom ` R ) e. ( U uCn V ) )

Proof

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