MPE Home 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  |-  DivRingOps  =  { <. g ,  h >.  |  ( <. g ,  h >.  e.  RingOps  /\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  GrpOp ) }
Distinct variable group:    g, h

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