Theorem 2idllidld

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

	Ref	Expression
Hypothesis	2idllidld.1	|- ( ph -> I e. ( 2Ideal ` R ) )
Assertion	2idllidld	|- ( ph -> I e. ( LIdeal ` R ) )

Proof

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