Metamath Proof Explorer

Theorem dflring4

Description: Alternate definition of a local ring: the set ( B \ U ) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypotheses dflring4.b 
|- B = ( Base ` R )
dflring4.u 
|- U = ( Unit ` R )
Assertion dflring4 
|- ( R e. CRing -> ( R e. LRing <-> ( B \ U ) e. ( LIdeal ` R ) ) )

Proof

Step Hyp Ref Expression
1 dflring4.b 
 |-  B = ( Base ` R )
2 dflring4.u 
 |-  U = ( Unit ` R )
3 simpl 
 |-  ( ( R e. CRing /\ R e. LRing ) -> R e. CRing )
4 simpr 
 |-  ( ( R e. CRing /\ R e. LRing ) -> R e. LRing )
5 1 2 3 4 dflringlem2 
 |-  ( ( R e. CRing /\ R e. LRing ) -> ( B \ U ) e. ( LIdeal ` R ) )
6 simpl 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> R e. CRing )
7 6 crngringd 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> R e. Ring )
8 7 adantr 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> R e. Ring )
9 simpr 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> m e. ( MaxIdeal ` R ) )
10 simplr 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> ( B \ U ) e. ( LIdeal ` R ) )
11 1 mxidlidl 
 |-  ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> m e. ( LIdeal ` R ) )
12 7 11 sylan 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> m e. ( LIdeal ` R ) )
13 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
14 1 13 lidlss 
 |-  ( m e. ( LIdeal ` R ) -> m C_ B )
15 12 14 syl 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> m C_ B )
16 15 adantr 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> m C_ B )
17 16 sselda 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) -> x e. B )
18 neldif 
 |-  ( ( x e. B /\ -. x e. ( B \ U ) ) -> x e. U )
19 17 18 sylan 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) /\ -. x e. ( B \ U ) ) -> x e. U )
20 simplr 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) /\ -. x e. ( B \ U ) ) -> x e. m )
21 8 ad3antrrr 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) /\ -. x e. ( B \ U ) ) -> R e. Ring )
22 12 ad3antrrr 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) /\ -. x e. ( B \ U ) ) -> m e. ( LIdeal ` R ) )
23 1 2 19 20 21 22 lidlunitel 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) /\ x e. m ) /\ -. x e. ( B \ U ) ) -> m = B )
24 nssrex 
 |-  ( -. m C_ ( B \ U ) <-> E. x e. m -. x e. ( B \ U ) )
25 24 bilani 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> E. x e. m -. x e. ( B \ U ) )
26 23 25 r19.29a 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> m = B )
27 8 adantr 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> R e. Ring )
28 simplr 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> m e. ( MaxIdeal ` R ) )
29 1 mxidlnr 
 |-  ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> m =/= B )
30 27 28 29 syl2anc 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> m =/= B )
31 30 neneqd 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ -. m C_ ( B \ U ) ) -> -. m = B )
32 26 31 condan 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> m C_ ( B \ U ) )
33 1 mxidlmax 
 |-  ( ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) /\ ( ( B \ U ) e. ( LIdeal ` R ) /\ m C_ ( B \ U ) ) ) -> ( ( B \ U ) = m \/ ( B \ U ) = B ) )
34 8 9 10 32 33 syl22anc 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> ( ( B \ U ) = m \/ ( B \ U ) = B ) )
35 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
36 1 35 7 ringidcld 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( 1r ` R ) e. B )
37 2 35 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
38 7 37 syl 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( 1r ` R ) e. U )
39 elndif 
 |-  ( ( 1r ` R ) e. U -> -. ( 1r ` R ) e. ( B \ U ) )
40 38 39 syl 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> -. ( 1r ` R ) e. ( B \ U ) )
41 nelne1 
 |-  ( ( ( 1r ` R ) e. B /\ -. ( 1r ` R ) e. ( B \ U ) ) -> B =/= ( B \ U ) )
42 36 40 41 syl2anc 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> B =/= ( B \ U ) )
43 42 necomd 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( B \ U ) =/= B )
44 43 adantr 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> ( B \ U ) =/= B )
45 44 neneqd 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> -. ( B \ U ) = B )
46 34 45 olcnd 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> ( B \ U ) = m )
47 46 eqcomd 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ m e. ( MaxIdeal ` R ) ) -> m = ( B \ U ) )
48 simpr 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( B \ U ) e. ( LIdeal ` R ) )
49 1 13 lidlss 
 |-  ( j e. ( LIdeal ` R ) -> j C_ B )
