Metamath Proof Explorer


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 ) )