Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019) (Proof shortened by SN, 23-Feb-2025)

	Ref	Expression
Hypotheses	0ring.b	|- B = ( Base ` R )
	0ring.0	|- .0. = ( 0g ` R )
	0ring01eq.1	|- .1. = ( 1r ` R )
Assertion	01eq0ring	|- ( ( R e. Ring /\ .0. = .1. ) -> B = { .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		eqcom	|- ( .0. = .1. <-> .1. = .0. )
5	1 2	ring0cl	|- ( R e. Ring -> .0. e. B )
6	5	ne0d	|- ( R e. Ring -> B =/= (/) )
7	5	adantr	|- ( ( R e. Ring /\ x e. B ) -> .0. e. B )
8	1 3 2	ring1eq0	|- ( ( R e. Ring /\ x e. B /\ .0. e. B ) -> ( .1. = .0. -> x = .0. ) )
9	7 8	mpd3an3	|- ( ( R e. Ring /\ x e. B ) -> ( .1. = .0. -> x = .0. ) )
10	9	impancom	|- ( ( R e. Ring /\ .1. = .0. ) -> ( x e. B -> x = .0. ) )
11	10	ralrimiv	|- ( ( R e. Ring /\ .1. = .0. ) -> A. x e. B x = .0. )
12		eqsn	|- ( B =/= (/) -> ( B = { .0. } <-> A. x e. B x = .0. ) )
13	12	biimpar	|- ( ( B =/= (/) /\ A. x e. B x = .0. ) -> B = { .0. } )
14	6 11 13	syl2an2r	|- ( ( R e. Ring /\ .1. = .0. ) -> B = { .0. } )
15	4 14	sylan2b	|- ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )