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

Metamath Proof Explorer

Theorem 2idl0

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

Ref Expression
Hypotheses 2idl0.u 
|- I = ( 2Ideal ` R )
2idl0.z 
|- .0. = ( 0g ` R )
Assertion 2idl0 
|- ( R e. Ring -> { .0. } e. I )

Proof

Step Hyp Ref Expression
1 2idl0.u 
 |-  I = ( 2Ideal ` R )
2 2idl0.z 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
4 3 2 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
5 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
6 5 2 ridl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` ( oppR ` R ) ) )
7 4 6 elind 
 |-  ( R e. Ring -> { .0. } 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 -> { .0. } e. I )