Metamath Proof Explorer

Theorem zlidlring

Description: The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses lidlabl.l 
|- L = ( LIdeal ` R )
lidlabl.i 
|- I = ( R |`s U )
zlidlring.b 
|- B = ( Base ` R )
zlidlring.0 
|- .0. = ( 0g ` R )
Assertion zlidlring 
|- ( ( R e. Ring /\ U = { .0. } ) -> I e. Ring )

Proof

Step Hyp Ref Expression
1 lidlabl.l 
 |-  L = ( LIdeal ` R )
2 lidlabl.i 
 |-  I = ( R |`s U )
3 zlidlring.b 
 |-  B = ( Base ` R )
4 zlidlring.0 
 |-  .0. = ( 0g ` R )
5 1 4 lidl0 
 |-  ( R e. Ring -> { .0. } e. L )
6 5 adantr 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> { .0. } e. L )
7 eleq1 
 |-  ( U = { .0. } -> ( U e. L <-> { .0. } e. L ) )
8 7 adantl 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> ( U e. L <-> { .0. } e. L ) )
9 6 8 mpbird 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> U e. L )
10 1 2 lidlrng 
 |-  ( ( R e. Ring /\ U e. L ) -> I e. Rng )
11 9 10 syldan 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> I e. Rng )
12 eleq1 
 |-  ( { .0. } = U -> ( { .0. } e. L <-> U e. L ) )
13 12 eqcoms 
 |-  ( U = { .0. } -> ( { .0. } e. L <-> U e. L ) )
14 13 adantl 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> ( { .0. } e. L <-> U e. L ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 15 4 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 15 17 4 ringlz 
 |-  ( ( R e. Ring /\ .0. e. ( Base ` R ) ) -> ( .0. ( .r ` R ) .0. ) = .0. )
19 18 18 jca 
 |-  ( ( R e. Ring /\ .0. e. ( Base ` R ) ) -> ( ( .0. ( .r ` R ) .0. ) = .0. /\ ( .0. ( .r ` R ) .0. ) = .0. ) )
20 16 19 mpdan 
 |-  ( R e. Ring -> ( ( .0. ( .r ` R ) .0. ) = .0. /\ ( .0. ( .r ` R ) .0. ) = .0. ) )
21 4 fvexi 
 |-  .0. e. _V
22 oveq2 
 |-  ( y = .0. -> ( .0. ( .r ` R ) y ) = ( .0. ( .r ` R ) .0. ) )
23 id 
 |-  ( y = .0. -> y = .0. )
24 22 23 eqeq12d 
 |-  ( y = .0. -> ( ( .0. ( .r ` R ) y ) = y <-> ( .0. ( .r ` R ) .0. ) = .0. ) )
25 oveq1 
 |-  ( y = .0. -> ( y ( .r ` R ) .0. ) = ( .0. ( .r ` R ) .0. ) )
26 25 23 eqeq12d 
 |-  ( y = .0. -> ( ( y ( .r ` R ) .0. ) = y <-> ( .0. ( .r ` R ) .0. ) = .0. ) )
27 24 26 anbi12d 
 |-  ( y = .0. -> ( ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) <-> ( ( .0. ( .r ` R ) .0. ) = .0. /\ ( .0. ( .r ` R ) .0. ) = .0. ) ) )
28 27 ralsng 
 |-  ( .0. e. _V -> ( A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) <-> ( ( .0. ( .r ` R ) .0. ) = .0. /\ ( .0. ( .r ` R ) .0. ) = .0. ) ) )
29 21 28 mp1i 
 |-  ( R e. Ring -> ( A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) <-> ( ( .0. ( .r ` R ) .0. ) = .0. /\ ( .0. ( .r ` R ) .0. ) = .0. ) ) )
30 20 29 mpbird 
 |-  ( R e. Ring -> A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) )
31 oveq1 
 |-  ( x = .0. -> ( x ( .r ` R ) y ) = ( .0. ( .r ` R ) y ) )
32 31 eqeq1d 
 |-  ( x = .0. -> ( ( x ( .r ` R ) y ) = y <-> ( .0. ( .r ` R ) y ) = y ) )
33 32 ovanraleqv 
 |-  ( x = .0. -> ( A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) <-> A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) ) )
34 33 rexsng 
 |-  ( .0. e. _V -> ( E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) <-> A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) ) )
35 21 34 mp1i 
 |-  ( R e. Ring -> ( E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) <-> A. y e. { .0. } ( ( .0. ( .r ` R ) y ) = y /\ ( y ( .r ` R ) .0. ) = y ) ) )
36 30 35 mpbird 
 |-  ( R e. Ring -> E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
37 36 adantr 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
38 37 adantr 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
39 1 2 lidlbas 
 |-  ( U e. L -> ( Base ` I ) = U )
40 simpr 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> U = { .0. } )
41 39 40 sylan9eqr 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( Base ` I ) = { .0. } )
42 2 17 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
43 42 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
44 43 adantl 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( .r ` I ) = ( .r ` R ) )
45 44 oveqd 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( x ( .r ` I ) y ) = ( x ( .r ` R ) y ) )
46 45 eqeq1d 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( ( x ( .r ` I ) y ) = y <-> ( x ( .r ` R ) y ) = y ) )
47 44 oveqd 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( y ( .r ` I ) x ) = ( y ( .r ` R ) x ) )
48 47 eqeq1d 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( ( y ( .r ` I ) x ) = y <-> ( y ( .r ` R ) x ) = y ) )
49 46 48 anbi12d 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
50 41 49 raleqbidv 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
51 41 50 rexeqbidv 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> E. x e. { .0. } A. y e. { .0. } ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
52 38 51 mpbird 
 |-  ( ( ( R e. Ring /\ U = { .0. } ) /\ U e. L ) -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) )
53 52 ex 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> ( U e. L -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
54 14 53 sylbid 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> ( { .0. } e. L -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
55 6 54 mpd 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) )
56 eqid 
 |-  ( Base ` I ) = ( Base ` I )
57 eqid 
 |-  ( .r ` I ) = ( .r ` I )
58 56 57 isringrng 
 |-  ( I e. Ring <-> ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
59 11 55 58 sylanbrc 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> I e. Ring )