Users' Mathboxes 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 32714
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 32713 . 2 class DivRingOps
2 vg . . . . . . 7 setvar 𝑔
32cv 1473 . . . . . 6 class 𝑔
4 vh . . . . . . 7 setvar
54cv 1473 . . . . . 6 class
63, 5cop 4130 . . . . 5 class 𝑔,
7 crngo 32659 . . . . 5 class RingOps
86, 7wcel 1976 . . . 4 wff 𝑔, ⟩ ∈ RingOps
93crn 5029 . . . . . . . 8 class ran 𝑔
10 cgi 26494 . . . . . . . . . 10 class GId
113, 10cfv 5790 . . . . . . . . 9 class (GId‘𝑔)
1211csn 4124 . . . . . . . 8 class {(GId‘𝑔)}
139, 12cdif 3536 . . . . . . 7 class (ran 𝑔 ∖ {(GId‘𝑔)})
1413, 13cxp 5026 . . . . . 6 class ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))
155, 14cres 5030 . . . . 5 class ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})))
16 cgr 26493 . . . . 5 class GrpOp
1715, 16wcel 1976 . . . 4 wff ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp
188, 17wa 382 . . 3 wff (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)
1918, 2, 4copab 4636 . 2 class {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
201, 19wceq 1474 1 wff DivRingOps = {⟨𝑔, ⟩ ∣ (⟨𝑔, ⟩ ∈ RingOps ∧ ( ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
Colors of variables: wff setvar class
This definition is referenced by:  isdivrngo  32715  drngoi  32716  isdrngo1  32721
  Copyright terms: Public domain W3C validator