Theorem 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.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	on1el3.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	on1el3.2	⊢ 𝑋 = ran 𝐺
Assertion	rngosn4	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		on1el3.2	⊢ 𝑋 = ran 𝐺
3		en1eqsnbi	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑋 ≈ 1o ↔ 𝑋 = { 𝐴 } ) )
4	3	adantl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 ≈ 1o ↔ 𝑋 = { 𝐴 } ) )
5	1 2	rngosn3	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 = { 𝐴 } ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ) )
6	4 5	bitrd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ) )