Theorem drngunit

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

	Ref	Expression
Hypotheses	isdrng.b	|- B = ( Base ` R )
	isdrng.u	|- U = ( Unit ` R )
	isdrng.z	|- .0. = ( 0g ` R )
Assertion	drngunit	|- ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X =/= .0. ) ) )

Proof

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