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

Theorem drngunit 20506
Description: Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
isdrng.b 𝐡 = (Baseβ€˜π‘…)
isdrng.u π‘ˆ = (Unitβ€˜π‘…)
isdrng.z 0 = (0gβ€˜π‘…)
Assertion
Ref Expression
drngunit (𝑅 ∈ DivRing β†’ (𝑋 ∈ π‘ˆ ↔ (𝑋 ∈ 𝐡 ∧ 𝑋 β‰  0 )))

Proof of Theorem drngunit
StepHypRef Expression
1 isdrng.b . . . . 5 𝐡 = (Baseβ€˜π‘…)
2 isdrng.u . . . . 5 π‘ˆ = (Unitβ€˜π‘…)
3 isdrng.z . . . . 5 0 = (0gβ€˜π‘…)
41, 2, 3isdrng 20505 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ π‘ˆ = (𝐡 βˆ– { 0 })))
54simprbi 496 . . 3 (𝑅 ∈ DivRing β†’ π‘ˆ = (𝐡 βˆ– { 0 }))
65eleq2d 2818 . 2 (𝑅 ∈ DivRing β†’ (𝑋 ∈ π‘ˆ ↔ 𝑋 ∈ (𝐡 βˆ– { 0 })))
7 eldifsn 4790 . 2 (𝑋 ∈ (𝐡 βˆ– { 0 }) ↔ (𝑋 ∈ 𝐡 ∧ 𝑋 β‰  0 ))
86, 7bitrdi 287 1 (𝑅 ∈ DivRing β†’ (𝑋 ∈ π‘ˆ ↔ (𝑋 ∈ 𝐡 ∧ 𝑋 β‰  0 )))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105   β‰  wne 2939   βˆ– cdif 3945  {csn 4628  β€˜cfv 6543  Basecbs 17149  0gc0g 17390  Ringcrg 20128  Unitcui 20247  DivRingcdr 20501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-drng 20503
This theorem is referenced by:  drngunz  20520  drnginvrcl  20523  drnginvrn0  20524  drnginvrl  20526  drnginvrr  20527  issubdrg  20545  sdrgunit  20556  abvdiv  20589  qsssubdrg  21205  redvr  21390  drnguc1p  25924  lgseisenlem3  27117  sdrgdvcl  32668  sdrginvcl  32669  ornglmullt  32696  orngrmullt  32697  isarchiofld  32706  ply1asclunit  32929  qqhval2lem  33260  qqhf  33265  matunitlindf  36790  fldhmf1  41262  lincreslvec3  47251  isldepslvec2  47254
  Copyright terms: Public domain W3C validator