Theorem 0ring

Description: If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	|- B = ( Base ` R )
2		0ring.0	|- .0. = ( 0g ` R )
3	1 2	ring0cl	|- ( R e. Ring -> .0. e. B )
4	1	fvexi	|- B e. _V
5		hashen1	|- ( B e. _V -> ( ( # ` B ) = 1 <-> B ~~ 1o ) )
6	4 5	ax-mp	|- ( ( # ` B ) = 1 <-> B ~~ 1o )
7		en1eqsn	|- ( ( .0. e. B /\ B ~~ 1o ) -> B = { .0. } )
8	7	ex	|- ( .0. e. B -> ( B ~~ 1o -> B = { .0. } ) )
9	6 8	syl5bi	|- ( .0. e. B -> ( ( # ` B ) = 1 -> B = { .0. } ) )
10	3 9	syl	|- ( R e. Ring -> ( ( # ` B ) = 1 -> B = { .0. } ) )
11	10	imp	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )