Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-drngo Structured version   Visualization version   GIF version

Definition df-drngo 33878
 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 = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
Distinct variable group:   𝑔,

Detailed syntax breakdown of Definition df-drngo
StepHypRef Expression
1 cdrng 33877 . 2 class DivRingOps
2 vg . . . . . . 7 setvar 𝑔
32cv 1522 . . . . . 6 class 𝑔
4 vh . . . . . . 7 setvar
54cv 1522 . . . . . 6 class
63, 5cop 4216 . . . . 5 class 𝑔,
7 crngo 33823 . . . . 5 class RingOps
86, 7wcel 2030 . . . 4 wff 𝑔, ⟩ ∈ RingOps
93crn 5144 . . . . . . . 8 class ran 𝑔
10 cgi 27472 . . . . . . . . . 10 class GId
113, 10cfv 5926 . . . . . . . . 9 class (GId‘𝑔)
1211csn 4210 . . . . . . . 8 class {(GId‘𝑔)}
139, 12cdif 3604 . . . . . . 7 class (ran 𝑔 ∖ {(GId‘𝑔)})
1413, 13cxp 5141 . . . . . 6 class ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))
155, 14cres 5145 . . . . 5 class ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})))
16 cgr 27471 . . . . 5 class GrpOp
1715, 16wcel 2030 . . . 4 wff ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp
188, 17wa 383 . . 3 wff (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)
1918, 2, 4copab 4745 . 2 class {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
201, 19wceq 1523 1 wff DivRingOps = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
 Colors of variables: wff setvar class This definition is referenced by:  isdivrngo  33879  drngoi  33880  isdrngo1  33885
 Copyright terms: Public domain W3C validator