Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-drngo Structured version   Unicode version

Definition df-drngo 21994
 Description: Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-drngo GId GId
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-drngo
StepHypRef Expression
1 cdrng 21993 . 2
2 vg . . . . . . 7
32cv 1651 . . . . . 6
4 vh . . . . . . 7
54cv 1651 . . . . . 6
63, 5cop 3817 . . . . 5
7 crngo 21963 . . . . 5
86, 7wcel 1725 . . . 4
93crn 4879 . . . . . . . 8
10 cgi 21775 . . . . . . . . . 10 GId
113, 10cfv 5454 . . . . . . . . 9 GId
1211csn 3814 . . . . . . . 8 GId
139, 12cdif 3317 . . . . . . 7 GId
1413, 13cxp 4876 . . . . . 6 GId GId
155, 14cres 4880 . . . . 5 GId GId
16 cgr 21774 . . . . 5
1715, 16wcel 1725 . . . 4 GId GId
188, 17wa 359 . . 3 GId GId
1918, 2, 4copab 4265 . 2 GId GId
201, 19wceq 1652 1 GId GId
 Colors of variables: wff set class This definition is referenced by:  drngoi  21995  isdivrngo  22019  isdrngo1  26572
 Copyright terms: Public domain W3C validator