Theorem ridl1

Description: Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	ridl0.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
	ridl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	ridl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ridl0.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
2		ridl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
4	3	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
5	3 2	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
6	1 5	lidl1	⊢ ( ( oppr ‘ 𝑅 ) ∈ Ring → 𝐵 ∈ 𝑈 )
7	4 6	syl	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )