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 ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )