Metamath Proof Explorer


Theorem ring1zr

Description: The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 7-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 ring1zr.b 𝐵 = ( Base ‘ 𝑅 )
2 ring1zr.p + = ( +g𝑅 )
3 ring1zr.t = ( .r𝑅 )
4 ringsrg ( 𝑅 ∈ Ring → 𝑅 ∈ SRing )
5 1 2 3 srg1zr ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
6 4 5 syl3anl1 ( ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )