| 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 2737 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 2 | eqid 2737 | . . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅) | |
| 3 | eqid 2737 | . . 3 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
| 4 | 1, 2, 3 | isdrng 20733 | . 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)}))) |
| 5 | 4 | simplbi 497 | 1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ∖ cdif 3948 {csn 4626 ‘cfv 6561 Basecbs 17247 0gc0g 17484 Ringcrg 20230 Unitcui 20355 DivRingcdr 20729 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-drng 20731 |
| This theorem is referenced by: drngringd 20737 drngid 20746 drngunz 20747 drngnzr 20748 drngdomn 20749 drngmcl 20750 drnginvrcl 20753 drnginvrn0 20754 drnginvrl 20756 drnginvrr 20757 drngmul0orOLD 20761 drhmsubc 20782 drngcat 20783 sdrgid 20793 sdrgacs 20802 cntzsdrg 20803 primefld 20806 rlmlvec 21211 drngnidl 21253 drnglpir 21342 qsssubdrg 21444 frlmlvec 21781 frlmphllem 21800 mpllvec 22040 cvsdivcl 25166 qcvs 25181 cphsubrglem 25211 rrxcph 25426 rrx0 25431 drnguc1p 26213 ig1peu 26214 ig1pcl 26218 ig1pdvds 26219 ig1prsp 26220 ply1lpir 26221 padicabv 27674 ofldchr 33344 reofld 33372 rearchi 33374 xrge0slmod 33376 drng0mxidl 33504 drngmxidl 33505 zringfrac 33582 sradrng 33633 drgext0gsca 33642 drgextlsp 33644 rlmdim 33660 rgmoddimOLD 33661 frlmdim 33662 matdim 33666 drngdimgt0 33669 fedgmullem1 33680 fedgmullem2 33681 fedgmul 33682 fldextid 33710 extdg1id 33716 ccfldsrarelvec 33721 zrhunitpreima 33977 elzrhunit 33978 qqhval2lem 33982 qqh0 33985 qqh1 33986 qqhf 33987 qqhghm 33989 qqhrhm 33990 qqhnm 33991 qqhucn 33993 zrhre 34020 qqhre 34021 lindsdom 37621 lindsenlbs 37622 matunitlindflem1 37623 matunitlindflem2 37624 matunitlindf 37625 dvalveclem 41027 dvhlveclem 41110 hlhilsrnglem 41959 fldhmf1 42091 ricdrng1 42538 0prjspnrel 42637 drhmsubcALTV 48245 drngcatALTV 48246 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |