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 2821 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | eqid 2821 | . . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
3 | eqid 2821 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
4 | 1, 2, 3 | isdrng 19506 | . 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)}))) |
5 | 4 | simplbi 500 | 1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 ∖ cdif 3933 {csn 4567 ‘cfv 6355 Basecbs 16483 0gc0g 16713 Ringcrg 19297 Unitcui 19389 DivRingcdr 19502 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-iota 6314 df-fv 6363 df-drng 19504 |
This theorem is referenced by: drnggrp 19510 drngid 19516 drngunz 19517 drnginvrcl 19519 drnginvrn0 19520 drnginvrl 19521 drnginvrr 19522 drngmul0or 19523 sdrgid 19575 sdrgacs 19580 cntzsdrg 19581 primefld 19584 abvtriv 19612 rlmlvec 19978 drngnidl 20002 drnglpir 20026 drngnzr 20035 drngdomn 20076 mpllvec 20233 qsssubdrg 20604 frlmlvec 20905 frlmphllem 20924 frlmphl 20925 cvsdivcl 23737 qcvs 23751 cphsubrglem 23781 rrxcph 23995 rrx0 24000 drnguc1p 24764 ig1peu 24765 ig1pcl 24769 ig1pdvds 24770 ig1prsp 24771 ply1lpir 24772 padicabv 26206 ofldchr 30887 reofld 30913 rearchi 30915 xrge0slmod 30917 sradrng 30988 drgext0gsca 30994 drgextlsp 30996 rgmoddim 31008 frlmdim 31009 matdim 31013 drngdimgt0 31016 fedgmullem1 31025 fedgmullem2 31026 fedgmul 31027 fldextid 31049 extdg1id 31053 ccfldsrarelvec 31056 zrhunitpreima 31219 elzrhunit 31220 qqhval2lem 31222 qqh0 31225 qqh1 31226 qqhf 31227 qqhghm 31229 qqhrhm 31230 qqhnm 31231 qqhucn 31233 zrhre 31260 qqhre 31261 lindsdom 34901 lindsenlbs 34902 matunitlindflem1 34903 matunitlindflem2 34904 matunitlindf 34905 dvalveclem 38176 dvhlveclem 38259 hlhilsrnglem 39104 0prjspnrel 39289 drhmsubc 44371 drngcat 44372 drhmsubcALTV 44389 drngcatALTV 44390 aacllem 44922 |
Copyright terms: Public domain | W3C validator |