![]() |
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 2651 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | eqid 2651 | . . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
3 | eqid 2651 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
4 | 1, 2, 3 | isdrng 18799 | . 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)}))) |
5 | 4 | simplbi 475 | 1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 ∖ cdif 3604 {csn 4210 ‘cfv 5926 Basecbs 15904 0gc0g 16147 Ringcrg 18593 Unitcui 18685 DivRingcdr 18795 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-drng 18797 |
This theorem is referenced by: drnggrp 18803 drngid 18809 drngunz 18810 drnginvrcl 18812 drnginvrn0 18813 drnginvrl 18814 drnginvrr 18815 drngmul0or 18816 abvtriv 18889 rlmlvec 19254 drngnidl 19277 drnglpir 19301 drngnzr 19310 drngdomn 19351 qsssubdrg 19853 frlmphllem 20167 frlmphl 20168 cvsdivcl 22979 qcvs 22993 cphsubrglem 23023 rrxcph 23226 drnguc1p 23975 ig1peu 23976 ig1pcl 23980 ig1pdvds 23981 ig1prsp 23982 ply1lpir 23983 padicabv 25364 ofldchr 29942 reofld 29968 rearchi 29970 xrge0slmod 29972 zrhunitpreima 30150 elzrhunit 30151 qqhval2lem 30153 qqh0 30156 qqh1 30157 qqhf 30158 qqhghm 30160 qqhrhm 30161 qqhnm 30162 qqhucn 30164 zrhre 30191 qqhre 30192 lindsdom 33533 lindsenlbs 33534 matunitlindflem1 33535 matunitlindflem2 33536 matunitlindf 33537 dvalveclem 36631 dvhlveclem 36714 hlhilsrnglem 37562 sdrgacs 38088 cntzsdrg 38089 drhmsubc 42405 drngcat 42406 drhmsubcALTV 42423 drngcatALTV 42424 aacllem 42875 |
Copyright terms: Public domain | W3C validator |