ring1zr

Description: The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 7-Feb-2020)

	Ref	Expression
Hypotheses	ring1zr.b	$⊢ B = {Base}_{R}$
	ring1zr.p	$⊢ \underset{˙}{+} = +_{R}$
	ring1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
Assertion	ring1zr	$⊢ ((R \in Ring \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		ring1zr.b	$⊢ B = {Base}_{R}$
2		ring1zr.p	$⊢ \underset{˙}{+} = +_{R}$
3		ring1zr.t	$⊢ \underset{˙}{*} = \cdot_{R}$
4		ringsrg	$⊢ R \in Ring \to R \in SRing$
5	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⟩\}))$
6	4 5	syl3anl1	$⊢ ((R \in Ring \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 ring1zr

Proof