Metamath Proof Explorer

Theorem qqhval2

Description: Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 26-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 qqhval2.0 
 |-  B = ( Base ` R )
2 qqhval2.1 
 |-  ./ = ( /r ` R )
3 qqhval2.2 
 |-  L = ( ZRHom ` R )
4 elex 
 |-  ( R e. DivRing -> R e. _V )
5 4 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> R e. _V )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 2 6 3 qqhval 
 |-  ( R e. _V -> ( QQHom ` R ) = ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
8 5 7 syl 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) = ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
9 eqid 
 |-  ZZ = ZZ
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 1 3 10 zrhunitpreima 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) )
12 mpoeq12 
 |-  ( ( ZZ = ZZ /\ ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) ) -> ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
13 9 11 12 sylancr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
14 13 rneqd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ran ( x e. ZZ , y e. ( `' L " ( Unit ` R ) ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = ran ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
15 nfv 
 |-  F/ e ( R e. DivRing /\ ( chr ` R ) = 0 )
16 nfab1 
 |-  F/_ e { e | E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. }
17 nfcv 
 |-  F/_ e { <. q , s >. | ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) }
18 simpr 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
19 zssq 
 |-  ZZ C_ QQ
20 simplrl 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> x e. ZZ )
21 19 20 sselid 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> x e. QQ )
22 simplrr 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> y e. ( ZZ \ { 0 } ) )
23 22 eldifad 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> y e. ZZ )
24 19 23 sselid 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> y e. QQ )
25 22 eldifbd 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> -. y e. { 0 } )
26 velsn 
 |-  ( y e. { 0 } <-> y = 0 )
27 26 necon3bbii 
 |-  ( -. y e. { 0 } <-> y =/= 0 )
28 25 27 sylib 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> y =/= 0 )
29 qdivcl 
 |-  ( ( x e. QQ /\ y e. QQ /\ y =/= 0 ) -> ( x / y ) e. QQ )
30 21 24 28 29 syl3anc 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> ( x / y ) e. QQ )
31 simplll 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> R e. DivRing )
32 simpllr 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> ( chr ` R ) = 0 )
33 1 2 3 qqhval2lem 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) ) -> ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) = ( ( L ` x ) ./ ( L ` y ) ) )
34 33 eqcomd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) ) -> ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) )
35 31 32 20 23 28 34 syl23anc 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) )
36 ovex 
 |-  ( x / y ) e. _V
37 ovex 
 |-  ( ( L ` x ) ./ ( L ` y ) ) e. _V
38 opeq12 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> <. q , s >. = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
39 38 eqeq2d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( e = <. q , s >. <-> e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) )
40 simpl 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> q = ( x / y ) )
41 40 eleq1d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( q e. QQ <-> ( x / y ) e. QQ ) )
42 simpr 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> s = ( ( L ` x ) ./ ( L ` y ) ) )
43 40 fveq2d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( numer ` q ) = ( numer ` ( x / y ) ) )
44 43 fveq2d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( L ` ( numer ` q ) ) = ( L ` ( numer ` ( x / y ) ) ) )
45 40 fveq2d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( denom ` q ) = ( denom ` ( x / y ) ) )
46 45 fveq2d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( L ` ( denom ` q ) ) = ( L ` ( denom ` ( x / y ) ) ) )
47 44 46 oveq12d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) )
48 42 47 eqeq12d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) <-> ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) ) )
49 41 48 anbi12d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) <-> ( ( x / y ) e. QQ /\ ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) ) ) )
50 39 49 anbi12d 
 |-  ( ( q = ( x / y ) /\ s = ( ( L ` x ) ./ ( L ` y ) ) ) -> ( ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) <-> ( e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. /\ ( ( x / y ) e. QQ /\ ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) ) ) ) )
51 36 37 50 spc2ev 
 |-  ( ( e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. /\ ( ( x / y ) e. QQ /\ ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` ( x / y ) ) ) ./ ( L ` ( denom ` ( x / y ) ) ) ) ) ) -> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) )
52 18 30 35 51 syl12anc 
 |-  ( ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) /\ e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) )
53 52 ex 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) ) -> ( e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. -> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) )
54 53 rexlimdvva 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. -> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) )
55 54 imp 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) -> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) )
56 19.42vv 
 |-  ( E. q E. s ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) <-> ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) )
57 simprrl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> q e. QQ )
58 qnumcl 
 |-  ( q e. QQ -> ( numer ` q ) e. ZZ )
59 57 58 syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> ( numer ` q ) e. ZZ )
60 qdencl 
 |-  ( q e. QQ -> ( denom ` q ) e. NN )
61 57 60 syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> ( denom ` q ) e. NN )
62 61 nnzd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> ( denom ` q ) e. ZZ )
63 nnne0 
 |-  ( ( denom ` q ) e. NN -> ( denom ` q ) =/= 0 )
