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=\mathrm{2Ideal}\left(R\right)$$
	2idl1el.b	$$⊢B={\mathrm{Base}}_R$$
	2idl1el.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	2idl1el	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to \left(\underset{\dot{}}{1}\in I\leftrightarrow I=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		2idl1el.u	$$⊢U=\mathrm{2Ideal}\left(R\right)$$
2		2idl1el.b	$$⊢B={\mathrm{Base}}_R$$
3		2idl1el.o	$$⊢\underset{\dot{}}{1}=1_R$$
4	1	eleq2i	$$⊢I\in U\leftrightarrow I\in \mathrm{2Ideal}\left(R\right)$$
5	4	biimpi	$$⊢I\in U\to I\in \mathrm{2Ideal}\left(R\right)$$
6	5	2idllidld	$$⊢I\in U\to I\in \mathrm{LIdeal}\left(R\right)$$
7		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
8	7 2 3	lidl1el	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\underset{\dot{}}{1}\in I\leftrightarrow I=B\right)$$
9	6 8	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to \left(\underset{\dot{}}{1}\in I\leftrightarrow I=B\right)$$