Theorem 0ringdif

Description: A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ringdif.b	|- B = ( Base ` R )
	0ringdif.0	|- .0. = ( 0g ` R )
Assertion	0ringdif	|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		0ringdif.b	|- B = ( Base ` R )
2		0ringdif.0	|- .0. = ( 0g ` R )
3		eldif	|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ -. R e. NzRing ) )
4	1	a1i	|- ( R e. Ring -> B = ( Base ` R ) )
5	4	fveqeq2d	|- ( R e. Ring -> ( ( # ` B ) = 1 <-> ( # ` ( Base ` R ) ) = 1 ) )
6	1 2	0ring	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
7	6	ex	|- ( R e. Ring -> ( ( # ` B ) = 1 -> B = { .0. } ) )
8		fveq2	|- ( B = { .0. } -> ( # ` B ) = ( # ` { .0. } ) )
9	2	fvexi	|- .0. e. _V
10		hashsng	|- ( .0. e. _V -> ( # ` { .0. } ) = 1 )
11	9 10	ax-mp	|- ( # ` { .0. } ) = 1
12	8 11	eqtrdi	|- ( B = { .0. } -> ( # ` B ) = 1 )
13	7 12	impbid1	|- ( R e. Ring -> ( ( # ` B ) = 1 <-> B = { .0. } ) )
14		0ringnnzr	|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
15	5 13 14	3bitr3rd	|- ( R e. Ring -> ( -. R e. NzRing <-> B = { .0. } ) )
16	15	pm5.32i	|- ( ( R e. Ring /\ -. R e. NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )
17	3 16	bitri	|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )