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

Definition df-drngo 21073
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 21072 . 2  class  DivRingOps
2 vg . . . . . . 7  set  g
32cv 1622 . . . . . 6  class  g
4 vh . . . . . . 7  set  h
54cv 1622 . . . . . 6  class  h
63, 5cop 3643 . . . . 5  class  <. g ,  h >.
7 crngo 21042 . . . . 5  class  RingOps
86, 7wcel 1684 . . . 4  wff  <. g ,  h >.  e.  RingOps
93crn 4690 . . . . . . . 8  class  ran  g
10 cgi 20854 . . . . . . . . . 10  class GId
113, 10cfv 5255 . . . . . . . . 9  class  (GId `  g )
1211csn 3640 . . . . . . . 8  class  { (GId
`  g ) }
139, 12cdif 3149 . . . . . . 7  class  ( ran  g  \  { (GId
`  g ) } )
1413, 13cxp 4687 . . . . . 6  class  ( ( ran  g  \  {
(GId `  g ) } )  X.  ( ran  g  \  { (GId
`  g ) } ) )
155, 14cres 4691 . . . . 5  class  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )
16 cgr 20853 . . . . 5  class  GrpOp
1715, 16wcel 1684 . . . 4  wff  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  GrpOp
188, 17wa 358 . . 3  wff  ( <.
g ,  h >.  e.  RingOps 
/\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  GrpOp )
1918, 2, 4copab 4076 . 2  class  { <. g ,  h >.  |  (
<. g ,  h >.  e.  RingOps 
/\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  GrpOp ) }
201, 19wceq 1623 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  21074  isdivrngo  21098  isdrngo1  26587
  Copyright terms: Public domain W3C validator