Metamath Proof Explorer

Theorem qqhghm

Description: The QQHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-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 qqhghm 
|- ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( Q GrpHom 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 qex 
 |-  QQ e. _V
7 cnfldadd 
 |-  + = ( +g ` CCfld )
8 4 7 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
9 6 8 ax-mp 
 |-  + = ( +g ` Q )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 4 qdrng 
 |-  Q e. DivRing
12 drnggrp 
 |-  ( Q e. DivRing -> Q e. Grp )
13 11 12 mp1i 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> Q e. Grp )
14 drnggrp 
 |-  ( R e. DivRing -> R e. Grp )
15 14 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> R e. Grp )
16 1 2 3 qqhf 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) : QQ --> B )
17 drngring 
 |-  ( R e. DivRing -> R e. Ring )
18 17 ad2antrr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> R e. Ring )
19 17 adantr 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> R e. Ring )
20 3 zrhrhm 
 |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )
21 zringbas 
 |-  ZZ = ( Base ` ZZring )
22 21 1 rhmf 
 |-  ( L e. ( ZZring RingHom R ) -> L : ZZ --> B )
23 19 20 22 3syl 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> L : ZZ --> B )
24 23 adantr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L : ZZ --> B )
25 qnumcl 
 |-  ( x e. QQ -> ( numer ` x ) e. ZZ )
26 25 ad2antrl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` x ) e. ZZ )
27 qdencl 
 |-  ( y e. QQ -> ( denom ` y ) e. NN )
28 27 ad2antll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. NN )
29 28 nnzd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. ZZ )
30 26 29 zmulcld 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( numer ` x ) x. ( denom ` y ) ) e. ZZ )
31 24 30 ffvelrnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) e. B )
32 qnumcl 
 |-  ( y e. QQ -> ( numer ` y ) e. ZZ )
33 32 ad2antll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` y ) e. ZZ )
34 qdencl 
 |-  ( x e. QQ -> ( denom ` x ) e. NN )
35 34 ad2antrl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. NN )
36 35 nnzd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. ZZ )
37 33 36 zmulcld 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( numer ` y ) x. ( denom ` x ) ) e. ZZ )
38 24 37 ffvelrnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) e. B )
39 18 20 syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L e. ( ZZring RingHom R ) )
40 zringmulr 
 |-  x. = ( .r ` ZZring )
41 eqid 
 |-  ( .r ` R ) = ( .r ` R )
42 21 40 41 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 ) ) ) )
43 39 36 29 42 syl3anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) = ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) )
44 simpl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( R e. DivRing /\ ( chr ` R ) = 0 ) )
45 35 nnne0d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) =/= 0 )
46 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
47 1 3 46 elzrhunit 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( denom ` x ) e. ZZ /\ ( denom ` x ) =/= 0 ) ) -> ( L ` ( denom ` x ) ) e. ( Unit ` R ) )
48 44 36 45 47 syl12anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( denom ` x ) ) e. ( Unit ` R ) )
49 28 nnne0d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) =/= 0 )
50 1 3 46 elzrhunit 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( ( denom ` y ) e. ZZ /\ ( denom ` y ) =/= 0 ) ) -> ( L ` ( denom ` y ) ) e. ( Unit ` R ) )
51 44 29 49 50 syl12anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( denom ` y ) ) e. ( Unit ` R ) )
52 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
53 52 41 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 ) )
54 18 48 51 53 syl3anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( L ` ( denom ` x ) ) ( .r ` R ) ( L ` ( denom ` y ) ) ) e. ( Unit ` R ) )
55 43 54 eqeltrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) e. ( Unit ` R ) )
56 1 52 10 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 ) ) ) ) ) )
57 18 31 38 55 56 syl13anc 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) ) )
58 qeqnumdivden 
 |-  ( x e. QQ -> x = ( ( numer ` x ) / ( denom ` x ) ) )
