Theorem 0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		0ring01eq.1	⊢ 1 = ( 1r ‘ 𝑅 )
4	1 2	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )
5	1 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
6		eleq2	⊢ ( 𝐵 = { 0 } → ( 1 ∈ 𝐵 ↔ 1 ∈ { 0 } ) )
7		elsni	⊢ ( 1 ∈ { 0 } → 1 = 0 )
8	7	eqcomd	⊢ ( 1 ∈ { 0 } → 0 = 1 )
9	6 8	biimtrdi	⊢ ( 𝐵 = { 0 } → ( 1 ∈ 𝐵 → 0 = 1 ) )
10	5 9	syl5com	⊢ ( 𝑅 ∈ Ring → ( 𝐵 = { 0 } → 0 = 1 ) )
11	10	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( 𝐵 = { 0 } → 0 = 1 ) )
12	4 11	mpd	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 0 = 1 )