Metamath Proof Explorer

Theorem qqhcn

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

Ref Expression
Hypotheses qqhcn.q 
|- Q = ( CCfld |`s QQ )
qqhcn.j 
|- J = ( TopOpen ` Q )
qqhcn.z 
|- Z = ( ZMod ` R )
qqhcn.k 
|- K = ( TopOpen ` R )
Assertion qqhcn 
|- ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( J Cn K ) )

Proof

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