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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qqhcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑄 )
qqhcn.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
qqhcn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
Assertion qqhcn ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

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