Theorem 0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	|- B = ( Base ` R )
2		0ring.0	|- .0. = ( 0g ` R )
3		0ring01eq.1	|- .1. = ( 1r ` R )
4	1 2	0ring	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
5	1 3	ringidcl	|- ( R e. Ring -> .1. e. B )
6		eleq2	|- ( B = { .0. } -> ( .1. e. B <-> .1. e. { .0. } ) )
7		elsni	|- ( .1. e. { .0. } -> .1. = .0. )
8	7	eqcomd	|- ( .1. e. { .0. } -> .0. = .1. )
9	6 8	biimtrdi	|- ( B = { .0. } -> ( .1. e. B -> .0. = .1. ) )
10	5 9	syl5com	|- ( R e. Ring -> ( B = { .0. } -> .0. = .1. ) )
11	10	adantr	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( B = { .0. } -> .0. = .1. ) )
12	4 11	mpd	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )