Metamath Proof Explorer

Theorem qqhrhm

Description: The QQHom homomorphism is a ring homomorphism if the target structure is a field. If the target structure is a division ring, it is a group homomorphism, but not a ring homomorphism, because it does not preserve the ring multiplication operation. (Contributed by Thierry Arnoux, 29-Oct-2017)

Ref Expression
Hypotheses qqhval2.0 
|- B = ( Base ` R )
qqhval2.1 
|- ./ = ( /r ` R )
qqhval2.2 
|- L = ( ZRHom ` R )
qqhrhm.1 
|- Q = ( CCfld |`s QQ )
Assertion qqhrhm 
|- ( ( R e. Field /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( Q RingHom R ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 
 |-  B = ( Base ` R )
2 qqhval2.1 
 |-  ./ = ( /r ` R )
3 qqhval2.2 
 |-  L = ( ZRHom ` R )
4 qqhrhm.1 
 |-  Q = ( CCfld |`s QQ )
5 4 qrngbas 
 |-  QQ = ( Base ` Q )
6 4 qrng1 
 |-  1 = ( 1r ` Q )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 qex 
 |-  QQ e. _V
9 cnfldmul 
 |-  x. = ( .r ` CCfld )
10 4 9 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
11 8 10 ax-mp 
 |-  x. = ( .r ` Q )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 4 qdrng 
 |-  Q e. DivRing
14 drngring 
 |-  ( Q e. DivRing -> Q e. Ring )
15 13 14 mp1i 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> Q e. Ring )
16 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
17 16 simplbi 
 |-  ( R e. Field -> R e. DivRing )
18 17 adantr 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> R e. DivRing )
19 drngring 
 |-  ( R e. DivRing -> R e. Ring )
20 18 19 syl 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> R e. Ring )
21 1 2 3 qqh1 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 1 ) = ( 1r ` R ) )
22 17 21 sylan 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 1 ) = ( 1r ` R ) )
23 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
24 eqid 
 |-  ( +g ` R ) = ( +g ` R )
25 16 simprbi 
 |-  ( R e. Field -> R e. CRing )
26 25 ad2antrr 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> R e. CRing )
27 3 zrhrhm 
 |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )
28 zringbas 
 |-  ZZ = ( Base ` ZZring )
29 28 1 rhmf 
 |-  ( L e. ( ZZring RingHom R ) -> L : ZZ --> B )
30 20 27 29 3syl 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> L : ZZ --> B )
31 30 adantr 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L : ZZ --> B )
32 qnumcl 
 |-  ( x e. QQ -> ( numer ` x ) e. ZZ )
33 32 ad2antrl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` x ) e. ZZ )
34 31 33 ffvelrnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( numer ` x ) ) e. B )
35 17 ad2antrr 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> R e. DivRing )
36 simplr 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( chr ` R ) = 0 )
37 35 36 jca 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( R e. DivRing /\ ( chr ` R ) = 0 ) )
38 qdencl 
 |-  ( x e. QQ -> ( denom ` x ) e. NN )
39 38 ad2antrl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. NN )
40 39 nnzd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. ZZ )
41 39 nnne0d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) =/= 0 )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 1 3 42 elzrhunit 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( denom ` x ) e. ZZ /\ ( denom ` x ) =/= 0 ) ) -> ( L ` ( denom ` x ) ) e. ( Unit ` R ) )
44 37 40 41 43 syl12anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( denom ` x ) ) e. ( Unit ` R ) )
45 qnumcl 
 |-  ( y e. QQ -> ( numer ` y ) e. ZZ )
46 45 ad2antll 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` y ) e. ZZ )
47 31 46 ffvelrnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( numer ` y ) ) e. B )
48 qdencl 
 |-  ( y e. QQ -> ( denom ` y ) e. NN )
49 48 ad2antll 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. NN )
50 49 nnzd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. ZZ )
51 49 nnne0d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) =/= 0 )
52 1 3 42 elzrhunit 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( denom ` y ) e. ZZ /\ ( denom ` y ) =/= 0 ) ) -> ( L ` ( denom ` y ) ) e. ( Unit ` R ) )
53 37 50 51 52 syl12anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( denom ` y ) ) e. ( Unit ` R ) )
54 1 23 24 2 12 26 34 44 47 53 rdivmuldivd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) ( .r ` R ) ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) ) = ( ( ( L ` ( numer ` x ) ) ( .r ` R ) ( L ` ( numer ` y ) ) ) ./ ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) ) )
55 qeqnumdivden 
 |-  ( x e. QQ -> x = ( ( numer ` x ) / ( denom ` x ) ) )
56 55 fveq2d 
 |-  ( x e. QQ -> ( ( QQHom ` R ) ` x ) = ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) )
57 56 ad2antrl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` x ) = ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) )
58 1 2 3 qqhvq 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( numer ` x ) e. ZZ /\ ( denom ` x ) e. ZZ /\ ( denom ` x ) =/= 0 ) ) -> ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) = ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) )
59 37 33 40 41 58 syl13anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) = ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) )
60 57 59 eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` x ) = ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) )
61 qeqnumdivden 
 |-  ( y e. QQ -> y = ( ( numer ` y ) / ( denom ` y ) ) )
