Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > drngring | Structured version Visualization version GIF version |
Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011.) |
Ref | Expression |
---|---|
drngring | ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2818 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | eqid 2818 | . . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
3 | eqid 2818 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
4 | 1, 2, 3 | isdrng 19435 | . 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)}))) |
5 | 4 | simplbi 498 | 1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∖ cdif 3930 {csn 4557 ‘cfv 6348 Basecbs 16471 0gc0g 16701 Ringcrg 19226 Unitcui 19318 DivRingcdr 19431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-drng 19433 |
This theorem is referenced by: drnggrp 19439 drngid 19445 drngunz 19446 drnginvrcl 19448 drnginvrn0 19449 drnginvrl 19450 drnginvrr 19451 drngmul0or 19452 sdrgid 19504 sdrgacs 19509 cntzsdrg 19510 primefld 19513 abvtriv 19541 rlmlvec 19907 drngnidl 19930 drnglpir 19954 drngnzr 19963 drngdomn 20004 mpllvec 20161 qsssubdrg 20532 frlmlvec 20833 frlmphllem 20852 frlmphl 20853 cvsdivcl 23664 qcvs 23678 cphsubrglem 23708 rrxcph 23922 rrx0 23927 drnguc1p 24691 ig1peu 24692 ig1pcl 24696 ig1pdvds 24697 ig1prsp 24698 ply1lpir 24699 padicabv 26133 ofldchr 30814 reofld 30840 rearchi 30842 xrge0slmod 30844 sradrng 30887 drgext0gsca 30893 drgextlsp 30895 rgmoddim 30907 frlmdim 30908 matdim 30912 drngdimgt0 30915 fedgmullem1 30924 fedgmullem2 30925 fedgmul 30926 fldextid 30948 extdg1id 30952 ccfldsrarelvec 30955 zrhunitpreima 31118 elzrhunit 31119 qqhval2lem 31121 qqh0 31124 qqh1 31125 qqhf 31126 qqhghm 31128 qqhrhm 31129 qqhnm 31130 qqhucn 31132 zrhre 31159 qqhre 31160 lindsdom 34767 lindsenlbs 34768 matunitlindflem1 34769 matunitlindflem2 34770 matunitlindf 34771 dvalveclem 38041 dvhlveclem 38124 hlhilsrnglem 38969 0prjspnrel 39147 drhmsubc 44279 drngcat 44280 drhmsubcALTV 44297 drngcatALTV 44298 aacllem 44830 |
Copyright terms: Public domain | W3C validator |