Theorem isnzr

Description: Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypotheses	isnzr.o	|- .1. = ( 1r ` R )
	isnzr.z	|- .0. = ( 0g ` R )
Assertion	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )

Proof

Step	Hyp	Ref	Expression
1		isnzr.o	|- .1. = ( 1r ` R )
2		isnzr.z	|- .0. = ( 0g ` R )
3		fveq2	|- ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
4	3 1	eqtr4di	|- ( r = R -> ( 1r ` r ) = .1. )
5		fveq2	|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
6	5 2	eqtr4di	|- ( r = R -> ( 0g ` r ) = .0. )
7	4 6	neeq12d	|- ( r = R -> ( ( 1r ` r ) =/= ( 0g ` r ) <-> .1. =/= .0. ) )
8		df-nzr	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
9	7 8	elrab2	|- ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )