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

Theorem drngunit 19504
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 19503 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
54simprbi 500 . . 3 (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
65eleq2d 2878 . 2 (𝑅 ∈ DivRing → (𝑋𝑈𝑋 ∈ (𝐵 ∖ { 0 })))
7 eldifsn 4683 . 2 (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋𝐵𝑋0 ))
86, 7syl6bb 290 1 (𝑅 ∈ DivRing → (𝑋𝑈 ↔ (𝑋𝐵𝑋0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  wne 2990  cdif 3881  {csn 4528  cfv 6328  Basecbs 16479  0gc0g 16709  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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
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 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-drng 19501
This theorem is referenced by:  drngunz  19514  drnginvrcl  19516  drnginvrn0  19517  drnginvrl  19518  drnginvrr  19519  issubdrg  19557  abvdiv  19605  qsssubdrg  20154  redvr  20310  drnguc1p  24775  lgseisenlem3  25965  ornglmullt  30935  orngrmullt  30936  isarchiofld  30945  qqhval2lem  31336  qqhf  31341  matunitlindf  35054  lincreslvec3  44888  isldepslvec2  44891
  Copyright terms: Public domain W3C validator