Theorem 0ring01eqbi

Description: In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by AV, 23-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		0ring01eq.1	⊢ 1 = ( 1r ‘ 𝑅 )
4	1	fvexi	⊢ 𝐵 ∈ V
5		hashen1	⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 1 ↔ 𝐵 ≈ 1o ) )
6	4 5	mp1i	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 ↔ 𝐵 ≈ 1o ) )
7	1 2 3	0ring01eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 0 = 1 )
8	7	eqcomd	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 1 = 0 )
9	8	ex	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 → 1 = 0 ) )
10		eqcom	⊢ ( 1 = 0 ↔ 0 = 1 )
11	1 2 3	01eq0ring	⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 } )
12		fveq2	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ { 0 } ) )
13	2	fvexi	⊢ 0 ∈ V
14		hashsng	⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
15	13 14	mp1i	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ { 0 } ) = 1 )
16	12 15	eqtrd	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = 1 )
17	11 16	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → ( ♯ ‘ 𝐵 ) = 1 )
18	17	ex	⊢ ( 𝑅 ∈ Ring → ( 0 = 1 → ( ♯ ‘ 𝐵 ) = 1 ) )
19	10 18	syl5bi	⊢ ( 𝑅 ∈ Ring → ( 1 = 0 → ( ♯ ‘ 𝐵 ) = 1 ) )
20	9 19	impbid	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 ↔ 1 = 0 ) )
21	6 20	bitr3d	⊢ ( 𝑅 ∈ Ring → ( 𝐵 ≈ 1o ↔ 1 = 0 ) )