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

Theorem isdrng 18975
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 6418 . . . 4 (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2 isdrng.u . . . 4 𝑈 = (Unit‘𝑅)
31, 2syl6eqr 2869 . . 3 (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4 fveq2 6418 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5 isdrng.b . . . . 5 𝐵 = (Base‘𝑅)
64, 5syl6eqr 2869 . . . 4 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7 fveq2 6418 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
8 isdrng.z . . . . . 6 0 = (0g𝑅)
97, 8syl6eqr 2869 . . . . 5 (𝑟 = 𝑅 → (0g𝑟) = 0 )
109sneqd 4393 . . . 4 (𝑟 = 𝑅 → {(0g𝑟)} = { 0 })
116, 10difeq12d 3939 . . 3 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g𝑟)}) = (𝐵 ∖ { 0 }))
123, 11eqeq12d 2832 . 2 (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13 df-drng 18973 . 2 DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)})}
1412, 13elrab2 3573 1 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wcel 2157  cdif 3777  {csn 4381  cfv 6111  Basecbs 16088  0gc0g 16325  Ringcrg 18769  Unitcui 18861  DivRingcdr 18971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6074  df-fv 6119  df-drng 18973
This theorem is referenced by:  drngunit  18976  drngui  18977  drngring  18978  isdrng2  18981  drngprop  18982  drngid  18985  opprdrng  18995  drngpropd  18998  issubdrg  19029  drngdomn  19532  fidomndrng  19536  zringndrg  20066  istdrg2  22215  cvsunit  23164  cphreccllem  23211  zrhunitpreima  30370  cntzsdrg  38291
  Copyright terms: Public domain W3C validator