Theorem drngunz

Description: A division ring's unit is different from its zero. (Contributed by NM, 8-Sep-2011)

	Ref	Expression
Hypotheses	drngunz.z	|- .0. = ( 0g ` R )
	drngunz.u	|- .1. = ( 1r ` R )
Assertion	drngunz	|- ( R e. DivRing -> .1. =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		drngunz.z	|- .0. = ( 0g ` R )
2		drngunz.u	|- .1. = ( 1r ` R )
3		drngring	|- ( R e. DivRing -> R e. Ring )
4		eqid	|- ( Unit ` R ) = ( Unit ` R )
5	4 2	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
6	3 5	syl	|- ( R e. DivRing -> .1. e. ( Unit ` R ) )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8	7 4 1	drngunit	|- ( R e. DivRing -> ( .1. e. ( Unit ` R ) <-> ( .1. e. ( Base ` R ) /\ .1. =/= .0. ) ) )
9	6 8	mpbid	|- ( R e. DivRing -> ( .1. e. ( Base ` R ) /\ .1. =/= .0. ) )
10	9	simprd	|- ( R e. DivRing -> .1. =/= .0. )