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 
|- N = ( norm ` R )
qqhnm.z 
|- Z = ( ZMod ` R )
Assertion qqhnm 
|- ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( QQHom ` R ) ` Q ) ) = ( abs ` Q ) )

Proof

Step Hyp Ref Expression
1 qqhnm.n 
 |-  N = ( norm ` R )
2 qqhnm.z 
 |-  Z = ( ZMod ` R )
3 simpr 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> Q e. QQ )
4 qeqnumdivden 
 |-  ( Q e. QQ -> Q = ( ( numer ` Q ) / ( denom ` Q ) ) )
5 4 fveq2d 
 |-  ( Q e. QQ -> ( abs ` Q ) = ( abs ` ( ( numer ` Q ) / ( denom ` Q ) ) ) )
6 3 5 syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( abs ` Q ) = ( abs ` ( ( numer ` Q ) / ( denom ` Q ) ) ) )
7 qnumcl 
 |-  ( Q e. QQ -> ( numer ` Q ) e. ZZ )
8 3 7 syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( numer ` Q ) e. ZZ )
9 8 zcnd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( numer ` Q ) e. CC )
10 qdencl 
 |-  ( Q e. QQ -> ( denom ` Q ) e. NN )
11 3 10 syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( denom ` Q ) e. NN )
12 11 nncnd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( denom ` Q ) e. CC )
13 nnne0 
 |-  ( ( denom ` Q ) e. NN -> ( denom ` Q ) =/= 0 )
14 3 10 13 3syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( denom ` Q ) =/= 0 )
15 9 12 14 absdivd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( abs ` ( ( numer ` Q ) / ( denom ` Q ) ) ) = ( ( abs ` ( numer ` Q ) ) / ( abs ` ( denom ` Q ) ) ) )
16 inss2 
 |-  ( NrmRing i^i DivRing ) C_ DivRing
17 simpl1 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> R e. ( NrmRing i^i DivRing ) )
18 16 17 sselid 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> R e. DivRing )
19 simpl3 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( chr ` R ) = 0 )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 eqid 
 |-  ( /r ` R ) = ( /r ` R )
22 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
23 20 21 22 qqhvval 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( QQHom ` R ) ` Q ) = ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) ( /r ` R ) ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) )
24 23 fveq2d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( QQHom ` R ) ` Q ) ) = ( N ` ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) ( /r ` R ) ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) )
25 18 19 3 24 syl21anc 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( QQHom ` R ) ` Q ) ) = ( N ` ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) ( /r ` R ) ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) )
26 inss1 
 |-  ( NrmRing i^i DivRing ) C_ NrmRing
27 26 17 sselid 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> R e. NrmRing )
28 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
29 18 28 syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> R e. NzRing )
30 drngring 
 |-  ( R e. DivRing -> R e. Ring )
31 22 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
32 zringbas 
 |-  ZZ = ( Base ` ZZring )
33 32 20 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
34 18 30 31 33 4syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
35 34 8 ffvelrnd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( ZRHom ` R ) ` ( numer ` Q ) ) e. ( Base ` R ) )
36 11 nnzd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( denom ` Q ) e. ZZ )
37 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
38 20 22 37 elzrhunit 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( denom ` Q ) e. ZZ /\ ( denom ` Q ) =/= 0 ) ) -> ( ( ZRHom ` R ) ` ( denom ` Q ) ) e. ( Unit ` R ) )
39 18 19 36 14 38 syl22anc 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( ZRHom ` R ) ` ( denom ` Q ) ) e. ( Unit ` R ) )
40 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
41 20 1 40 21 nmdvr 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) e. ( Base ` R ) /\ ( ( ZRHom ` R ) ` ( denom ` Q ) ) e. ( Unit ` R ) ) ) -> ( N ` ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) ( /r ` R ) ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) = ( ( N ` ( ( ZRHom ` R ) ` ( numer ` Q ) ) ) / ( N ` ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) )
42 27 29 35 39 41 syl22anc 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( ( ZRHom ` R ) ` ( numer ` Q ) ) ( /r ` R ) ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) = ( ( N ` ( ( ZRHom ` R ) ` ( numer ` Q ) ) ) / ( N ` ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) )
43 simpl2 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> Z e. NrmMod )
44 2 zhmnrg 
 |-  ( R e. NrmRing -> Z e. NrmRing )
45 27 44 syl 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> Z e. NrmRing )
46 20 1 2 22 zrhnm 
 |-  ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ ( numer ` Q ) e. ZZ ) -> ( N ` ( ( ZRHom ` R ) ` ( numer ` Q ) ) ) = ( abs ` ( numer ` Q ) ) )
47 43 45 29 8 46 syl31anc 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( ZRHom ` R ) ` ( numer ` Q ) ) ) = ( abs ` ( numer ` Q ) ) )
48 20 1 2 22 zrhnm 
 |-  ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ ( denom ` Q ) e. ZZ ) -> ( N ` ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) = ( abs ` ( denom ` Q ) ) )
49 43 45 29 36 48 syl31anc 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) = ( abs ` ( denom ` Q ) ) )
50 47 49 oveq12d 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( N ` ( ( ZRHom ` R ) ` ( numer ` Q ) ) ) / ( N ` ( ( ZRHom ` R ) ` ( denom ` Q ) ) ) ) = ( ( abs ` ( numer ` Q ) ) / ( abs ` ( denom ` Q ) ) ) )
51 25 42 50 3eqtrrd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( ( abs ` ( numer ` Q ) ) / ( abs ` ( denom ` Q ) ) ) = ( N ` ( ( QQHom ` R ) ` Q ) ) )
52 6 15 51 3eqtrrd 
 |-  ( ( ( R e. ( NrmRing i^i DivRing ) /\ Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ Q e. QQ ) -> ( N ` ( ( QQHom ` R ) ` Q ) ) = ( abs ` Q ) )