Metamath Proof Explorer

Theorem qqhf

Description: QQHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 qqhval2.0 
 |-  B = ( Base ` R )
2 qqhval2.1 
 |-  ./ = ( /r ` R )
3 qqhval2.2 
 |-  L = ( ZRHom ` R )
4 1 2 3 qqhval2 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) = ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 5 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> R e. Ring )
7 6 adantr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> R e. Ring )
8 3 zrhrhm 
 |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )
9 zringbas 
 |-  ZZ = ( Base ` ZZring )
10 9 1 rhmf 
 |-  ( L e. ( ZZring RingHom R ) -> L : ZZ --> B )
11 7 8 10 3syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> L : ZZ --> B )
12 qnumcl 
 |-  ( q e. QQ -> ( numer ` q ) e. ZZ )
13 12 adantl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( numer ` q ) e. ZZ )
14 11 13 ffvelrnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( L ` ( numer ` q ) ) e. B )
15 simpll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> R e. DivRing )
16 qdencl 
 |-  ( q e. QQ -> ( denom ` q ) e. NN )
17 16 adantl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( denom ` q ) e. NN )
18 17 nnzd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( denom ` q ) e. ZZ )
19 11 18 ffvelrnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( L ` ( denom ` q ) ) e. B )
20 17 nnne0d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( denom ` q ) =/= 0 )
21 20 neneqd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> -. ( denom ` q ) = 0 )
22 fvex 
 |-  ( denom ` q ) e. _V
23 22 elsn 
 |-  ( ( denom ` q ) e. { 0 } <-> ( denom ` q ) = 0 )
24 21 23 sylnibr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> -. ( denom ` q ) e. { 0 } )
25 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
26 1 3 25 zrhker 
 |-  ( R e. Ring -> ( ( chr ` R ) = 0 <-> ( `' L " { ( 0g ` R ) } ) = { 0 } ) )
27 26 biimpa 
 |-  ( ( R e. Ring /\ ( chr ` R ) = 0 ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )
28 5 27 sylan 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )
29 28 adantr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )
30 24 29 neleqtrrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> -. ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) )
31 ffn 
 |-  ( L : ZZ --> B -> L Fn ZZ )
32 8 10 31 3syl 
 |-  ( R e. Ring -> L Fn ZZ )
33 elpreima 
 |-  ( L Fn ZZ -> ( ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) <-> ( ( denom ` q ) e. ZZ /\ ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } ) ) )
34 5 32 33 3syl 
 |-  ( R e. DivRing -> ( ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) <-> ( ( denom ` q ) e. ZZ /\ ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } ) ) )
35 34 biimpar 
 |-  ( ( R e. DivRing /\ ( ( denom ` q ) e. ZZ /\ ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } ) ) -> ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) )
36 35 expr 
 |-  ( ( R e. DivRing /\ ( denom ` q ) e. ZZ ) -> ( ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } -> ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) ) )
37 36 con3dimp 
 |-  ( ( ( R e. DivRing /\ ( denom ` q ) e. ZZ ) /\ -. ( denom ` q ) e. ( `' L " { ( 0g ` R ) } ) ) -> -. ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } )
38 15 18 30 37 syl21anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> -. ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } )
39 fvex 
 |-  ( L ` ( denom ` q ) ) e. _V
40 39 elsn 
 |-  ( ( L ` ( denom ` q ) ) e. { ( 0g ` R ) } <-> ( L ` ( denom ` q ) ) = ( 0g ` R ) )
41 38 40 sylnib 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> -. ( L ` ( denom ` q ) ) = ( 0g ` R ) )
42 41 neqned 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( L ` ( denom ` q ) ) =/= ( 0g ` R ) )
43 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
44 1 43 25 drngunit 
 |-  ( R e. DivRing -> ( ( L ` ( denom ` q ) ) e. ( Unit ` R ) <-> ( ( L ` ( denom ` q ) ) e. B /\ ( L ` ( denom ` q ) ) =/= ( 0g ` R ) ) ) )
45 44 biimpar 
 |-  ( ( R e. DivRing /\ ( ( L ` ( denom ` q ) ) e. B /\ ( L ` ( denom ` q ) ) =/= ( 0g ` R ) ) ) -> ( L ` ( denom ` q ) ) e. ( Unit ` R ) )
46 15 19 42 45 syl12anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( L ` ( denom ` q ) ) e. ( Unit ` R ) )
47 1 43 2 dvrcl 
 |-  ( ( R e. Ring /\ ( L ` ( numer ` q ) ) e. B /\ ( L ` ( denom ` q ) ) e. ( Unit ` R ) ) -> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) e. B )
48 7 14 46 47 syl3anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ q e. QQ ) -> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) e. B )
49 4 48 fmpt3d 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) : QQ --> B )