This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0ringbas

Description: The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ring.0	⊢ 0 = ( 0_g ‘ 𝑅 )
Assertion	0ringbas	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) → 𝐵 = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		0ring.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ring.0	⊢ 0 = ( 0_g ‘ 𝑅 )
3	1 2	0ringdif	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) ↔ ( 𝑅 ∈ Ring ∧ 𝐵 = { 0 } ) )
4	3	simprbi	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) → 𝐵 = { 0 } )