Theorem ringen1zr0

Description: The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 , and semirings, see srgen1zr0 . (Contributed by FL, 15-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 19-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ring1zr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ring1zr.p	⊢ + = ( +g ‘ 𝑅 )
3		ring1zr.t	⊢ ∗ = ( .r ‘ 𝑅 )
4		ringen1zr0.0	⊢ 𝑍 = ( 0g ‘ 𝑅 )
5		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
6	1 2 3 4	rngen1zr0	⊢ ( ( 𝑅 ∈ Rng ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
7	5 6	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )