Metamath Proof Explorer

Theorem dflringlem3

Description: Lemma for dflring3 . In a commutative local ring R , the set ( B \ U ) of non-units is a maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypotheses dflringlem2.b 
|- B = ( Base ` R )
dflringlem2.u 
|- U = ( Unit ` R )
dflringlem2.1 
|- ( ph -> R e. CRing )
dflringlem2.2 
|- ( ph -> R e. LRing )
Assertion dflringlem3 
|- ( ph -> ( B \ U ) e. ( MaxIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 dflringlem2.b 
 |-  B = ( Base ` R )
2 dflringlem2.u 
 |-  U = ( Unit ` R )
3 dflringlem2.1 
 |-  ( ph -> R e. CRing )
4 dflringlem2.2 
 |-  ( ph -> R e. LRing )
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 3 5 syl 
 |-  ( ph -> R e. Ring )
7 1 2 3 4 dflringlem2 
 |-  ( ph -> ( B \ U ) e. ( LIdeal ` R ) )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 1 8 5 ringidcld 
 |-  ( R e. CRing -> ( 1r ` R ) e. B )
10 3 9 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
11 2 8 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
12 6 11 syl 
 |-  ( ph -> ( 1r ` R ) e. U )
13 elndif 
 |-  ( ( 1r ` R ) e. U -> -. ( 1r ` R ) e. ( B \ U ) )
14 12 13 syl 
 |-  ( ph -> -. ( 1r ` R ) e. ( B \ U ) )
15 nelne1 
 |-  ( ( ( 1r ` R ) e. B /\ -. ( 1r ` R ) e. ( B \ U ) ) -> B =/= ( B \ U ) )
16 10 14 15 syl2anc 
 |-  ( ph -> B =/= ( B \ U ) )
17 16 necomd 
 |-  ( ph -> ( B \ U ) =/= B )
18 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
19 1 18 lidlss 
 |-  ( j e. ( LIdeal ` R ) -> j C_ B )
20 19 ad3antlr 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j C_ B )
21 ssdif0 
 |-  ( j C_ B <-> ( j \ B ) = (/) )
22 20 21 sylib 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j \ B ) = (/) )
23 22 uneq1d 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( ( j \ B ) u. ( j i^i U ) ) = ( (/) u. ( j i^i U ) ) )
24 0un 
 |-  ( (/) u. ( j i^i U ) ) = ( j i^i U )
25 23 24 eqtr2di 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j i^i U ) = ( ( j \ B ) u. ( j i^i U ) ) )
26 simplr 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( B \ U ) C_ j )
27 neqne 
 |-  ( -. j = ( B \ U ) -> j =/= ( B \ U ) )
28 27 adantl 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j =/= ( B \ U ) )
29 28 necomd 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( B \ U ) =/= j )
30 difdif2 
 |-  ( j \ ( B \ U ) ) = ( ( j \ B ) u. ( j i^i U ) )
31 pssdifn0 
 |-  ( ( ( B \ U ) C_ j /\ ( B \ U ) =/= j ) -> ( j \ ( B \ U ) ) =/= (/) )
32 30 31 eqnetrrid 
 |-  ( ( ( B \ U ) C_ j /\ ( B \ U ) =/= j ) -> ( ( j \ B ) u. ( j i^i U ) ) =/= (/) )
33 26 29 32 syl2anc 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( ( j \ B ) u. ( j i^i U ) ) =/= (/) )
34 25 33 eqnetrd 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> ( j i^i U ) =/= (/) )
35 simpr 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. ( j i^i U ) )
36 35 elin2d 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. U )
37 35 elin1d 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> x e. j )
38 6 ad4antr 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> R e. Ring )
39 simp-4r 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> j e. ( LIdeal ` R ) )
40 1 2 36 37 38 39 lidlunitel 
 |-  ( ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) /\ x e. ( j i^i U ) ) -> j = B )
41 34 40 n0limd 
 |-  ( ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) /\ -. j = ( B \ U ) ) -> j = B )
42 41 ex 
 |-  ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) -> ( -. j = ( B \ U ) -> j = B ) )
43 42 orrd 
 |-  ( ( ( ph /\ j e. ( LIdeal ` R ) ) /\ ( B \ U ) C_ j ) -> ( j = ( B \ U ) \/ j = B ) )
44 43 ex 
 |-  ( ( ph /\ j e. ( LIdeal ` R ) ) -> ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) )
45 44 ralrimiva 
 |-  ( ph -> A. j e. ( LIdeal ` R ) ( ( B \ U ) C_ j -> ( j = ( B \ U ) \/ j = B ) ) )
46 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 ) ) ) ) )
47 46 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 ) )
48 6 7 17 45 47 syl13anc 
 |-  ( ph -> ( B \ U ) e. ( MaxIdeal ` R ) )