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

Theorem isdrng 19503
 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 6646 . . . 4 (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2 isdrng.u . . . 4 𝑈 = (Unit‘𝑅)
31, 2eqtr4di 2851 . . 3 (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4 fveq2 6646 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5 isdrng.b . . . . 5 𝐵 = (Base‘𝑅)
64, 5eqtr4di 2851 . . . 4 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7 fveq2 6646 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
8 isdrng.z . . . . . 6 0 = (0g𝑅)
97, 8eqtr4di 2851 . . . . 5 (𝑟 = 𝑅 → (0g𝑟) = 0 )
109sneqd 4537 . . . 4 (𝑟 = 𝑅 → {(0g𝑟)} = { 0 })
116, 10difeq12d 4051 . . 3 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g𝑟)}) = (𝐵 ∖ { 0 }))
123, 11eqeq12d 2814 . 2 (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13 df-drng 19501 . 2 DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)})}
1412, 13elrab2 3631 1 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∖ cdif 3878  {csn 4525  ‘cfv 6325  Basecbs 16478  0gc0g 16708  Ringcrg 19294  Unitcui 19389  DivRingcdr 19499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-iota 6284  df-fv 6333  df-drng 19501 This theorem is referenced by:  drngunit  19504  drngui  19505  drngring  19506  isdrng2  19509  drngprop  19510  drngid  19513  opprdrng  19523  drngpropd  19526  issubdrg  19557  cntzsdrg  19578  drngdomn  20073  fidomndrng  20077  zringndrg  20187  istdrg2  22793  cvsunit  23746  cphreccllem  23793  sradrng  31091  zrhunitpreima  31344
 Copyright terms: Public domain W3C validator