rngosn4

Description: Obsolete as of 25-Jan-2020. Use rngen1zr instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	on1el3.1	$⊢ G = 1^{st} (R)$
	on1el3.2	$⊢ X = ran G$
Assertion	rngosn4	$⊢ (R \in RingOps \land A \in X) \to (X \approx 1_{𝑜} \leftrightarrow R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩)$

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	$⊢ G = 1^{st} (R)$
2		on1el3.2	$⊢ X = ran G$
3		en1eqsnbi	$⊢ A \in X \to (X \approx 1_{𝑜} \leftrightarrow X = \{A\})$
4	3	adantl	$⊢ (R \in RingOps \land A \in X) \to (X \approx 1_{𝑜} \leftrightarrow X = \{A\})$
5	1 2	rngosn3	$⊢ (R \in RingOps \land A \in X) \to (X = \{A\} \leftrightarrow R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩)$
6	4 5	bitrd	$⊢ (R \in RingOps \land A \in X) \to (X \approx 1_{𝑜} \leftrightarrow R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩)$

Metamath Proof Explorer

Theorem rngosn4

Proof