59 58 ad2antrl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> x = ( ( numer ` x ) / ( denom ` x ) ) )
60 qeqnumdivden 
 |-  ( y e. QQ -> y = ( ( numer ` y ) / ( denom ` y ) ) )
61 60 ad2antll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> y = ( ( numer ` y ) / ( denom ` y ) ) )
62 59 61 oveq12d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) = ( ( ( numer ` x ) / ( denom ` x ) ) + ( ( numer ` y ) / ( denom ` y ) ) ) )
63 26 zcnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` x ) e. CC )
64 36 zcnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` x ) e. CC )
65 33 zcnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( numer ` y ) e. CC )
66 29 zcnd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( denom ` y ) e. CC )
67 63 64 65 66 45 49 divadddivd 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) )
68 62 67 eqtrd 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) )
69 68 fveq2d 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
70 30 37 zaddcld 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( ( numer ` x ) x. ( denom ` y ) ) + ( ( numer ` y ) x. ( denom ` x ) ) ) e. ZZ )
71 36 29 zmulcld 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) e. ZZ )
72 64 66 45 49 mulne0d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) =/= 0 )
73 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 ) ) ) ) )
74 44 70 71 72 73 syl13anc 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
75 rhmghm 
 |-  ( L e. ( ZZring RingHom R ) -> L e. ( ZZring GrpHom R ) )
76 39 75 syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> L e. ( ZZring GrpHom R ) )
77 zringplusg 
 |-  + = ( +g ` ZZring )
78 21 77 10 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 ) ) ) ) )
79 78 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 ) ) ) ) )
80 76 30 37 79 syl3anc 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
81 69 74 80 3eqtrd 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
82 58 fveq2d 
 |-  ( x e. QQ -> ( ( QQHom ` R ) ` x ) = ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) )
83 82 ad2antrl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` x ) = ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) )
84 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 ) ) ) )
85 44 26 36 45 84 syl13anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( numer ` x ) / ( denom ` x ) ) ) = ( ( L ` ( numer ` x ) ) ./ ( L ` ( denom ` x ) ) ) )
86 52 21 2 40 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 ) ) ) ) )
87 39 26 36 29 48 51 86 syl132anc 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
88 83 85 87 3eqtrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` x ) = ( ( L ` ( ( numer ` x ) x. ( denom ` y ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
89 60 fveq2d 
 |-  ( y e. QQ -> ( ( QQHom ` R ) ` y ) = ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) )
90 89 ad2antll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` y ) = ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) )
91 52 21 2 40 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 ) ) ) ) )
92 39 33 29 36 51 48 91 syl132anc 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
93 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 ) ) ) )
94 44 33 29 49 93 syl13anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( ( numer ` y ) / ( denom ` y ) ) ) = ( ( L ` ( numer ` y ) ) ./ ( L ` ( denom ` y ) ) ) )
95 64 66 mulcomd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( denom ` x ) x. ( denom ` y ) ) = ( ( denom ` y ) x. ( denom ` x ) ) )
96 95 fveq2d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) = ( L ` ( ( denom ` y ) x. ( denom ` x ) ) ) )
97 96 oveq2d 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
98 92 94 97 3eqtr4d 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) )
99 90 98 eqtrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` y ) = ( ( L ` ( ( numer ` y ) x. ( denom ` x ) ) ) ./ ( L ` ( ( denom ` x ) x. ( denom ` y ) ) ) ) )
100 88 99 oveq12d 
 |-  ( ( ( R e. DivRing /\ ( 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 ) ) ) ) ) )
101 57 81 100 3eqtr4d 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( QQHom ` R ) ` ( x + y ) ) = ( ( ( QQHom ` R ) ` x ) ( +g ` R ) ( ( QQHom ` R ) ` y ) ) )
102 5 1 9 10 13 15 16 101 isghmd 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( QQHom ` R ) e. ( Q GrpHom R ) )