Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sdrg Unicode version

Definition df-sdrg 27607
Description: A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.)
Assertion
Ref Expression
df-sdrg  |- SubDRing  =  ( w  e.  DivRing  |->  { s  e.  (SubRing `  w
)  |  ( ws  s )  e.  DivRing } )
Distinct variable group:    w, s

Detailed syntax breakdown of Definition df-sdrg
StepHypRef Expression
1 csdrg 27606 . 2  class SubDRing
2 vw . . 3  set  w
3 cdr 15528 . . 3  class  DivRing
42cv 1631 . . . . . 6  class  w
5 vs . . . . . . 7  set  s
65cv 1631 . . . . . 6  class  s
7 cress 13165 . . . . . 6  classs
84, 6, 7co 5874 . . . . 5  class  ( ws  s )
98, 3wcel 1696 . . . 4  wff  ( ws  s )  e.  DivRing
10 csubrg 15557 . . . . 5  class SubRing
114, 10cfv 5271 . . . 4  class  (SubRing `  w
)
129, 5, 11crab 2560 . . 3  class  { s  e.  (SubRing `  w
)  |  ( ws  s )  e.  DivRing }
132, 3, 12cmpt 4093 . 2  class  ( w  e.  DivRing  |->  { s  e.  (SubRing `  w )  |  ( ws  s )  e.  DivRing } )
141, 13wceq 1632 1  wff SubDRing  =  ( w  e.  DivRing  |->  { s  e.  (SubRing `  w
)  |  ( ws  s )  e.  DivRing } )
Colors of variables: wff set class
This definition is referenced by:  issdrg  27608
  Copyright terms: Public domain W3C validator