srg1zr

Description: The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 19-Jun-2026)

	Ref	Expression
Hypotheses	srg1zr.b	$⊢ B = {Base}_{R}$
	srg1zr.p	$⊢ \underset{˙}{+} = +_{R}$
	srg1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
Assertion	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⟩\}))$

Proof

Step	Hyp	Ref	Expression
1		srg1zr.b	$⊢ B = {Base}_{R}$
2		srg1zr.p	$⊢ \underset{˙}{+} = +_{R}$
3		srg1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
4		srgmnd	$⊢ R \in SRing \to R \in Mnd$
5		mndmgm	$⊢ R \in Mnd \to R \in Mgm$
6	4 5	syl	$⊢ R \in SRing \to R \in Mgm$
7		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
8	7	srgmgp	$⊢ R \in SRing \to {mulGrp}_{R} \in Mnd$
9		mndmgm	$⊢ {mulGrp}_{R} \in Mnd \to {mulGrp}_{R} \in Mgm$
10	8 9	syl	$⊢ R \in SRing \to {mulGrp}_{R} \in Mgm$
11	6 10	jca	$⊢ R \in SRing \to (R \in Mgm \land {mulGrp}_{R} \in Mgm)$
12	11	3ad2ant1	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to (R \in Mgm \land {mulGrp}_{R} \in Mgm)$
13	12	adantr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to (R \in Mgm \land {mulGrp}_{R} \in Mgm)$
14		3simpc	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \to (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B))$
15	14	adantr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (\underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B))$
16		simpr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to Z \in B$
17	1 2 3	rng1zrlem	$⊢ ((R \in Mgm \land {mulGrp}_{R} \in Mgm) \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⟩\}))$
18	13 15 16 17	syl3anc	$⊢ ((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⟩\}))$

Metamath Proof Explorer

Theorem srg1zr

Proof