Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019) (Proof shortened by SN, 23-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		0ring01eq.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		eqcom	⊢ ( 0 = 1 ↔ 1 = 0 )
5	1 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
6	5	ne0d	⊢ ( 𝑅 ∈ Ring → 𝐵 ≠ ∅ )
7	5	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ 𝐵 )
8	1 3 2	ring1eq0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 1 = 0 → 𝑥 = 0 ) )
9	7 8	mpd3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 1 = 0 → 𝑥 = 0 ) )
10	9	impancom	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → ( 𝑥 ∈ 𝐵 → 𝑥 = 0 ) )
11	10	ralrimiv	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → ∀ 𝑥 ∈ 𝐵 𝑥 = 0 )
12		eqsn	⊢ ( 𝐵 ≠ ∅ → ( 𝐵 = { 0 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) )
13	12	biimpar	⊢ ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) → 𝐵 = { 0 } )
14	6 11 13	syl2an2r	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → 𝐵 = { 0 } )
15	4 14	sylan2b	⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 } )