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

Metamath Proof Explorer

Theorem rnglidl0

Description: Every non-unital ring contains a zero ideal. (Contributed by AV, 19-Feb-2025)

Ref Expression
Hypotheses rnglidl0.u 
|- U = ( LIdeal ` R )
rnglidl0.z 
|- .0. = ( 0g ` R )
Assertion rnglidl0 
|- ( R e. Rng -> { .0. } e. U )

Proof

Step Hyp Ref Expression
1 rnglidl0.u 
 |-  U = ( LIdeal ` R )
2 rnglidl0.z 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 2 rng0cl 
 |-  ( R e. Rng -> .0. e. ( Base ` R ) )
5 4 snssd 
 |-  ( R e. Rng -> { .0. } C_ ( Base ` R ) )
6 2 fvexi 
 |-  .0. e. _V
7 6 a1i 
 |-  ( R e. Rng -> .0. e. _V )
8 7 snn0d 
 |-  ( R e. Rng -> { .0. } =/= (/) )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 3 9 2 rngrz 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) .0. ) = .0. )
11 10 oveq1d 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) = ( .0. ( +g ` R ) .0. ) )
12 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
13 3 2 grpidcl 
 |-  ( R e. Grp -> .0. e. ( Base ` R ) )
14 eqid 
 |-  ( +g ` R ) = ( +g ` R )
15 3 14 2 grprid 
 |-  ( ( R e. Grp /\ .0. e. ( Base ` R ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
16 12 13 15 syl2anc2 
 |-  ( R e. Rng -> ( .0. ( +g ` R ) .0. ) = .0. )
17 16 adantr 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) .0. ) = .0. )
18 11 17 eqtrd 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) = .0. )
19 6 elsn2 
 |-  ( ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) e. { .0. } <-> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) = .0. )
20 18 19 sylibr 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) e. { .0. } )
21 oveq2 
 |-  ( y = .0. -> ( x ( .r ` R ) y ) = ( x ( .r ` R ) .0. ) )
22 21 oveq1d 
 |-  ( y = .0. -> ( ( x ( .r ` R ) y ) ( +g ` R ) z ) = ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) )
23 22 eleq1d 
 |-  ( y = .0. -> ( ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } <-> ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) e. { .0. } ) )
24 23 ralbidv 
 |-  ( y = .0. -> ( A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } <-> A. z e. { .0. } ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) e. { .0. } ) )
25 6 24 ralsn 
 |-  ( A. y e. { .0. } A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } <-> A. z e. { .0. } ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) e. { .0. } )
26 oveq2 
 |-  ( z = .0. -> ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) = ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) )
27 26 eleq1d 
 |-  ( z = .0. -> ( ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) e. { .0. } <-> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) e. { .0. } ) )
28 6 27 ralsn 
 |-  ( A. z e. { .0. } ( ( x ( .r ` R ) .0. ) ( +g ` R ) z ) e. { .0. } <-> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) e. { .0. } )
29 25 28 bitri 
 |-  ( A. y e. { .0. } A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } <-> ( ( x ( .r ` R ) .0. ) ( +g ` R ) .0. ) e. { .0. } )
30 20 29 sylibr 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) ) -> A. y e. { .0. } A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } )
31 30 ralrimiva 
 |-  ( R e. Rng -> A. x e. ( Base ` R ) A. y e. { .0. } A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } )
32 1 3 14 9 islidl 
 |-  ( { .0. } e. U <-> ( { .0. } C_ ( Base ` R ) /\ { .0. } =/= (/) /\ A. x e. ( Base ` R ) A. y e. { .0. } A. z e. { .0. } ( ( x ( .r ` R ) y ) ( +g ` R ) z ) e. { .0. } ) )
33 5 8 31 32 syl3anbrc 
 |-  ( R e. Rng -> { .0. } e. U )