Theorem 0ring01eqbi2

Description: In a ring, 0 = 1 iff the ring contains only 0 . (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Hypotheses	0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
	0ring01eq.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	0ring01eqbi2	⊢ ( 𝑅 ∈ Ring → ( 𝐵 = { 0 } ↔ 1 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		0ring01eq.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		fveq2	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ { 0 } ) )
5	2	fvexi	⊢ 0 ∈ V
6		hashsng	⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
7	5 6	ax-mp	⊢ ( ♯ ‘ { 0 } ) = 1
8	4 7	eqtrdi	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = 1 )
9	1 2 3	0ring01eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 0 = 1 )
10	8 9	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) → 0 = 1 )
11	10	eqcomd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) → 1 = 0 )
12	11	ex	⊢ ( 𝑅 ∈ Ring → ( 𝐵 = { 0 } → 1 = 0 ) )
13		eqcom	⊢ ( 1 = 0 ↔ 0 = 1 )
14	1 2 3	01eq0ring	⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 } )
15	14	ex	⊢ ( 𝑅 ∈ Ring → ( 0 = 1 → 𝐵 = { 0 } ) )
16	13 15	biimtrid	⊢ ( 𝑅 ∈ Ring → ( 1 = 0 → 𝐵 = { 0 } ) )
17	12 16	impbid	⊢ ( 𝑅 ∈ Ring → ( 𝐵 = { 0 } ↔ 1 = 0 ) )