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=BaseR
qqhval2.1 ×˙=/rR
qqhval2.2 L=ℤRHomR
qqhrhm.1 Q=fld𝑠
Assertion qqhghm RDivRingchrR=0ℚHomRQGrpHomR

Proof

Step Hyp Ref Expression
1 qqhval2.0 B=BaseR
2 qqhval2.1 ×˙=/rR
3 qqhval2.2 L=ℤRHomR
4 qqhrhm.1 Q=fld𝑠
5 4 qrngbas =BaseQ
6 qex V
7 cnfldadd +=+fld
8 4 7 ressplusg V+=+Q
9 6 8 ax-mp +=+Q
10 eqid +R=+R
11 4 qdrng QDivRing
12 drnggrp QDivRingQGrp
13 11 12 mp1i RDivRingchrR=0QGrp
14 drnggrp RDivRingRGrp
15 14 adantr RDivRingchrR=0RGrp
16 1 2 3 qqhf RDivRingchrR=0ℚHomR:B
17 drngring RDivRingRRing
18 17 ad2antrr RDivRingchrR=0xyRRing
19 17 adantr RDivRingchrR=0RRing
20 3 zrhrhm RRingLringRingHomR
21 zringbas =Basering
22 21 1 rhmf LringRingHomRL:B
23 19 20 22 3syl RDivRingchrR=0L:B
24 23 adantr RDivRingchrR=0xyL:B
25 qnumcl xnumerx
26 25 ad2antrl RDivRingchrR=0xynumerx
27 qdencl ydenomy
28 27 ad2antll RDivRingchrR=0xydenomy
29 28 nnzd RDivRingchrR=0xydenomy
30 26 29 zmulcld RDivRingchrR=0xynumerxdenomy
31 24 30 ffvelrnd RDivRingchrR=0xyLnumerxdenomyB
32 qnumcl ynumery
33 32 ad2antll RDivRingchrR=0xynumery
34 qdencl xdenomx
35 34 ad2antrl RDivRingchrR=0xydenomx
36 35 nnzd RDivRingchrR=0xydenomx
37 33 36 zmulcld RDivRingchrR=0xynumerydenomx
38 24 37 ffvelrnd RDivRingchrR=0xyLnumerydenomxB
39 18 20 syl RDivRingchrR=0xyLringRingHomR
40 zringmulr ×=ring
41 eqid R=R
42 21 40 41 rhmmul LringRingHomRdenomxdenomyLdenomxdenomy=LdenomxRLdenomy
43 39 36 29 42 syl3anc RDivRingchrR=0xyLdenomxdenomy=LdenomxRLdenomy
44 simpl RDivRingchrR=0xyRDivRingchrR=0
45 35 nnne0d RDivRingchrR=0xydenomx0
46 eqid 0R=0R
47 1 3 46 elzrhunit RDivRingchrR=0denomxdenomx0LdenomxUnitR
48 44 36 45 47 syl12anc RDivRingchrR=0xyLdenomxUnitR
49 28 nnne0d RDivRingchrR=0xydenomy0
50 1 3 46 elzrhunit RDivRingchrR=0denomydenomy0LdenomyUnitR
51 44 29 49 50 syl12anc RDivRingchrR=0xyLdenomyUnitR
52 eqid UnitR=UnitR
53 52 41 unitmulcl RRingLdenomxUnitRLdenomyUnitRLdenomxRLdenomyUnitR
54 18 48 51 53 syl3anc RDivRingchrR=0xyLdenomxRLdenomyUnitR
55 43 54 eqeltrd RDivRingchrR=0xyLdenomxdenomyUnitR
56 1 52 10 2 dvrdir RRingLnumerxdenomyBLnumerydenomxBLdenomxdenomyUnitRLnumerxdenomy+RLnumerydenomx×˙Ldenomxdenomy=Lnumerxdenomy×˙Ldenomxdenomy+RLnumerydenomx×˙Ldenomxdenomy
57 18 31 38 55 56 syl13anc RDivRingchrR=0xyLnumerxdenomy+RLnumerydenomx×˙Ldenomxdenomy=Lnumerxdenomy×˙Ldenomxdenomy+RLnumerydenomx×˙Ldenomxdenomy
58 qeqnumdivden xx=numerxdenomx
59 58 ad2antrl RDivRingchrR=0xyx=numerxdenomx
60 qeqnumdivden yy=numerydenomy
61 60 ad2antll RDivRingchrR=0xyy=numerydenomy
62 59 61 oveq12d RDivRingchrR=0xyx+y=numerxdenomx+numerydenomy
63 26 zcnd RDivRingchrR=0xynumerx
64 36 zcnd RDivRingchrR=0xydenomx
65 33 zcnd RDivRingchrR=0xynumery
66 29 zcnd RDivRingchrR=0xydenomy
67 63 64 65 66 45 49 divadddivd RDivRingchrR=0xynumerxdenomx+numerydenomy=numerxdenomy+numerydenomxdenomxdenomy
68 62 67 eqtrd RDivRingchrR=0xyx+y=numerxdenomy+numerydenomxdenomxdenomy
69 68 fveq2d RDivRingchrR=0xyℚHomRx+y=ℚHomRnumerxdenomy+numerydenomxdenomxdenomy
70 30 37 zaddcld RDivRingchrR=0xynumerxdenomy+numerydenomx
71 36 29 zmulcld RDivRingchrR=0xydenomxdenomy
72 64 66 45 49 mulne0d RDivRingchrR=0xydenomxdenomy0
73 1 2 3 qqhvq RDivRingchrR=0numerxdenomy+numerydenomxdenomxdenomydenomxdenomy0ℚHomRnumerxdenomy+numerydenomxdenomxdenomy=Lnumerxdenomy+numerydenomx×˙Ldenomxdenomy
74 44 70 71 72 73 syl13anc RDivRingchrR=0xyℚHomRnumerxdenomy+numerydenomxdenomxdenomy=Lnumerxdenomy+numerydenomx×˙Ldenomxdenomy
75 rhmghm LringRingHomRLringGrpHomR
76 39 75 syl RDivRingchrR=0xyLringGrpHomR
77 zringplusg +=+ring
78 21 77 10 ghmlin LringGrpHomRnumerxdenomynumerydenomxLnumerxdenomy+numerydenomx=Lnumerxdenomy+RLnumerydenomx
79 78 oveq1d LringGrpHomRnumerxdenomynumerydenomxLnumerxdenomy+numerydenomx×˙Ldenomxdenomy=Lnumerxdenomy+RLnumerydenomx×˙Ldenomxdenomy
80 76 30 37 79 syl3anc RDivRingchrR=0xyLnumerxdenomy+numerydenomx×˙Ldenomxdenomy=Lnumerxdenomy+RLnumerydenomx×˙Ldenomxdenomy
81 69 74 80 3eqtrd RDivRingchrR=0xyℚHomRx+y=Lnumerxdenomy+RLnumerydenomx×˙Ldenomxdenomy
82 58 fveq2d xℚHomRx=ℚHomRnumerxdenomx
83 82 ad2antrl RDivRingchrR=0xyℚHomRx=ℚHomRnumerxdenomx
84 1 2 3 qqhvq RDivRingchrR=0numerxdenomxdenomx0ℚHomRnumerxdenomx=Lnumerx×˙Ldenomx
85 44 26 36 45 84 syl13anc RDivRingchrR=0xyℚHomRnumerxdenomx=Lnumerx×˙Ldenomx
86 52 21 2 40 rhmdvd LringRingHomRnumerxdenomxdenomyLdenomxUnitRLdenomyUnitRLnumerx×˙Ldenomx=Lnumerxdenomy×˙Ldenomxdenomy
87 39 26 36 29 48 51 86 syl132anc RDivRingchrR=0xyLnumerx×˙Ldenomx=Lnumerxdenomy×˙Ldenomxdenomy
88 83 85 87 3eqtrd RDivRingchrR=0xyℚHomRx=Lnumerxdenomy×˙Ldenomxdenomy
89 60 fveq2d yℚHomRy=ℚHomRnumerydenomy
90 89 ad2antll RDivRingchrR=0xyℚHomRy=ℚHomRnumerydenomy
91 52 21 2 40 rhmdvd LringRingHomRnumerydenomydenomxLdenomyUnitRLdenomxUnitRLnumery×˙Ldenomy=Lnumerydenomx×˙Ldenomydenomx
92 39 33 29 36 51 48 91 syl132anc RDivRingchrR=0xyLnumery×˙Ldenomy=Lnumerydenomx×˙Ldenomydenomx
93 1 2 3 qqhvq RDivRingchrR=0numerydenomydenomy0ℚHomRnumerydenomy=Lnumery×˙Ldenomy
94 44 33 29 49 93 syl13anc RDivRingchrR=0xyℚHomRnumerydenomy=Lnumery×˙Ldenomy
95 64 66 mulcomd RDivRingchrR=0xydenomxdenomy=denomydenomx
96 95 fveq2d RDivRingchrR=0xyLdenomxdenomy=Ldenomydenomx
97 96 oveq2d RDivRingchrR=0xyLnumerydenomx×˙Ldenomxdenomy=Lnumerydenomx×˙Ldenomydenomx
98 92 94 97 3eqtr4d RDivRingchrR=0xyℚHomRnumerydenomy=Lnumerydenomx×˙Ldenomxdenomy
99 90 98 eqtrd RDivRingchrR=0xyℚHomRy=Lnumerydenomx×˙Ldenomxdenomy
100 88 99 oveq12d RDivRingchrR=0xyℚHomRx+RℚHomRy=Lnumerxdenomy×˙Ldenomxdenomy+RLnumerydenomx×˙Ldenomxdenomy
101 57 81 100 3eqtr4d RDivRingchrR=0xyℚHomRx+y=ℚHomRx+RℚHomRy
102 5 1 9 10 13 15 16 101 isghmd RDivRingchrR=0ℚHomRQGrpHomR