Theorem 2idlridld

Description: A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	2idllidld.1	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	2idlridld.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	2idlridld	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		2idllidld.1	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
2		2idlridld.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
3		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4		eqid	⊢ ( LIdeal ‘ 𝑂 ) = ( LIdeal ‘ 𝑂 )
5		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
6	3 2 4 5	2idlval	⊢ ( 2Ideal ‘ 𝑅 ) = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) )
7	1 6	eleqtrdi	⊢ ( 𝜑 → 𝐼 ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) )
8	7	elin2d	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑂 ) )