Theorem rngosn6

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

	Ref	Expression
Hypotheses	on1el3.1	|- G = ( 1st ` R )
	on1el3.2	|- X = ran G
	on1el3.3	|- Z = ( GId ` G )
Assertion	rngosn6	|- ( R e. RingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	|- G = ( 1st ` R )
2		on1el3.2	|- X = ran G
3		on1el3.3	|- Z = ( GId ` G )
4	1 2 3	rngo0cl	|- ( R e. RingOps -> Z e. X )
5	1 2	rngosn4	|- ( ( R e. RingOps /\ Z e. X ) -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )
6	4 5	mpdan	|- ( R e. RingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )