![]() |
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 2732 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | eqid 2732 | . . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
3 | eqid 2732 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
4 | 1, 2, 3 | isdrng 20311 | . 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)}))) |
5 | 4 | simplbi 498 | 1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ∖ cdif 3944 {csn 4627 ‘cfv 6540 Basecbs 17140 0gc0g 17381 Ringcrg 20049 Unitcui 20161 DivRingcdr 20307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-drng 20309 |
This theorem is referenced by: drngringd 20315 drngid 20325 drngunz 20326 drngnzr 20327 drnginvrcl 20329 drnginvrn0 20330 drnginvrl 20332 drnginvrr 20333 drngmul0or 20336 sdrgid 20400 sdrgacs 20409 cntzsdrg 20410 primefld 20413 abvtriv 20441 rlmlvec 20820 drngnidl 20846 drnglpir 20883 drngdomn 20913 qsssubdrg 20996 frlmlvec 21307 frlmphllem 21326 mpllvec 21570 cvsdivcl 24640 qcvs 24655 cphsubrglem 24685 rrxcph 24900 rrx0 24905 drnguc1p 25679 ig1peu 25680 ig1pcl 25684 ig1pdvds 25685 ig1prsp 25686 ply1lpir 25687 padicabv 27122 ofldchr 32420 reofld 32447 rearchi 32449 xrge0slmod 32451 drng0mxidl 32580 drngmxidl 32581 sradrng 32661 drgext0gsca 32667 drgextlsp 32669 rlmdim 32682 rgmoddimOLD 32683 frlmdim 32684 matdim 32688 drngdimgt0 32691 fedgmullem1 32702 fedgmullem2 32703 fedgmul 32704 fldextid 32726 extdg1id 32730 ccfldsrarelvec 32733 zrhunitpreima 32946 elzrhunit 32947 qqhval2lem 32949 qqh0 32952 qqh1 32953 qqhf 32954 qqhghm 32956 qqhrhm 32957 qqhnm 32958 qqhucn 32960 zrhre 32987 qqhre 32988 lindsdom 36470 lindsenlbs 36471 matunitlindflem1 36472 matunitlindflem2 36473 matunitlindf 36474 dvalveclem 39884 dvhlveclem 39967 hlhilsrnglem 40816 fldhmf1 40943 ricdrng1 41099 0prjspnrel 41365 drhmsubc 46931 drngcat 46932 drhmsubcALTV 46949 drngcatALTV 46950 aacllem 47801 |
Copyright terms: Public domain | W3C validator |