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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dflring4.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion dflring4 ( 𝑅 ∈ CRing → ( 𝑅 ∈ LRing ↔ ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) ) )

Proof

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