Theorem drngunit 18975

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 18974	. . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
5	4	simprbi 486	. . 3 ⊢ (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
6	5	eleq2d 2882	. 2 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐵 ∖ { 0 })))
7		eldifsn 4519	. 2 ⊢ (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ))
8	6, 7	syl6bb 278	1 ⊢ (𝑅 ∈ DivRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2157   ≠ wne 2989   ∖ cdif 3777  {csn 4381  ‘cfv 6110  Basecbs 16087  0_gc0g 16324  Ringcrg 18768  Unitcui 18860  DivRingcdr 18970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118  df-drng 18972

This theorem is referenced by:  drngunz  18985  drnginvrcl  18987  drnginvrn0  18988  drnginvrl  18989  drnginvrr  18990  issubdrg  19028  abvdiv  19060  qsssubdrg  20032  redvr  20191  drnguc1p  24166  lgseisenlem3  25338  ornglmullt  30154  orngrmullt  30155  isarchiofld  30164  qqhval2lem  30372  qqhf  30377  matunitlindf  33738  lincreslvec3  42856  isldepslvec2  42859