Theorem isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised 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	isdrng	|- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .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		fveq2	|- ( r = R -> ( Unit ` r ) = ( Unit ` R ) )
5	4 2	eqtr4di	|- ( r = R -> ( Unit ` r ) = U )
6		fveq2	|- ( r = R -> ( Base ` r ) = ( Base ` R ) )
7	6 1	eqtr4di	|- ( r = R -> ( Base ` r ) = B )
8		fveq2	|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
9	8 3	eqtr4di	|- ( r = R -> ( 0g ` r ) = .0. )
10	9	sneqd	|- ( r = R -> { ( 0g ` r ) } = { .0. } )
11	7 10	difeq12d	|- ( r = R -> ( ( Base ` r ) \ { ( 0g ` r ) } ) = ( B \ { .0. } ) )
12	5 11	eqeq12d	|- ( r = R -> ( ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) <-> U = ( B \ { .0. } ) ) )
13		df-drng	|- DivRing = { r e. Ring | ( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
14	12 13	elrab2	|- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )