Theorem drngunit 20990

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

Step	Hyp	Ref	Expression
1		isdrng.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
2		isdrng.u	. . . . 5 ⊢ 𝑈 = (Unit‘𝑅)
3		isdrng.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
4	1, 2, 3	isdrng 20989	. . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
5	4	simprbi 503	. . 3 ⊢ (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
6	5	eleq2d 2846	. 2 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐵 ∖ { 0 })))
7		eldifsn 4744	. 2 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))
8	6, 7	bitrdi 290	1 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ≠ wne 2955   ∖ cdif 4045  {csn 4584  ‘cfv 6538  Basecbs 17392  0_gc0g 17615  Ringcrg 20464  Unitcui 20590  DivRingcdr 20985

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-drng 20987

This theorem is used by:  drngunz  21006  drnginvrcl  21016  drnginvrn0  21017  drnginvrl  21019  drnginvrr  21020  issubdrg  21042  sdrgunit  21058  abvdiv  21091  ornglmullt  21131  orngrmullt  21132  qsssubdrg  21737  redvr  21928  matunitlindf  23001  drnguc1p  26497  lgseisenlem3  27709  fxpsdrg  33782  isarchiofld  33806  sdrgdvcl  33907  sdrginvcl  33908  drnglring  34070  1arithufd  34126  ply1asclunit  34152  ply1dg1rt  34158  qqhval2lem  34659  qqhf  34664  fldhmf1  43233  lincreslvec3  49687  isldepslvec2  49690  veroquaddetzerod  51154