Metamath Proof Explorer

Theorem 2idlelbas

Description: The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025)

Ref Expression
Hypotheses 2idlbas.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
2idlbas.j 
|- J = ( R |`s I )
2idlbas.b 
|- B = ( Base ` J )
Assertion 2idlelbas 
|- ( ph -> ( B e. ( LIdeal ` R ) /\ B e. ( LIdeal ` ( oppR ` R ) ) ) )

Proof

Step Hyp Ref Expression
1 2idlbas.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
2 2idlbas.j 
 |-  J = ( R |`s I )
3 2idlbas.b 
 |-  B = ( Base ` J )
4 1 2 3 2idlbas 
 |-  ( ph -> B = I )
5 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
6 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
7 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
8 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
9 5 6 7 8 2idlelb 
 |-  ( I e. ( 2Ideal ` R ) <-> ( I e. ( LIdeal ` R ) /\ I e. ( LIdeal ` ( oppR ` R ) ) ) )
10 9 simplbi 
 |-  ( I e. ( 2Ideal ` R ) -> I e. ( LIdeal ` R ) )
11 1 10 syl 
 |-  ( ph -> I e. ( LIdeal ` R ) )
12 4 11 eqeltrd 
 |-  ( ph -> B e. ( LIdeal ` R ) )
13 9 simprbi 
 |-  ( I e. ( 2Ideal ` R ) -> I e. ( LIdeal ` ( oppR ` R ) ) )
14 1 13 syl 
 |-  ( ph -> I e. ( LIdeal ` ( oppR ` R ) ) )
15 4 14 eqeltrd 
 |-  ( ph -> B e. ( LIdeal ` ( oppR ` R ) ) )
16 12 15 jca 
 |-  ( ph -> ( B e. ( LIdeal ` R ) /\ B e. ( LIdeal ` ( oppR ` R ) ) ) )