Theorem 0ringdif

Description: A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	0ringdif	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) ↔ ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		eldif	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) ↔ ( 𝑅 ∈ Ring ∧ ¬ 𝑅 ∈ NzRing ) )
4	1	a1i	⊢ ( 𝑅 ∈ Ring → 𝐵 = ( Base ‘ 𝑅 ) )
5	4	fveqeq2d	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
6	1 2	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )
7	6	ex	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 → 𝐵 = { 0 } ) )
8		fveq2	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ { 0 } ) )
9	2	fvexi	⊢ 0 ∈ V
10		hashsng	⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
11	9 10	ax-mp	⊢ ( ♯ ‘ { 0 } ) = 1
12	8 11	eqtrdi	⊢ ( 𝐵 = { 0 } → ( ♯ ‘ 𝐵 ) = 1 )
13	7 12	impbid1	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) = 1 ↔ 𝐵 = { 0 } ) )
14		0ringnnzr	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )
15	5 13 14	3bitr3rd	⊢ ( 𝑅 ∈ Ring → ( ¬ 𝑅 ∈ NzRing ↔ 𝐵 = { 0 } ) )
16	15	pm5.32i	⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 𝑅 ∈ NzRing ) ↔ ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) )
17	3 16	bitri	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) ↔ ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) )