Theorem ridl0

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

	Ref	Expression
Hypotheses	ridl0.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
	ridl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	ridl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ridl0.u	⊢ 𝑈 = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
2		ridl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
4	3	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
5	3 2	oppr0	⊢ 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) )
6	1 5	lidl0	⊢ ( ( oppr ‘ 𝑅 ) ∈ Ring → { 0 } ∈ 𝑈 )
7	4 6	syl	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )