Theorem rngosn6

Description: Obsolete as of 25-Jan-2020. Use ringen1zr0 or srgen1zr0 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		on1el3.2	⊢ 𝑋 = ran 𝐺
3		on1el3.3	⊢ 𝑍 = ( GId ‘ 𝐺 )
4	1 2 3	rngo0cl	⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ 𝑋 )
5	1 2	rngosn4	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑍 ∈ 𝑋 ) → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ) )
6	4 5	mpdan	⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ) )