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)

	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		pm4.24	$⊢ B = \{Z\} \leftrightarrow (B = \{Z\} \land B = \{Z\})$
5		srgmnd	$⊢ R \in SRing \to R \in Mnd$
6	5	3ad2ant1	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to R \in Mnd$
7	6	adantr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to R \in Mnd$
8		mndmgm	$⊢ R \in Mnd \to R \in Mgm$
9	7 8	syl	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to R \in Mgm$
10		simpr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to Z \in B$
11		simpl2	$⊢ ((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)$
12	1 2	mgmb1mgm1	$⊢ (R \in Mgm \land Z \in B \land \underset{˙}{+} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow \underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\})$
13	9 10 11 12	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⟩\})$
14		simpl1	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to R \in SRing$
15		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
16	15	srgmgp	$⊢ R \in SRing \to {mulGrp}_{R} \in Mnd$
17		mndmgm	$⊢ {mulGrp}_{R} \in Mnd \to {mulGrp}_{R} \in Mgm$
18	14 16 17	3syl	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to {mulGrp}_{R} \in Mgm$
19	15 3	mgpplusg	$⊢ \underset{˙}{*} = +_{{mulGrp}_{R}}$
20	19	fneq1i	$⊢ \underset{˙}{*} Fn (B \times B) \leftrightarrow +_{{mulGrp}_{R}} Fn (B \times B)$
21	20	biimpi	$⊢ \underset{˙}{*} Fn (B \times B) \to +_{{mulGrp}_{R}} Fn (B \times B)$
22	21	3ad2ant3	$⊢ (R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \to +_{{mulGrp}_{R}} Fn (B \times B)$
23	22	adantr	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to +_{{mulGrp}_{R}} Fn (B \times B)$
24	15 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
25		eqid	$⊢ +_{{mulGrp}_{R}} = +_{{mulGrp}_{R}}$
26	24 25	mgmb1mgm1	$⊢ ({mulGrp}_{R} \in Mgm \land Z \in B \land +_{{mulGrp}_{R}} Fn (B \times B)) \to (B = \{Z\} \leftrightarrow +_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\})$
27	18 10 23 26	syl3anc	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{*} Fn (B \times B)) \land Z \in B) \to (B = \{Z\} \leftrightarrow +_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\})$
28	19	eqcomi	$⊢ +_{{mulGrp}_{R}} = \underset{˙}{*}$
29	28	a1i	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to +_{{mulGrp}_{R}} = \underset{˙}{}$
30	29	eqeq1d	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to (+_{{mulGrp}_{R}} = \{⟨⟨Z, Z⟩, Z⟩\} \leftrightarrow \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\})$
31	27 30	bitrd	$⊢ ((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⟩\})$
32	13 31	anbi12d	$⊢ ((R \in SRing \land \underset{˙}{+} Fn (B \times B) \land \underset{˙}{} Fn (B \times B)) \land Z \in B) \to ((B = \{Z\} \land B = \{Z\}) \leftrightarrow (\underset{˙}{+} = \{⟨⟨Z, Z⟩, Z⟩\} \land \underset{˙}{} = \{⟨⟨Z, Z⟩, Z⟩\}))$
33	4 32	syl5bb	$⊢ ((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