50 49 ad3antlr 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j C_ B )
51 ssdif0 
 |-  ( j C_ B <-> ( j \ B ) = (/) )
52 50 51 sylib 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j \ B ) = (/) )
53 52 uneq1d 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( ( j \ B ) u. ( j i^i U ) ) = ( (/) u. ( j i^i U ) ) )
54 0un 
 |-  ( (/) u. ( j i^i U ) ) = ( j i^i U )
55 53 54 eqtr2di 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j i^i U ) = ( ( j \ B ) u. ( j i^i U ) ) )
56 simplr 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( B \ U ) C_ j )
57 neqne 
 |-  ( -. j = ( B \ U ) -> j =/= ( B \ U ) )
58 57 adantl 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j =/= ( B \ U ) )
59 58 necomd 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( B \ U ) =/= j )
60 difdif2 
 |-  ( j \ ( B \ U ) ) = ( ( j \ B ) u. ( j i^i U ) )
61 pssdifn0 
 |-  ( ( ( B \ U ) C_ j /\ ( B \ U ) =/= j ) -> ( j \ ( B \ U ) ) =/= (/) )
62 60 61 eqnetrrid 
 |-  ( ( ( B \ U ) C_ j /\ ( B \ U ) =/= j ) -> ( ( j \ B ) u. ( j i^i U ) ) =/= (/) )
63 56 59 62 syl2anc 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( ( j \ B ) u. ( j i^i U ) ) =/= (/) )
64 55 63 eqnetrd 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j i^i U ) =/= (/) )
65 simpr 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. ( j i^i U ) )
66 65 elin2d 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. U )
67 65 elin1d 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. j )
68 7 ad4antr 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> R e. Ring )
69 simp-4r 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> j e. ( LIdeal ` R ) )
70 1 2 66 67 68 69 lidlunitel 
 |-  ( ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> j = B )
71 64 70 n0limd 
 |-  ( ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j = B )
72 71 ex 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) -> ( -. j = ( B \ U ) -> j = B ) )
73 72 orrd 
 |-  ( ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) -> ( j = ( B \ U ) \/ j = B ) )
74 73 ex 
 |-  ( ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) /\ j e. ( LIdeal ` R ) ) -> ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) )
75 74 ralrimiva 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> A. j e. ( LIdeal ` R ) ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) )
76 1 ismxidl 
 |-  ( R e. Ring -> ( ( B \ U ) e. ( MaxIdeal ` R ) <-> ( ( B \ U ) e. ( LIdeal ` R ) /\ ( B \ U ) =/= B /\ A. j e. ( LIdeal ` R ) ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) ) ) )
77 76 biimpar 
 |-  ( ( R e. Ring /\ ( ( B \ U ) e. ( LIdeal ` R ) /\ ( B \ U ) =/= B /\ A. j e. ( LIdeal ` R ) ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) ) ) -> ( B \ U ) e. ( MaxIdeal ` R ) )
78 7 48 43 75 77 syl13anc 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( B \ U ) e. ( MaxIdeal ` R ) )
79 47 78 eqsnd 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( MaxIdeal ` R ) = { ( B \ U ) } )
80 1 fvexi 
 |-  B e. _V
81 80 a1i 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> B e. _V )
82 81 difexd 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( B \ U ) e. _V )
83 ensn1g 
 |-  ( ( B \ U ) e. _V -> { ( B \ U ) } ~~ 1o )
84 82 83 syl 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> { ( B \ U ) } ~~ 1o )
85 79 84 eqbrtrd 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> ( MaxIdeal ` R ) ~~ 1o )
86 dflring3 
 |-  ( R e. CRing -> ( R e. LRing <-> ( MaxIdeal ` R ) ~~ 1o ) )
87 86 biimpar 
 |-  ( ( R e. CRing /\ ( MaxIdeal ` R ) ~~ 1o ) -> R e. LRing )
88 6 85 87 syl2anc 
 |-  ( ( R e. CRing /\ ( B \ U ) e. ( LIdeal ` R ) ) -> R e. LRing )
89 5 88 impbida 
 |-  ( R e. CRing -> ( R e. LRing <-> ( B \ U ) e. ( LIdeal ` R ) ) )