62 61 fveq2d 
 |-  ( y e. QQ -> ( ( QQHom ` R ) ` y ) = ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) )
63 62 ad2antll 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` y ) = ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) )
64 1 2 3 qqhvq 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( numer ` y ) e. ZZ /\ ( denom ` y ) e. ZZ /\ ( denom ` y ) =/= 0 ) ) -> ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) )
65 37 46 50 51 64 syl13anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) )
66 63 65 eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` y ) = ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) )
67 60 66 oveq12d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( QQHom ` R ) ` x ) ( .r ` R ) ( ( QQHom ` R ) ` y ) ) = ( ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) ( .r ` R ) ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) ) )
68 55 ad2antrl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> x = ( ( numer ` x ) / ( denom ` x ) ) )
69 61 ad2antll 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> y = ( ( numer ` y ) / ( denom ` y ) ) )
70 68 69 oveq12d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x x. y ) = ( ( ( numer ` x ) / ( denom ` x ) ) x. ( ( numer ` y ) / ( denom ` y ) ) ) )
71 33 zcnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` x ) e. CC )
72 40 zcnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. CC )
73 46 zcnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` y ) e. CC )
74 50 zcnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. CC )
75 71 72 73 74 41 51 divmuldivd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( numer ` x ) / ( denom ` x ) ) x. ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( ( numer ` x ) x. ( numer ` y ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) )
76 70 75 eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x x. y ) = ( ( ( numer ` x ) x. ( numer ` y ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) )
77 76 fveq2d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x x. y ) ) = ( ( QQHom ` R ) ` ( ( ( numer ` x ) x. ( numer ` y ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
78 33 46 zmulcld 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( numer ` x ) x. ( numer ` y ) ) e. ZZ )
79 40 50 zmulcld 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) e. ZZ )
80 72 74 41 51 mulne0d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) =/= 0 )
81 1 2 3 qqhvq 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( ( numer ` x ) x. ( numer ` y ) ) e. ZZ /\ ( ( denom ` x ) x. ( denom ` y ) ) e. ZZ /\ ( ( denom ` x ) x. ( denom ` y ) ) =/= 0 ) ) -> ( ( QQHom ` R ) ` ( ( ( numer ` x ) x. ( numer ` y ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( L ` ( ( numer ` x ) x. ( numer ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
82 37 78 79 80 81 syl13anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( ( numer ` x ) x. ( numer ` y ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( L ` ( ( numer ` x ) x. ( numer ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
83 35 19 syl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> R e. Ring )
84 83 27 syl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L e. ( ZZring RingHom R ) )
85 zringmulr 
 |-  x. = ( .r ` ZZring )
86 28 85 12 rhmmul 
 |-  ( ( L e. ( ZZring RingHom R ) /\ ( numer ` x ) e. ZZ /\ ( numer ` y ) e. ZZ ) -> ( L ` ( ( numer ` x ) x. ( numer ` y ) ) ) = ( ( L ` ( numer ` x ) ) ( .r ` R ) ( L ` ( numer ` y ) ) ) )
87 84 33 46 86 syl3anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( numer ` x ) x. ( numer ` y ) ) ) = ( ( L ` ( numer ` x ) ) ( .r ` R ) ( L ` ( numer ` y ) ) ) )
88 28 85 12 rhmmul 
 |-  ( ( L e. ( ZZring RingHom R ) /\ ( denom ` x ) e. ZZ /\ ( denom ` y ) e. ZZ ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) = ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) )
89 84 40 50 88 syl3anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) = ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) )
90 87 89 oveq12d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( ( numer ` x ) x. ( numer ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( ( L ` ( numer ` x ) ) ( .r ` R ) ( L ` ( numer ` y ) ) ) ./ ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) ) )
91 77 82 90 3eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x x. y ) ) = ( ( ( L ` ( numer ` x ) ) ( .r ` R ) ( L ` ( numer ` y ) ) ) ./ ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) ) )
92 54 67 91 3eqtr4rd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x x. y ) ) = ( ( ( QQHom ` R ) ` x ) ( .r ` R ) ( ( QQHom ` R ) ` y ) ) )
93 cnfldadd 
 |-  + = ( +g ` CCfld )
94 4 93 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
95 8 94 ax-mp 
 |-  + = ( +g ` Q )
96 1 2 3 qqhf 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) : QQ --> B )
97 17 96 sylan 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) : QQ --> B )
98 33 50 zmulcld 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( numer ` x ) x. ( denom ` y ) ) e. ZZ )
99 31 98 ffvelrnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) e. B )
100 46 40 zmulcld 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( numer ` y ) x. ( denom ` x ) ) e. ZZ )
101 31 100 ffvelrnd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) e. B )
102 23 12 unitmulcl 
 |-  ( ( R e. Ring /\ ( L ` ( denom ` x ) ) e. ( Unit ` R ) /\ ( L ` ( denom ` y ) ) e. ( Unit ` R ) ) -> ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) e. ( Unit ` R ) )
