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

Definition df-drngo 26134
 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 26133 . 2
2 vg . . . . . . 7
32cv 1443 . . . . . 6
4 vh . . . . . . 7
54cv 1443 . . . . . 6
63, 5cop 3974 . . . . 5
7 crngo 26103 . . . . 5
86, 7wcel 1887 . . . 4
93crn 4835 . . . . . . . 8
10 cgi 25915 . . . . . . . . . 10 GId
113, 10cfv 5582 . . . . . . . . 9 GId
1211csn 3968 . . . . . . . 8 GId
139, 12cdif 3401 . . . . . . 7 GId
1413, 13cxp 4832 . . . . . 6 GId GId
155, 14cres 4836 . . . . 5 GId GId
16 cgr 25914 . . . . 5
1715, 16wcel 1887 . . . 4 GId GId
188, 17wa 371 . . 3 GId GId
1918, 2, 4copab 4460 . 2 GId GId
201, 19wceq 1444 1 GId GId
 Colors of variables: wff setvar class This definition is referenced by:  drngoi  26135  isdivrngo  26159  isdrngo1  32195
 Copyright terms: Public domain W3C validator