Theorem drngui

Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	drngui.b	|- B = ( Base ` R )
	drngui.z	|- .0. = ( 0g ` R )
	drngui.r	|- R e. DivRing
Assertion	drngui	|- ( B \ { .0. } ) = ( Unit ` R )

Proof

Step	Hyp	Ref	Expression
1		drngui.b	|- B = ( Base ` R )
2		drngui.z	|- .0. = ( 0g ` R )
3		drngui.r	|- R e. DivRing
4		eqid	|- ( Unit ` R ) = ( Unit ` R )
5	1 4 2	isdrng	|- ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) )
6	3 5	mpbi	|- ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) )
7	6	simpri	|- ( Unit ` R ) = ( B \ { .0. } )
8	7	eqcomi	|- ( B \ { .0. } ) = ( Unit ` R )