Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  qqhval2 Structured version   Visualization version   Unicode version

Theorem qqhval2 28798
 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.)
Hypotheses
Ref Expression
qqhval2.0
qqhval2.1 /r
qqhval2.2 RHom
Assertion
Ref Expression
qqhval2 chr QQHom numer denom
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem qqhval2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3056 . . . 4
21adantr 467 . . 3 chr
3 qqhval2.1 . . . 4 /r
4 eqid 2453 . . . 4
5 qqhval2.2 . . . 4 RHom
63, 4, 5qqhval 28790 . . 3 QQHom Unit
72, 6syl 17 . 2 chr QQHom Unit
8 eqidd 2454 . . . 4 chr
9 qqhval2.0 . . . . 5
10 eqid 2453 . . . . 5
119, 5, 10zrhunitpreima 28794 . . . 4 chr Unit
12 mpt2eq12 6356 . . . 4 Unit Unit
138, 11, 12syl2anc 667 . . 3 chr Unit
1413rneqd 5065 . 2 chr Unit
15 nfv 1763 . . . 4 chr
16 nfab1 2596 . . . 4
17 nfcv 2594 . . . 4 numer denom
18 simpr 463 . . . . . . . . . 10 chr
19 zssq 11278 . . . . . . . . . . . 12
20 simplrl 771 . . . . . . . . . . . 12 chr
2119, 20sseldi 3432 . . . . . . . . . . 11 chr
22 simplrr 772 . . . . . . . . . . . . 13 chr
2322eldifad 3418 . . . . . . . . . . . 12 chr
2419, 23sseldi 3432 . . . . . . . . . . 11 chr
2522eldifbd 3419 . . . . . . . . . . . 12 chr
26 elsn 3984 . . . . . . . . . . . . 13
2726necon3bbii 2673 . . . . . . . . . . . 12
2825, 27sylib 200 . . . . . . . . . . 11 chr
29 qdivcl 11292 . . . . . . . . . . 11
3021, 24, 28, 29syl3anc 1269 . . . . . . . . . 10 chr
31 simplll 769 . . . . . . . . . . 11 chr
32 simpllr 770 . . . . . . . . . . 11 chr chr
339, 3, 5qqhval2lem 28797 . . . . . . . . . . . 12 chr numer denom
3433eqcomd 2459 . . . . . . . . . . 11 chr numer denom
3531, 32, 20, 23, 28, 34syl23anc 1276 . . . . . . . . . 10 chr numer denom
36 ovex 6323 . . . . . . . . . . 11
37 ovex 6323 . . . . . . . . . . 11
38 opeq12 4171 . . . . . . . . . . . . 13
3938eqeq2d 2463 . . . . . . . . . . . 12
40 simpl 459 . . . . . . . . . . . . . 14
4140eleq1d 2515 . . . . . . . . . . . . 13
42 simpr 463 . . . . . . . . . . . . . 14
4340fveq2d 5874 . . . . . . . . . . . . . . . 16 numer numer
4443fveq2d 5874 . . . . . . . . . . . . . . 15 numer numer
4540fveq2d 5874 . . . . . . . . . . . . . . . 16 denom denom
4645fveq2d 5874 . . . . . . . . . . . . . . 15 denom denom
4744, 46oveq12d 6313 . . . . . . . . . . . . . 14 numer denom numer denom
4842, 47eqeq12d 2468 . . . . . . . . . . . . 13 numer denom numer denom
4941, 48anbi12d 718 . . . . . . . . . . . 12 numer denom numer denom
5039, 49anbi12d 718 . . . . . . . . . . 11 numer denom numer denom
5136, 37, 50spc2ev 3144 . . . . . . . . . 10 numer denom numer denom
5218, 30, 35, 51syl12anc 1267 . . . . . . . . 9 chr numer denom
5352ex 436 . . . . . . . 8 chr numer denom
5453rexlimdvva 2888 . . . . . . 7 chr numer denom
5554imp 431 . . . . . 6 chr numer denom
56 19.42vv 1838 . . . . . . 7 chr numer denom chr numer denom
57 simprrl 775 . . . . . . . . . 10 chr numer denom
58 qnumcl 14701 . . . . . . . . . 10 numer
5957, 58syl 17 . . . . . . . . 9 chr numer denom numer
60 qdencl 14702 . . . . . . . . . . . 12 denom
6157, 60syl 17 . . . . . . . . . . 11 chr numer denom denom
6261nnzd 11046 . . . . . . . . . 10 chr numer denom denom
63 nnne0 10649 . . . . . . . . . . 11 denom denom
64 elsni 3995 . . . . . . . . . . . 12 denom denom
6564necon3ai 2651 . . . . . . . . . . 11 denom denom
6661, 63, 653syl 18 . . . . . . . . . 10 chr numer denom denom
6762, 66eldifd 3417 . . . . . . . . 9 chr numer denom denom
68 simprl 765 . . . . . . . . . 10 chr numer denom
69 qeqnumdivden 14707 . . . . . . . . . . . 12 numer denom
7057, 69syl 17 . . . . . . . . . . 11 chr numer denom numer denom
71 simprrr 776 . . . . . . . . . . 11 chr numer denom numer denom
7270, 71opeq12d 4177 . . . . . . . . . 10 chr numer denom numer denom numer denom
7368, 72eqtrd 2487 . . . . . . . . 9 chr numer denom numer denom numer denom
74 oveq1 6302 . . . . . . . . . . . 12 numer numer
75 fveq2 5870 . . . . . . . . . . . . 13 numer numer
7675oveq1d 6310 . . . . . . . . . . . 12 numer numer
7774, 76opeq12d 4177 . . . . . . . . . . 11 numer numer numer
7877eqeq2d 2463 . . . . . . . . . 10 numer numer numer
79 oveq2 6303 . . . . . . . . . . . 12 denom numer numer denom
80 fveq2 5870 . . . . . . . . . . . . 13 denom denom
8180oveq2d 6311 . . . . . . . . . . . 12 denom numer numer denom
8279, 81opeq12d 4177 . . . . . . . . . . 11 denom numer numer numer denom numer denom
8382eqeq2d 2463 . . . . . . . . . 10 denom numer numer numer denom numer denom
8478, 83rspc2ev 3163 . . . . . . . . 9 numer denom numer denom numer denom
8559, 67, 73, 84syl3anc 1269 . . . . . . . 8 chr numer denom
8685exlimivv 1780 . . . . . . 7 chr numer denom
8756, 86sylbir 217 . . . . . 6 chr numer denom
8855, 87impbida 844 . . . . 5 chr numer denom
89 abid 2441 . . . . 5
90 elopab 4712 . . . . 5 numer denom numer denom
9188, 89, 903bitr4g 292 . . . 4 chr numer denom
9215, 16, 17, 91eqrd 3452 . . 3 chr numer denom
93 eqid 2453 . . . 4
9493rnmpt2 6411 . . 3
95 df-mpt 4466 . . 3 numer denom numer denom
9692, 94, 953eqtr4g 2512 . 2 chr numer denom
977, 14, 963eqtrd 2491 1 chr QQHom numer denom
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 371   w3a 986   wceq 1446  wex 1665   wcel 1889  cab 2439   wne 2624  wrex 2740  cvv 3047   cdif 3403  csn 3970  cop 3976  copab 4463   cmpt 4464  ccnv 4836   crn 4838  cima 4840  cfv 5585  (class class class)co 6295   cmpt2 6297  cc0 9544   cdiv 10276  cn 10616  cz 10944  cq 11271  numercnumer 14694  denomcdenom 14695  cbs 15133  c0g 15350  cur 17747  Unitcui 17879  /rcdvr 17922  cdr 17987  RHomczrh 19083  chrcchr 19085  QQHomcqqh 28788 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-inf2 8151  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622  ax-addf 9623  ax-mulf 9624 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-tpos 6978  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7961  df-inf 7962  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-q 11272  df-rp 11310  df-fz 11792  df-fl 12035  df-mod 12104  df-seq 12221  df-exp 12280  df-cj 13174  df-re 13175  df-im 13176  df-sqrt 13310  df-abs 13311  df-dvds 14318  df-gcd 14481  df-numer 14696  df-denom 14697  df-gz 14886  df-struct 15135  df-ndx 15136  df-slot 15137  df-base 15138  df-sets 15139  df-ress 15140  df-plusg 15215  df-mulr 15216  df-starv 15217  df-tset 15221  df-ple 15222  df-ds 15224  df-unif 15225  df-0g 15352  df-mgm 16500  df-sgrp 16539  df-mnd 16549  df-mhm 16594  df-grp 16685  df-minusg 16686  df-sbg 16687  df-mulg 16688  df-subg 16826  df-ghm 16893  df-od 17184  df-cmn 17444  df-mgp 17736  df-ur 17748  df-ring 17794  df-cring 17795  df-oppr 17863  df-dvdsr 17881  df-unit 17882  df-invr 17912  df-dvr 17923  df-rnghom 17955  df-drng 17989  df-subrg 18018  df-cnfld 18983  df-zring 19052  df-zrh 19087  df-chr 19089  df-qqh 28789 This theorem is referenced by:  qqhvval  28799  qqhf  28802
 Copyright terms: Public domain W3C validator