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

Theorem isdrng 20307
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 6887 . . . 4 (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2 isdrng.u . . . 4 𝑈 = (Unit‘𝑅)
31, 2eqtr4di 2791 . . 3 (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4 fveq2 6887 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5 isdrng.b . . . . 5 𝐵 = (Base‘𝑅)
64, 5eqtr4di 2791 . . . 4 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7 fveq2 6887 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
8 isdrng.z . . . . . 6 0 = (0g𝑅)
97, 8eqtr4di 2791 . . . . 5 (𝑟 = 𝑅 → (0g𝑟) = 0 )
109sneqd 4638 . . . 4 (𝑟 = 𝑅 → {(0g𝑟)} = { 0 })
116, 10difeq12d 4121 . . 3 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g𝑟)}) = (𝐵 ∖ { 0 }))
123, 11eqeq12d 2749 . 2 (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13 df-drng 20305 . 2 DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g𝑟)})}
1412, 13elrab2 3684 1 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wcel 2107  cdif 3943  {csn 4626  cfv 6539  Basecbs 17139  0gc0g 17380  Ringcrg 20046  Unitcui 20157  DivRingcdr 20303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-br 5147  df-iota 6491  df-fv 6547  df-drng 20305
This theorem is referenced by:  drngunit  20308  drngui  20309  drngring  20310  isdrng2  20316  drngprop  20317  drngid  20320  opprdrng  20334  drngpropd  20339  issubdrg  20376  imadrhmcl  20400  cntzsdrg  20405  drngdomn  20905  fidomndrng  20910  zringndrg  21021  istdrg2  23663  cvsunit  24628  cphreccllem  24676  isdrng4  32363  sradrng  32618  zrhunitpreima  32895
  Copyright terms: Public domain W3C validator