Metamath Proof Explorer

Theorem qqh0

Description: The image of 0 by the QQHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses qqhval2.0 
|- B = ( Base ` R )
qqhval2.1 
|- ./ = ( /r ` R )
qqhval2.2 
|- L = ( ZRHom ` R )
Assertion qqh0 
|- ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 0 ) = ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 
 |-  B = ( Base ` R )
2 qqhval2.1 
 |-  ./ = ( /r ` R )
3 qqhval2.2 
 |-  L = ( ZRHom ` R )
4 zssq 
 |-  ZZ C_ QQ
5 0z 
 |-  0 e. ZZ
6 4 5 sselii 
 |-  0 e. QQ
7 1 2 3 qqhvval 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ 0 e. QQ ) -> ( ( QQHom ` R ) ` 0 ) = ( ( L ` ( numer ` 0 ) ) ./ ( L ` ( denom ` 0 ) ) ) )
8 6 7 mpan2 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 0 ) = ( ( L ` ( numer ` 0 ) ) ./ ( L ` ( denom ` 0 ) ) ) )
9 1z 
 |-  1 e. ZZ
10 gcd0id 
 |-  ( 1 e. ZZ -> ( 0 gcd 1 ) = ( abs ` 1 ) )
11 9 10 ax-mp 
 |-  ( 0 gcd 1 ) = ( abs ` 1 )
12 abs1 
 |-  ( abs ` 1 ) = 1
13 11 12 eqtri 
 |-  ( 0 gcd 1 ) = 1
14 0cn 
 |-  0 e. CC
15 14 div1i 
 |-  ( 0 / 1 ) = 0
16 15 eqcomi 
 |-  0 = ( 0 / 1 )
17 13 16 pm3.2i 
 |-  ( ( 0 gcd 1 ) = 1 /\ 0 = ( 0 / 1 ) )
18 1nn 
 |-  1 e. NN
19 qnumdenbi 
 |-  ( ( 0 e. QQ /\ 0 e. ZZ /\ 1 e. NN ) -> ( ( ( 0 gcd 1 ) = 1 /\ 0 = ( 0 / 1 ) ) <-> ( ( numer ` 0 ) = 0 /\ ( denom ` 0 ) = 1 ) ) )
20 6 5 18 19 mp3an 
 |-  ( ( ( 0 gcd 1 ) = 1 /\ 0 = ( 0 / 1 ) ) <-> ( ( numer ` 0 ) = 0 /\ ( denom ` 0 ) = 1 ) )
21 17 20 mpbi 
 |-  ( ( numer ` 0 ) = 0 /\ ( denom ` 0 ) = 1 )
22 21 simpli 
 |-  ( numer ` 0 ) = 0
23 22 fveq2i 
 |-  ( L ` ( numer ` 0 ) ) = ( L ` 0 )
24 21 simpri 
 |-  ( denom ` 0 ) = 1
25 24 fveq2i 
 |-  ( L ` ( denom ` 0 ) ) = ( L ` 1 )
26 23 25 oveq12i 
 |-  ( ( L ` ( numer ` 0 ) ) ./ ( L ` ( denom ` 0 ) ) ) = ( ( L ` 0 ) ./ ( L ` 1 ) )
27 drngring 
 |-  ( R e. DivRing -> R e. Ring )
28 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
29 3 28 zrh0 
 |-  ( R e. Ring -> ( L ` 0 ) = ( 0g ` R ) )
30 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
31 3 30 zrh1 
 |-  ( R e. Ring -> ( L ` 1 ) = ( 1r ` R ) )
32 29 31 oveq12d 
 |-  ( R e. Ring -> ( ( L ` 0 ) ./ ( L ` 1 ) ) = ( ( 0g ` R ) ./ ( 1r ` R ) ) )
33 27 32 syl 
 |-  ( R e. DivRing -> ( ( L ` 0 ) ./ ( L ` 1 ) ) = ( ( 0g ` R ) ./ ( 1r ` R ) ) )
34 drnggrp 
 |-  ( R e. DivRing -> R e. Grp )
35 1 28 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. B )
36 34 35 syl 
 |-  ( R e. DivRing -> ( 0g ` R ) e. B )
37 1 2 30 dvr1 
 |-  ( ( R e. Ring /\ ( 0g ` R ) e. B ) -> ( ( 0g ` R ) ./ ( 1r ` R ) ) = ( 0g ` R ) )
38 27 36 37 syl2anc 
 |-  ( R e. DivRing -> ( ( 0g ` R ) ./ ( 1r ` R ) ) = ( 0g ` R ) )
39 33 38 eqtrd 
 |-  ( R e. DivRing -> ( ( L ` 0 ) ./ ( L ` 1 ) ) = ( 0g ` R ) )
40 26 39 syl5eq 
 |-  ( R e. DivRing -> ( ( L ` ( numer ` 0 ) ) ./ ( L ` ( denom ` 0 ) ) ) = ( 0g ` R ) )
41 40 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( L ` ( numer ` 0 ) ) ./ ( L ` ( denom ` 0 ) ) ) = ( 0g ` R ) )
42 8 41 eqtrd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 0 ) = ( 0g ` R ) )