Theorem 0ring01eqbi

Description: In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by AV, 23-Jan-2020)

	Ref	Expression
Hypotheses	0ring.b	|- B = ( Base ` R )
	0ring.0	|- .0. = ( 0g ` R )
	0ring01eq.1	|- .1. = ( 1r ` R )
Assertion	0ring01eqbi	|- ( R e. Ring -> ( B ~~ 1o <-> .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	1	fvexi	|- B e. _V
5		hashen1	|- ( B e. _V -> ( ( # ` B ) = 1 <-> B ~~ 1o ) )
6	4 5	mp1i	|- ( R e. Ring -> ( ( # ` B ) = 1 <-> B ~~ 1o ) )
7	1 2 3	0ring01eq	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )
8	7	eqcomd	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .1. = .0. )
9	8	ex	|- ( R e. Ring -> ( ( # ` B ) = 1 -> .1. = .0. ) )
10		eqcom	|- ( .1. = .0. <-> .0. = .1. )
11	1 2 3	01eq0ring	|- ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )
12		fveq2	|- ( B = { .0. } -> ( # ` B ) = ( # ` { .0. } ) )
13	2	fvexi	|- .0. e. _V
14		hashsng	|- ( .0. e. _V -> ( # ` { .0. } ) = 1 )
15	13 14	mp1i	|- ( B = { .0. } -> ( # ` { .0. } ) = 1 )
16	12 15	eqtrd	|- ( B = { .0. } -> ( # ` B ) = 1 )
17	11 16	syl	|- ( ( R e. Ring /\ .0. = .1. ) -> ( # ` B ) = 1 )
18	17	ex	|- ( R e. Ring -> ( .0. = .1. -> ( # ` B ) = 1 ) )
19	10 18	syl5bi	|- ( R e. Ring -> ( .1. = .0. -> ( # ` B ) = 1 ) )
20	9 19	impbid	|- ( R e. Ring -> ( ( # ` B ) = 1 <-> .1. = .0. ) )
21	6 20	bitr3d	|- ( R e. Ring -> ( B ~~ 1o <-> .1. = .0. ) )