Metamath Proof Explorer

Theorem qqh1

Description: The image of 1 by the QQHom homomorphism is the ring's unit. (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 qqh1 
|- ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 1 ) = ( 1r ` 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 1z 
 |-  1 e. ZZ
6 4 5 sselii 
 |-  1 e. QQ
7 1 2 3 qqhvval 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ 1 e. QQ ) -> ( ( QQHom ` R ) ` 1 ) = ( ( L ` ( numer ` 1 ) ) ./ ( L ` ( denom ` 1 ) ) ) )
8 6 7 mpan2 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 1 ) = ( ( L ` ( numer ` 1 ) ) ./ ( L ` ( denom ` 1 ) ) ) )
9 gcd1 
 |-  ( 1 e. ZZ -> ( 1 gcd 1 ) = 1 )
10 5 9 ax-mp 
 |-  ( 1 gcd 1 ) = 1
11 1div1e1 
 |-  ( 1 / 1 ) = 1
12 11 eqcomi 
 |-  1 = ( 1 / 1 )
13 10 12 pm3.2i 
 |-  ( ( 1 gcd 1 ) = 1 /\ 1 = ( 1 / 1 ) )
14 1nn 
 |-  1 e. NN
15 qnumdenbi 
 |-  ( ( 1 e. QQ /\ 1 e. ZZ /\ 1 e. NN ) -> ( ( ( 1 gcd 1 ) = 1 /\ 1 = ( 1 / 1 ) ) <-> ( ( numer ` 1 ) = 1 /\ ( denom ` 1 ) = 1 ) ) )
16 6 5 14 15 mp3an 
 |-  ( ( ( 1 gcd 1 ) = 1 /\ 1 = ( 1 / 1 ) ) <-> ( ( numer ` 1 ) = 1 /\ ( denom ` 1 ) = 1 ) )
17 13 16 mpbi 
 |-  ( ( numer ` 1 ) = 1 /\ ( denom ` 1 ) = 1 )
18 17 simpli 
 |-  ( numer ` 1 ) = 1
19 18 fveq2i 
 |-  ( L ` ( numer ` 1 ) ) = ( L ` 1 )
20 17 simpri 
 |-  ( denom ` 1 ) = 1
21 20 fveq2i 
 |-  ( L ` ( denom ` 1 ) ) = ( L ` 1 )
22 19 21 oveq12i 
 |-  ( ( L ` ( numer ` 1 ) ) ./ ( L ` ( denom ` 1 ) ) ) = ( ( L ` 1 ) ./ ( L ` 1 ) )
23 drngring 
 |-  ( R e. DivRing -> R e. Ring )
24 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
25 3 24 zrh1 
 |-  ( R e. Ring -> ( L ` 1 ) = ( 1r ` R ) )
26 25 25 oveq12d 
 |-  ( R e. Ring -> ( ( L ` 1 ) ./ ( L ` 1 ) ) = ( ( 1r ` R ) ./ ( 1r ` R ) ) )
27 23 26 syl 
 |-  ( R e. DivRing -> ( ( L ` 1 ) ./ ( L ` 1 ) ) = ( ( 1r ` R ) ./ ( 1r ` R ) ) )
28 1 24 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
29 1 2 24 dvr1 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. B ) -> ( ( 1r ` R ) ./ ( 1r ` R ) ) = ( 1r ` R ) )
30 23 28 29 syl2anc2 
 |-  ( R e. DivRing -> ( ( 1r ` R ) ./ ( 1r ` R ) ) = ( 1r ` R ) )
31 27 30 eqtrd 
 |-  ( R e. DivRing -> ( ( L ` 1 ) ./ ( L ` 1 ) ) = ( 1r ` R ) )
32 22 31 syl5eq 
 |-  ( R e. DivRing -> ( ( L ` ( numer ` 1 ) ) ./ ( L ` ( denom ` 1 ) ) ) = ( 1r ` R ) )
33 32 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( L ` ( numer ` 1 ) ) ./ ( L ` ( denom ` 1 ) ) ) = ( 1r ` R ) )
34 8 33 eqtrd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 1 ) = ( 1r ` R ) )