Theorem 2idlridld

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

	Ref	Expression
Hypotheses	2idllidld.1	|- ( ph -> I e. ( 2Ideal ` R ) )
	2idlridld.o	|- O = ( oppR ` R )
Assertion	2idlridld	|- ( ph -> I e. ( LIdeal ` O ) )

Proof

Step	Hyp	Ref	Expression
1		2idllidld.1	|- ( ph -> I e. ( 2Ideal ` R ) )
2		2idlridld.o	|- O = ( oppR ` R )
3		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
4		eqid	|- ( LIdeal ` O ) = ( LIdeal ` O )
5		eqid	|- ( 2Ideal ` R ) = ( 2Ideal ` R )
6	3 2 4 5	2idlval	|- ( 2Ideal ` R ) = ( ( LIdeal ` R ) i^i ( LIdeal ` O ) )
7	1 6	eleqtrdi	|- ( ph -> I e. ( ( LIdeal ` R ) i^i ( LIdeal ` O ) ) )
8	7	elin2d	|- ( ph -> I e. ( LIdeal ` O ) )