Theorem drngunit 18752

Description: Elementhood in the set of units when R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypotheses

Ref	Expression
isdrng.b	|- B = ( Base ` R )
isdrng.u	|- U = (Unit ` R )
isdrng.z	|- .0. = ( 0g ` R )

Assertion

Ref	Expression
drngunit	|- ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X =/= .0. ) ) )

Proof of Theorem drngunit

Step	Hyp	Ref	Expression
1		isdrng.b	. . . . 5 |- B = ( Base ` R )
2		isdrng.u	. . . . 5 |- U = (Unit ` R )
3		isdrng.z	. . . . 5 |- .0. = ( 0g ` R )
4	1, 2, 3	isdrng 18751	. . . 4 |- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )
5	4	simprbi 480	. . 3 |- ( R e. DivRing -> U = ( B \ { .0. } ) )
6	5	eleq2d 2687	. 2 |- ( R e. DivRing -> ( X e. U <-> X e. ( B \ { .0. } ) ) )
7		eldifsn 4317	. 2 |- ( X e. ( B \ { .0. } ) <-> ( X e. B /\ X =/= .0. ) )
8	6, 7	syl6bb 276	1 |- ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X =/= .0. ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   \ cdif 3571   {csn 4177   ` cfv 5888   Basecbs 15857   0gc0g 16100   Ringcrg 18547  Unitcui 18639   DivRingcdr 18747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-drng 18749

This theorem is referenced by:  drngunz  18762  drnginvrcl  18764  drnginvrn0  18765  drnginvrl  18766  drnginvrr  18767  issubdrg  18805  abvdiv  18837  qsssubdrg  19805  redvr  19963  drnguc1p  23930  lgseisenlem3  25102  ornglmullt  29807  orngrmullt  29808  isarchiofld  29817  qqhval2lem  30025  qqhf  30030  matunitlindf  33407  lincreslvec3  42271  isldepslvec2  42274