Theorem drngunit 20667

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 20666	. . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
5	4	simprbi 496	. . 3 ⊢ (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
6	5	eleq2d 2822	. 2 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐵 ∖ { 0 })))
7		eldifsn 4742	. 2 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))
8	6, 7	bitrdi 287	1 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2932   ∖ cdif 3898  {csn 4580  ‘cfv 6492  Basecbs 17136  0_gc0g 17359  Ringcrg 20168  Unitcui 20291  DivRingcdr 20662

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-drng 20664

This theorem is referenced by:  drngunz  20680  drnginvrcl  20686  drnginvrn0  20687  drnginvrl  20689  drnginvrr  20690  issubdrg  20713  sdrgunit  20729  abvdiv  20762  ornglmullt  20802  orngrmullt  20803  qsssubdrg  21381  redvr  21572  drnguc1p  26135  lgseisenlem3  27344  fxpsdrg  33257  isarchiofld  33281  sdrgdvcl  33381  sdrginvcl  33382  1arithufd  33629  ply1asclunit  33655  ply1dg1rt  33661  qqhval2lem  34138  qqhf  34143  matunitlindf  37815  fldhmf1  42340  lincreslvec3  48724  isldepslvec2  48727