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 syl5bb
 |-  ( ( R e. Domn /\ U e. L ) -> ( I e. Ring <-> ( U = { .0. } \/ U = B ) ) )