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	$⊢ B = {Base}_{R}$
		srg1zr.p	$⊢ \underset{˙}{+} = +_{R}$
		srg1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
		srgen1zr.p	$⊢ Z = 0_{R}$
	Assertion	srgen1zr	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \to (B \approx 1_{𝑜} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$

Proof

Step	Hyp	Ref	Expression
1		srg1zr.b	$⊢ B = {Base}_{R}$
2		srg1zr.p	$⊢ \underset{˙}{+} = +_{R}$
3		srg1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
4		srgen1zr.p	$⊢ Z = 0_{R}$
5	1 4	srg0cl	$⊢ R \in SRing \to Z \in B$
6	5	3ad2ant1	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to Z \in B$
7		en1eqsnbi	$⊢ Z \in B \to (B \approx 1_{𝑜} \leftrightarrow B = \{Z\})$
8	7	adantl	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to (B \approx 1_{𝑜} \leftrightarrow B = \{Z\})$
9	1 2 3	srg1zr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$
10	8 9	bitrd	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (B \approx 1_{𝑜} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$
11	6 10	mpdan	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \to (B \approx 1_{𝑜} \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$