Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isdrng Structured version   Visualization version   GIF version

Theorem isdrng 19229
 Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
isdrng.b 𝐵 = (Base‘𝑅)
isdrng.u 𝑈 = (Unit‘𝑅)
isdrng.z 0 = (0g𝑅)
Assertion
Ref Expression
isdrng (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))

Proof of Theorem isdrng
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6499 . . . 4 (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2 isdrng.u . . . 4 𝑈 = (Unit‘𝑅)
31, 2syl6eqr 2833 . . 3 (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4 fveq2 6499 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5 isdrng.b . . . . 5 𝐵 = (Base‘𝑅)
64, 5syl6eqr 2833 . . . 4 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7 fveq2 6499 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
8 isdrng.z . . . . . 6 0 = (0g𝑅)
97, 8syl6eqr 2833 . . . . 5 (𝑟 = 𝑅 → (0g𝑟) = 0 )
109sneqd 4453 . . . 4 (𝑟 = 𝑅 → {(0g𝑟)} = { 0 })
116, 10difeq12d 3991 . . 3 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g𝑟)}) = (𝐵 ∖ { 0 }))
123, 11eqeq12d 2794 . 2 (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13 df-drng 19227 . 2 DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)})}
1412, 13elrab2 3600 1 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050   ∖ cdif 3827  {csn 4441  ‘cfv 6188  Basecbs 16339  0gc0g 16569  Ringcrg 19020  Unitcui 19112  DivRingcdr 19225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-iota 6152  df-fv 6196  df-drng 19227 This theorem is referenced by:  drngunit  19230  drngui  19231  drngring  19232  isdrng2  19235  drngprop  19236  drngid  19239  opprdrng  19249  drngpropd  19252  issubdrg  19283  cntzsdrg  19303  drngdomn  19797  fidomndrng  19801  zringndrg  20339  istdrg2  22489  cvsunit  23438  cphreccllem  23485  sradrng  30614  zrhunitpreima  30860
 Copyright terms: Public domain W3C validator