This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2idl1

Description: Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025)

Ref Expression
Hypotheses 2idl0.u 
|- I = ( 2Ideal ` R )
2idl1.b 
|- B = ( Base ` R )
Assertion 2idl1 
|- ( R e. Ring -> B e. I )

Proof

Step Hyp Ref Expression
1 2idl0.u 
 |-  I = ( 2Ideal ` R )
2 2idl1.b 
 |-  B = ( Base ` R )
3 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
4 3 2 lidl1 
 |-  ( R e. Ring -> B e. ( LIdeal ` R ) )
5 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
6 5 2 ridl1 
 |-  ( R e. Ring -> B e. ( LIdeal ` ( oppR ` R ) ) )
7 4 6 elind 
 |-  ( R e. Ring -> B e. ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) ) )
8 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
9 3 8 5 1 2idlval 
 |-  I = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) )
10 7 9 eleqtrrdi 
 |-  ( R e. Ring -> B e. I )