64 nelsn 
 |-  ( ( denom ` q ) =/= 0 -> -. ( denom ` q ) e. { 0 } )
65 61 63 64 3syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> -. ( denom ` q ) e. { 0 } )
66 62 65 eldifd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> ( denom ` q ) e. ( ZZ \ { 0 } ) )
67 simprl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> e = <. q , s >. )
68 qeqnumdivden 
 |-  ( q e. QQ -> q = ( ( numer ` q ) / ( denom ` q ) ) )
69 57 68 syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> q = ( ( numer ` q ) / ( denom ` q ) ) )
70 simprrr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) )
71 69 70 opeq12d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> <. q , s >. = <. ( ( numer ` q ) / ( denom ` q ) ) , ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) >. )
72 67 71 eqtrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> e = <. ( ( numer ` q ) / ( denom ` q ) ) , ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) >. )
73 oveq1 
 |-  ( x = ( numer ` q ) -> ( x / y ) = ( ( numer ` q ) / y ) )
74 fveq2 
 |-  ( x = ( numer ` q ) -> ( L ` x ) = ( L ` ( numer ` q ) ) )
75 74 oveq1d 
 |-  ( x = ( numer ` q ) -> ( ( L ` x ) ./ ( L ` y ) ) = ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) )
76 73 75 opeq12d 
 |-  ( x = ( numer ` q ) -> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. = <. ( ( numer ` q ) / y ) , ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) >. )
77 76 eqeq2d 
 |-  ( x = ( numer ` q ) -> ( e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. <-> e = <. ( ( numer ` q ) / y ) , ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) >. ) )
78 oveq2 
 |-  ( y = ( denom ` q ) -> ( ( numer ` q ) / y ) = ( ( numer ` q ) / ( denom ` q ) ) )
79 fveq2 
 |-  ( y = ( denom ` q ) -> ( L ` y ) = ( L ` ( denom ` q ) ) )
80 79 oveq2d 
 |-  ( y = ( denom ` q ) -> ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) )
81 78 80 opeq12d 
 |-  ( y = ( denom ` q ) -> <. ( ( numer ` q ) / y ) , ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) >. = <. ( ( numer ` q ) / ( denom ` q ) ) , ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) >. )
82 81 eqeq2d 
 |-  ( y = ( denom ` q ) -> ( e = <. ( ( numer ` q ) / y ) , ( ( L ` ( numer ` q ) ) ./ ( L ` y ) ) >. <-> e = <. ( ( numer ` q ) / ( denom ` q ) ) , ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) >. ) )
83 77 82 rspc2ev 
 |-  ( ( ( numer ` q ) e. ZZ /\ ( denom ` q ) e. ( ZZ \ { 0 } ) /\ e = <. ( ( numer ` q ) / ( denom ` q ) ) , ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) >. ) -> E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
84 59 66 72 83 syl3anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
85 84 exlimivv 
 |-  ( E. q E. s ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
86 56 85 sylbir 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) -> E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
87 55 86 impbida 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. <-> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) ) )
88 abid 
 |-  ( e e. { e | E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. } <-> E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
89 elopab 
 |-  ( e e. { <. q , s >. | ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) } <-> E. q E. s ( e = <. q , s >. /\ ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) ) )
90 87 88 89 3bitr4g 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( e e. { e | E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. } <-> e e. { <. q , s >. | ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) } ) )
91 15 16 17 90 eqrd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> { e | E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. } = { <. q , s >. | ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) } )
92 eqid 
 |-  ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. )
93 92 rnmpo 
 |-  ran ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = { e | E. x e. ZZ E. y e. ( ZZ \ { 0 } ) e = <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. }
94 df-mpt 
 |-  ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) = { <. q , s >. | ( q e. QQ /\ s = ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) }
95 91 93 94 3eqtr4g 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ran ( x e. ZZ , y e. ( ZZ \ { 0 } ) |-> <. ( x / y ) , ( ( L ` x ) ./ ( L ` y ) ) >. ) = ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) )
96 8 14 95 3eqtrd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) = ( q e. QQ |-> ( ( L ` ( numer ` q ) ) ./ ( L ` ( denom ` q ) ) ) ) )