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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dflringlem2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dflringlem2.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
dflringlem2.2 ⊢ ( 𝜑 → 𝑅 ∈ LRing )
Assertion dflringlem3 ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ∈ ( MaxIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dflringlem2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dflringlem2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dflringlem2.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 dflringlem2.2 ⊢ ( 𝜑 → 𝑅 ∈ LRing )
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 3 5 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 1 2 3 4 dflringlem2 ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) )
8 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9 1 8 5 ringidcld ⊢ ( 𝑅 ∈ CRing → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
10 3 9 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
11 2 8 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
12 6 11 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
13 elndif ⊢ ( ( 1r ‘ 𝑅 ) ∈ 𝑈 → ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑈 ) )
14 12 13 syl ⊢ ( 𝜑 → ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑈 ) )
15 nelne1 ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝐵 ≠ ( 𝐵 ∖ 𝑈 ) )
16 10 14 15 syl2anc ⊢ ( 𝜑 → 𝐵 ≠ ( 𝐵 ∖ 𝑈 ) )
17 16 necomd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ≠ 𝐵 )
18 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
19 1 18 lidlss ⊢ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) → 𝑗 ⊆ 𝐵 )
20 19 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → 𝑗 ⊆ 𝐵 )
21 ssdif0 ⊢ ( 𝑗 ⊆ 𝐵 ↔ ( 𝑗 ∖ 𝐵 ) = ∅ )
22 20 21 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( 𝑗 ∖ 𝐵 ) = ∅ )
23 22 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( ( 𝑗 ∖ 𝐵 ) ∪ ( 𝑗 ∩ 𝑈 ) ) = ( ∅ ∪ ( 𝑗 ∩ 𝑈 ) ) )
24 0un ⊢ ( ∅ ∪ ( 𝑗 ∩ 𝑈 ) ) = ( 𝑗 ∩ 𝑈 )
25 23 24 eqtr2di ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( 𝑗 ∩ 𝑈 ) = ( ( 𝑗 ∖ 𝐵 ) ∪ ( 𝑗 ∩ 𝑈 ) ) )
26 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 )
27 neqne ⊢ ( ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) → 𝑗 ≠ ( 𝐵 ∖ 𝑈 ) )
28 27 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → 𝑗 ≠ ( 𝐵 ∖ 𝑈 ) )
29 28 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( 𝐵 ∖ 𝑈 ) ≠ 𝑗 )
30 difdif2 ⊢ ( 𝑗 ∖ ( 𝐵 ∖ 𝑈 ) ) = ( ( 𝑗 ∖ 𝐵 ) ∪ ( 𝑗 ∩ 𝑈 ) )
31 pssdifn0 ⊢ ( ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ∧ ( 𝐵 ∖ 𝑈 ) ≠ 𝑗 ) → ( 𝑗 ∖ ( 𝐵 ∖ 𝑈 ) ) ≠ ∅ )
32 30 31 eqnetrrid ⊢ ( ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ∧ ( 𝐵 ∖ 𝑈 ) ≠ 𝑗 ) → ( ( 𝑗 ∖ 𝐵 ) ∪ ( 𝑗 ∩ 𝑈 ) ) ≠ ∅ )
33 26 29 32 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( ( 𝑗 ∖ 𝐵 ) ∪ ( 𝑗 ∩ 𝑈 ) ) ≠ ∅ )
34 25 33 eqnetrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → ( 𝑗 ∩ 𝑈 ) ≠ ∅ )
35 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) )
36 35 elin2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
37 35 elin1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑥 ∈ 𝑗 )
38 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑅 ∈ Ring )
39 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
40 1 2 36 37 38 39 lidlunitel ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ( 𝑗 ∩ 𝑈 ) ) → 𝑗 = 𝐵 )
41 34 40 n0limd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) ∧ ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) ) → 𝑗 = 𝐵 )
42 41 ex ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) → ( ¬ 𝑗 = ( 𝐵 ∖ 𝑈 ) → 𝑗 = 𝐵 ) )
43 42 orrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 ) → ( 𝑗 = ( 𝐵 ∖ 𝑈 ) ∨ 𝑗 = 𝐵 ) )
44 43 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 → ( 𝑗 = ( 𝐵 ∖ 𝑈 ) ∨ 𝑗 = 𝐵 ) ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 → ( 𝑗 = ( 𝐵 ∖ 𝑈 ) ∨ 𝑗 = 𝐵 ) ) )
46 1 ismxidl ⊢ ( 𝑅 ∈ Ring → ( ( 𝐵 ∖ 𝑈 ) ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝐵 ∖ 𝑈 ) ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 → ( 𝑗 = ( 𝐵 ∖ 𝑈 ) ∨ 𝑗 = 𝐵 ) ) ) ) )
47 46 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝐵 ∖ 𝑈 ) ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝑗 → ( 𝑗 = ( 𝐵 ∖ 𝑈 ) ∨ 𝑗 = 𝐵 ) ) ) ) → ( 𝐵 ∖ 𝑈 ) ∈ ( MaxIdeal ‘ 𝑅 ) )
48 6 7 17 45 47 syl13anc ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ∈ ( MaxIdeal ‘ 𝑅 ) )