Theorem lidl1

Description: Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	rnglidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	rnglidl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	lidl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		rnglidl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
4	1 2	rnglidl1	⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ 𝑈 )
5	3 4	syl	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )