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

Metamath Proof Explorer

Theorem srgen1zr

Description: The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010) (Revised by AV, 25-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 srg1zr.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srg1zr.p ⊢ + = ( +g ‘ 𝑅 )
3 srg1zr.t ⊢ ∗ = ( .r ‘ 𝑅 )
4 srgen1zr.p ⊢ 𝑍 = ( 0g ‘ 𝑅 )
5 1 4 srg0cl ⊢ ( 𝑅 ∈ SRing → 𝑍 ∈ 𝐵 )
6 5 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → 𝑍 ∈ 𝐵 )
7 en1eqsnbi ⊢ ( 𝑍 ∈ 𝐵 → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝑍 } ) )
8 7 adantl ⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝑍 } ) )
9 1 2 3 srg1zr ⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
10 8 9 bitrd ⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
11 6 10 mpdan ⊢ ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )