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	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
	2idl1el.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	2idl1el.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	2idl1el	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		2idl1el.u	⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
2		2idl1el.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		2idl1el.o	⊢ 1 = ( 1r ‘ 𝑅 )
4	1	eleq2i	⊢ ( 𝐼 ∈ 𝑈 ↔ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
5	4	biimpi	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
6	5	2idllidld	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
8	7 2 3	lidl1el	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )
9	6 8	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )