Theorem 0ring1eq0

Description: In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	|- B = ( Base ` R )
	0ring.0	|- .0. = ( 0g ` R )
	0ring01eq.1	|- .1. = ( 1r ` R )
Assertion	0ring1eq0	|- ( R e. ( Ring \ NzRing ) -> .1. = .0. )

Proof

Step	Hyp	Ref	Expression
1		0ring.b	|- B = ( Base ` R )
2		0ring.0	|- .0. = ( 0g ` R )
3		0ring01eq.1	|- .1. = ( 1r ` R )
4		eldif	|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ -. R e. NzRing ) )
5		0ringnnzr	|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
6		eqid	|- ( Base ` R ) = ( Base ` R )
7	6 2 3	0ring01eq	|- ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .0. = .1. )
8	7	eqcomd	|- ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .1. = .0. )
9	8	ex	|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 -> .1. = .0. ) )
10	5 9	sylbird	|- ( R e. Ring -> ( -. R e. NzRing -> .1. = .0. ) )
11	10	imp	|- ( ( R e. Ring /\ -. R e. NzRing ) -> .1. = .0. )
12	4 11	sylbi	|- ( R e. ( Ring \ NzRing ) -> .1. = .0. )