Theorem rngen1zr0

Description: The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Hypotheses	rng1zr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rng1zr.p	⊢ + = ( +g ‘ 𝑅 )
	rng1zr.t	⊢ ∗ = ( .r ‘ 𝑅 )
	rngen1zr0.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	rngen1zr0	⊢ ( ( 𝑅 ∈ Rng ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ∧ ∗ = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		rng1zr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rng1zr.p	⊢ + = ( +g ‘ 𝑅 )
3		rng1zr.t	⊢ ∗ = ( .r ‘ 𝑅 )
4		rngen1zr0.0	⊢ 0 = ( 0g ‘ 𝑅 )
5	1 4	rng0cl	⊢ ( 𝑅 ∈ Rng → 0 ∈ 𝐵 )
6	5	3ad2ant1	⊢ ( ( 𝑅 ∈ Rng ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → 0 ∈ 𝐵 )
7	1 2 3	rngen1zr	⊢ ( ( ( 𝑅 ∈ Rng ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 0 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ∧ ∗ = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ) ) )
8	6 7	mpdan	⊢ ( ( 𝑅 ∈ Rng ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ∧ ∗ = { ⟨ ⟨ 0 , 0 ⟩ , 0 ⟩ } ) ) )