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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3	1 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
4	1	fvexi	⊢ 𝐵 ∈ V
5		hashen1	⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 1 ↔ 𝐵 ≈ 1o ) )
6	4 5	ax-mp	⊢ ( ( ♯ ‘ 𝐵 ) = 1 ↔ 𝐵 ≈ 1o )
7		en1eqsn	⊢ ( ( 0 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
8	7	ex	⊢ ( 0 ∈ 𝐵 → ( 𝐵 ≈ 1o → 𝐵 = { 0 } ) )
9	6 8	biimtrid	⊢ ( 0 ∈ 𝐵 → ( ( ♯ ‘ 𝐵 ) = 1 → 𝐵 = { 0 } ) )
10	3 9	syl	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 → 𝐵 = { 0 } ) )
11	10	imp	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )