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

Theorem drngunit 20734
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 20733 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
54simprbi 496 . . 3 (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
65eleq2d 2827 . 2 (𝑅 ∈ DivRing → (𝑋𝑈𝑋 ∈ (𝐵 ∖ { 0 })))
7 eldifsn 4786 . 2 (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋𝐵𝑋0 ))
86, 7bitrdi 287 1 (𝑅 ∈ DivRing → (𝑋𝑈 ↔ (𝑋𝐵𝑋0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wne 2940  cdif 3948  {csn 4626  cfv 6561  Basecbs 17247  0gc0g 17484  Ringcrg 20230  Unitcui 20355  DivRingcdr 20729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-drng 20731
This theorem is referenced by:  drngunz  20747  drnginvrcl  20753  drnginvrn0  20754  drnginvrl  20756  drnginvrr  20757  issubdrg  20781  sdrgunit  20797  abvdiv  20830  qsssubdrg  21444  redvr  21635  drnguc1p  26213  lgseisenlem3  27421  sdrgdvcl  33301  sdrginvcl  33302  ornglmullt  33337  orngrmullt  33338  isarchiofld  33347  1arithufd  33576  ply1asclunit  33599  ply1dg1rt  33604  qqhval2lem  33982  qqhf  33987  matunitlindf  37625  fldhmf1  42091  lincreslvec3  48399  isldepslvec2  48402
  Copyright terms: Public domain W3C validator