Metamath Proof Explorer

Theorem qqhnm

Description: The norm of the image by QQHom of a rational number in a topological division ring. (Contributed by Thierry Arnoux, 8-Nov-2017)

Ref Expression
Hypotheses qqhnm.n ⊢ 𝑁 = ( norm ‘ 𝑅 )
qqhnm.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
Assertion qqhnm ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) ) = ( abs ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 qqhnm.n ⊢ 𝑁 = ( norm ‘ 𝑅 )
2 qqhnm.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
3 simpr ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑄 ∈ ℚ )
4 qeqnumdivden ⊢ ( 𝑄 ∈ ℚ → 𝑄 = ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) )
5 4 fveq2d ⊢ ( 𝑄 ∈ ℚ → ( abs ‘ 𝑄 ) = ( abs ‘ ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) ) )
6 3 5 syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( abs ‘ 𝑄 ) = ( abs ‘ ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) ) )
7 qnumcl ⊢ ( 𝑄 ∈ ℚ → ( numer ‘ 𝑄 ) ∈ ℤ )
8 3 7 syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( numer ‘ 𝑄 ) ∈ ℤ )
9 8 zcnd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( numer ‘ 𝑄 ) ∈ ℂ )
10 qdencl ⊢ ( 𝑄 ∈ ℚ → ( denom ‘ 𝑄 ) ∈ ℕ )
11 3 10 syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( denom ‘ 𝑄 ) ∈ ℕ )
12 11 nncnd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( denom ‘ 𝑄 ) ∈ ℂ )
13 nnne0 ⊢ ( ( denom ‘ 𝑄 ) ∈ ℕ → ( denom ‘ 𝑄 ) ≠ 0 )
14 3 10 13 3syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( denom ‘ 𝑄 ) ≠ 0 )
15 9 12 14 absdivd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( abs ‘ ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) ) = ( ( abs ‘ ( numer ‘ 𝑄 ) ) / ( abs ‘ ( denom ‘ 𝑄 ) ) ) )
16 inss2 ⊢ ( NrmRing ∩ DivRing ) ⊆ DivRing
17 simpl1 ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑅 ∈ ( NrmRing ∩ DivRing ) )
18 16 17 sselid ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑅 ∈ DivRing )
19 simpl3 ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( chr ‘ 𝑅 ) = 0 )
20 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 eqid ⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
22 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
23 20 21 22 qqhvval ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ( /r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) )
24 23 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) ) = ( 𝑁 ‘ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ( /r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) )
25 18 19 3 24 syl21anc ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) ) = ( 𝑁 ‘ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ( /r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) )
26 inss1 ⊢ ( NrmRing ∩ DivRing ) ⊆ NrmRing
27 26 17 sselid ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑅 ∈ NrmRing )
28 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
29 18 28 syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑅 ∈ NzRing )
30 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
31 22 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
32 zringbas ⊢ ℤ = ( Base ‘ ℤring )
33 32 20 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
34 18 30 31 33 4syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
35 34 8 ffvelrnd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) )
36 11 nnzd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( denom ‘ 𝑄 ) ∈ ℤ )
37 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
38 20 22 37 elzrhunit ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( ( denom ‘ 𝑄 ) ∈ ℤ ∧ ( denom ‘ 𝑄 ) ≠ 0 ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ∈ ( Unit ‘ 𝑅 ) )
39 18 19 36 14 38 syl22anc ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ∈ ( Unit ‘ 𝑅 ) )
40 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
41 20 1 40 21 nmdvr ⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑁 ‘ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ( /r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) = ( ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ) / ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) )
42 27 29 35 39 41 syl22anc ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ( /r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) = ( ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ) / ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) )
43 simpl2 ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑍 ∈ NrmMod )
44 2 zhmnrg ⊢ ( 𝑅 ∈ NrmRing → 𝑍 ∈ NrmRing )
45 27 44 syl ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → 𝑍 ∈ NrmRing )
46 20 1 2 22 zrhnm ⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( numer ‘ 𝑄 ) ∈ ℤ ) → ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ) = ( abs ‘ ( numer ‘ 𝑄 ) ) )
47 43 45 29 8 46 syl31anc ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ) = ( abs ‘ ( numer ‘ 𝑄 ) ) )
48 20 1 2 22 zrhnm ⊢ ( ( ( 𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( denom ‘ 𝑄 ) ∈ ℤ ) → ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) = ( abs ‘ ( denom ‘ 𝑄 ) ) )
49 43 45 29 36 48 syl31anc ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) = ( abs ‘ ( denom ‘ 𝑄 ) ) )
50 47 49 oveq12d ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( numer ‘ 𝑄 ) ) ) / ( 𝑁 ‘ ( ( ℤRHom ‘ 𝑅 ) ‘ ( denom ‘ 𝑄 ) ) ) ) = ( ( abs ‘ ( numer ‘ 𝑄 ) ) / ( abs ‘ ( denom ‘ 𝑄 ) ) ) )
51 25 42 50 3eqtrrd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( ( abs ‘ ( numer ‘ 𝑄 ) ) / ( abs ‘ ( denom ‘ 𝑄 ) ) ) = ( 𝑁 ‘ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) ) )
52 6 15 51 3eqtrrd ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 𝑄 ∈ ℚ ) → ( 𝑁 ‘ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑄 ) ) = ( abs ‘ 𝑄 ) )