103 83 44 53 102 syl3anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) e. ( Unit ` R ) )
104 89 103 eqeltrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) e. ( Unit ` R ) )
105 1 23 24 2 dvrdir 
 |-  ( ( R e. Ring /\ ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) e. B /\ ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) e. B /\ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) e. ( Unit ` R ) ) ) -> ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ( +g ` R ) ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ) )
106 83 99 101 104 105 syl13anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ( +g ` R ) ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ) )
107 68 69 oveq12d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) = ( ( ( numer ` x ) / ( denom ` x ) ) + ( ( numer ` y ) / ( denom ` y ) ) ) )
108 71 72 73 74 41 51 divadddivd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( numer ` x ) / ( denom ` x ) ) + ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) )
109 107 108 eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) = ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) )
110 109 fveq2d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x + y ) ) = ( ( QQHom ` R ) ` ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
111 98 100 zaddcld 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) e. ZZ )
112 1 2 3 qqhvq 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) e. ZZ /\ ( ( denom ` x ) x. ( denom ` y ) ) e. ZZ /\ ( ( denom ` x ) x. ( denom ` y ) ) =/= 0 ) ) -> ( ( QQHom ` R ) ` ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( L ` ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
113 37 111 79 80 112 syl13anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) / ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( L ` ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
114 rhmghm 
 |-  ( L e. ( ZZring RingHom R ) -> L e. ( ZZring GrpHom R ) )
115 84 114 syl 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L e. ( ZZring GrpHom R ) )
116 zringplusg 
 |-  + = ( +g ` ZZring )
117 28 116 24 ghmlin 
 |-  ( ( L e. ( ZZring GrpHom R ) /\ ( ( numer ` x ) x. ( denom ` y ) ) e. ZZ /\ ( ( numer ` y ) x. ( denom ` x ) ) e. ZZ ) -> ( L ` ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) ) = ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) )
118 117 oveq1d 
 |-  ( ( L e. ( ZZring GrpHom R ) /\ ( ( numer ` x ) x. ( denom ` y ) ) e. ZZ /\ ( ( numer ` y ) x. ( denom ` x ) ) e. ZZ ) -> ( ( L ` ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
119 115 98 100 118 syl3anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
120 110 113 119 3eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x + y ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ( +g ` R ) ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
121 23 28 2 85 rhmdvd 
 |-  ( ( L e. ( ZZring RingHom R ) /\ ( ( numer ` x ) e. ZZ /\ ( denom ` x ) e. ZZ /\ ( denom ` y ) e. ZZ ) /\ ( ( L ` ( denom ` x ) ) e. ( Unit ` R ) /\ ( L ` ( denom ` y ) ) e. ( Unit ` R ) ) ) -> ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) = ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
122 84 33 40 50 44 53 121 syl132anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) = ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
123 57 59 122 3eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` x ) = ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
124 23 28 2 85 rhmdvd 
 |-  ( ( L e. ( ZZring RingHom R ) /\ ( ( numer ` y ) e. ZZ /\ ( denom ` y ) e. ZZ /\ ( denom ` x ) e. ZZ ) /\ ( ( L ` ( denom ` y ) ) e. ( Unit ` R ) /\ ( L ` ( denom ` x ) ) e. ( Unit ` R ) ) ) -> ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` y ) x. ( denom ` x ) ) ) ) )
125 84 46 50 40 53 44 124 syl132anc 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` y ) x. ( denom ` x ) ) ) ) )
126 72 74 mulcomd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) = ( ( denom ` y ) x. ( denom ` x ) ) )
127 126 fveq2d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) = ( L ` ( ( denom ` y ) x. ( denom ` x ) ) ) )
128 127 oveq2d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` y ) x. ( denom ` x ) ) ) ) )
129 125 65 128 3eqtr4d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
130 63 129 eqtrd 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` y ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
131 123 130 oveq12d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( QQHom ` R ) ` x ) ( +g ` R ) ( ( QQHom ` R ) ` y ) ) = ( ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ( +g ` R ) ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) ) )
132 106 120 131 3eqtr4d 
 |-  ( ( ( R e. Field /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x + y ) ) = ( ( ( QQHom ` R ) ` x ) ( +g ` R ) ( ( QQHom ` R ) ` y ) ) )
133 5 6 7 11 12 15 20 22 92 1 95 24 97 132 isrhmd 
 |-  ( ( R e. Field /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( Q RingHom R ) )