Theorem 2idl1el

Description: A two-sided ideal contains 1 iff it is the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 24-Aug-2026)

	Ref	Expression
Hypotheses	2idl1el.u	|- U = ( 2Ideal ` R )
	2idl1el.b	|- B = ( Base ` R )
	2idl1el.o	|- .1. = ( 1r ` R )
Assertion	2idl1el	|- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )

Proof

Step	Hyp	Ref	Expression
1		2idl1el.u	|- U = ( 2Ideal ` R )
2		2idl1el.b	|- B = ( Base ` R )
3		2idl1el.o	|- .1. = ( 1r ` R )
4	1	eleq2i	|- ( I e. U <-> I e. ( 2Ideal ` R ) )
5	4	biimpi	|- ( I e. U -> I e. ( 2Ideal ` R ) )
6	5	2idllidld	|- ( I e. U -> I e. ( LIdeal ` R ) )
7		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
8	7 2 3	lidl1el	|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> ( .1. e. I <-> I = B ) )
9	6 8	sylan2	|- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )