Metamath Proof Explorer

Theorem uzlidlring

Description: Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-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 uzlidlring 
|- ( ( R e. Domn /\ U e. L ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )

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 eqid 
 |-  ( Base ` I ) = ( Base ` I )
6 eqid 
 |-  ( .r ` I ) = ( .r ` I )
7 5 6 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 ) ) )
8 domnring 
 |-  ( R e. Domn -> R e. Ring )
9 8 anim1i 
 |-  ( ( R e. Domn /\ U e. L ) -> ( R e. Ring /\ U e. L ) )
10 1 2 lidlrng 
 |-  ( ( R e. Ring /\ U e. L ) -> I e. Rng )
11 9 10 syl 
 |-  ( ( R e. Domn /\ U e. L ) -> I e. Rng )
12 ibar 
 |-  ( I e. Rng -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) ) )
13 12 bicomd 
 |-  ( I e. Rng -> ( ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) <-> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
14 13 adantl 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) <-> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 2 15 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
17 16 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
18 17 oveqd 
 |-  ( U e. L -> ( x ( .r ` I ) y ) = ( x ( .r ` R ) y ) )
19 18 eqeq1d 
 |-  ( U e. L -> ( ( x ( .r ` I ) y ) = y <-> ( x ( .r ` R ) y ) = y ) )
20 17 oveqd 
 |-  ( U e. L -> ( y ( .r ` I ) x ) = ( y ( .r ` R ) x ) )
21 20 eqeq1d 
 |-  ( U e. L -> ( ( y ( .r ` I ) x ) = y <-> ( y ( .r ` R ) x ) = y ) )
22 19 21 anbi12d 
 |-  ( U e. L -> ( ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
23 22 ad2antlr 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
24 23 ad2antrr 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> ( ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
25 24 ralbidv 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> A. y e. ( Base ` I ) ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
26 simp-4l 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> R e. Domn )
27 1 2 lidlbas 
 |-  ( U e. L -> ( Base ` I ) = U )
28 27 eleq1d 
 |-  ( U e. L -> ( ( Base ` I ) e. L <-> U e. L ) )
29 28 ibir 
 |-  ( U e. L -> ( Base ` I ) e. L )
30 29 ad3antlr 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( Base ` I ) e. L )
31 27 ad2antlr 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( Base ` I ) = U )
32 31 eqeq1d 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( Base ` I ) = { .0. } <-> U = { .0. } ) )
33 32 biimpd 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( Base ` I ) = { .0. } -> U = { .0. } ) )
34 33 necon3bd 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( -. U = { .0. } -> ( Base ` I ) =/= { .0. } ) )
35 34 imp 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( Base ` I ) =/= { .0. } )
36 30 35 jca 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( ( Base ` I ) e. L /\ ( Base ` I ) =/= { .0. } ) )
37 36 adantr 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> ( ( Base ` I ) e. L /\ ( Base ` I ) =/= { .0. } ) )
38 simpr 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> x e. ( Base ` I ) )
39 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
40 1 15 39 4 lidldomn1 
 |-  ( ( R e. Domn /\ ( ( Base ` I ) e. L /\ ( Base ` I ) =/= { .0. } ) /\ x e. ( Base ` I ) ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) -> x = ( 1r ` R ) ) )
41 26 37 38 40 syl3anc 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) -> x = ( 1r ` R ) ) )
42 25 41 sylbid 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) -> x = ( 1r ` R ) ) )
43 42 imp 
 |-  ( ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) /\ A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> x = ( 1r ` R ) )
44 27 ad3antlr 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( Base ` I ) = U )
45 44 eleq2d 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( x e. ( Base ` I ) <-> x e. U ) )
46 45 biimpd 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( x e. ( Base ` I ) -> x e. U ) )
47 46 imp 
 |-  ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) -> x e. U )
48 47 adantr 
 |-  ( ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) /\ A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> x e. U )
49 43 48 eqeltrrd 
 |-  ( ( ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) /\ x e. ( Base ` I ) ) /\ A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> ( 1r ` R ) e. U )
50 49 rexlimdva2 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ -. U = { .0. } ) -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) -> ( 1r ` R ) e. U ) )
51 50 impancom 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> ( -. U = { .0. } -> ( 1r ` R ) e. U ) )
52 9 adantr 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( R e. Ring /\ U e. L ) )
53 1 3 39 lidl1el 
 |-  ( ( R e. Ring /\ U e. L ) -> ( ( 1r ` R ) e. U <-> U = B ) )
54 52 53 syl 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( 1r ` R ) e. U <-> U = B ) )
55 54 adantr 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> ( ( 1r ` R ) e. U <-> U = B ) )
56 51 55 sylibd 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> ( -. U = { .0. } -> U = B ) )
57 56 orrd 
 |-  ( ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) -> ( U = { .0. } \/ U = B ) )
58 57 ex 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) -> ( U = { .0. } \/ U = B ) ) )
59 1 2 3 4 zlidlring 
 |-  ( ( R e. Ring /\ U = { .0. } ) -> I e. Ring )
60 7 simprbi 
 |-  ( I e. Ring -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) )
61 59 60 syl 
 |-  ( ( 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 ) )
62 61 ex 
 |-  ( 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 ) ) )
63 8 62 syl 
 |-  ( R e. Domn -> ( U = { .0. } -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
64 63 ad2antrr 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( U = { .0. } -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
65 9 anim1i 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) )
66 3 15 ringideu 
 |-  ( R e. Ring -> E! x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
67 reurex 
 |-  ( E! x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) -> E. x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
68 66 67 syl 
 |-  ( R e. Ring -> E. x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
69 68 adantr 
 |-  ( ( R e. Ring /\ U e. L ) -> E. x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
70 69 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> E. x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) )
71 2 3 ressbas 
 |-  ( U e. L -> ( U i^i B ) = ( Base ` I ) )
72 71 ad3antlr 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( U i^i B ) = ( Base ` I ) )
73 ineq1 
 |-  ( U = B -> ( U i^i B ) = ( B i^i B ) )
74 inidm 
 |-  ( B i^i B ) = B
75 73 74 eqtrdi 
 |-  ( U = B -> ( U i^i B ) = B )
76 75 adantl 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( U i^i B ) = B )
77 72 76 eqtr3d 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( Base ` I ) = B )
78 22 ad3antlr 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
79 77 78 raleqbidv 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
80 77 79 rexeqbidv 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> E. x e. B A. y e. B ( ( x ( .r ` R ) y ) = y /\ ( y ( .r ` R ) x ) = y ) ) )
81 70 80 mpbird 
 |-  ( ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) /\ U = B ) -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) )
82 81 ex 
 |-  ( ( ( R e. Ring /\ U e. L ) /\ I e. Rng ) -> ( U = B -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
83 65 82 syl 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( U = B -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
84 64 83 jaod 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( U = { .0. } \/ U = B ) -> E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) )
85 58 84 impbid 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) <-> ( U = { .0. } \/ U = B ) ) )
86 14 85 bitrd 
 |-  ( ( ( R e. Domn /\ U e. L ) /\ I e. Rng ) -> ( ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) <-> ( U = { .0. } \/ U = B ) ) )
87 11 86 mpdan 
 |-  ( ( R e. Domn /\ U e. L ) -> ( ( I e. Rng /\ E. x e. ( Base ` I ) A. y e. ( Base ` I ) ( ( x ( .r ` I ) y ) = y /\ ( y ( .r ` I ) x ) = y ) ) <-> ( U = { .0. } \/ U = B ) ) )
88 7 87 bitrid 
 |-  ( ( R e. Domn /\ U e. L ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )