Metamath Proof Explorer

Theorem dflring3

Description: Alternate definition of a local ring: local rings have a single maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Assertion dflring3 ( 𝑅 ∈ CRing → ( 𝑅 ∈ LRing ↔ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) )

Proof

Step Hyp Ref Expression
1 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
2 1 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → 𝑅 ∈ Ring )
3 2 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
4 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → 𝑅 ∈ CRing )
8 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → 𝑅 ∈ LRing )
9 5 6 7 8 dflringlem2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
10 9 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∈ ( LIdeal ‘ 𝑅 ) )
11 5 mxidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
12 2 11 sylan ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
13 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
14 5 13 lidlss ⊢ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) → 𝑚 ⊆ ( Base ‘ 𝑅 ) )
15 12 14 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ⊆ ( Base ‘ 𝑅 ) )
16 15 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 ⊆ ( Base ‘ 𝑅 ) )
17 16 sselda ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
18 neldif ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
19 17 18 sylan ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
20 simplr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑥 ∈ 𝑚 )
21 2 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
22 12 ad3antrrr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
23 5 6 19 20 21 22 lidlunitel ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 = ( Base ‘ 𝑅 ) )
24 nssrex ⊢ ( ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ↔ ∃ 𝑥 ∈ 𝑚 ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
25 24 bilani ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → ∃ 𝑥 ∈ 𝑚 ¬ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
26 23 25 r19.29a ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 = ( Base ‘ 𝑅 ) )
27 2 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
28 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
29 5 mxidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ≠ ( Base ‘ 𝑅 ) )
30 27 28 29 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → 𝑚 ≠ ( Base ‘ 𝑅 ) )
31 30 neneqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ¬ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → ¬ 𝑚 = ( Base ‘ 𝑅 ) )
32 26 31 condan ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
33 5 mxidlmax ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ⊆ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ) → ( ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = 𝑚 ∨ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( Base ‘ 𝑅 ) ) )
34 3 4 10 32 33 syl22anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = 𝑚 ∨ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( Base ‘ 𝑅 ) ) )
35 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
36 5 35 1 ringidcld ⊢ ( 𝑅 ∈ CRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
37 36 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
38 6 35 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
39 elndif ⊢ ( ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) → ¬ ( 1r ‘ 𝑅 ) ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
40 2 38 39 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ¬ ( 1r ‘ 𝑅 ) ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
41 nelne1 ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ¬ ( 1r ‘ 𝑅 ) ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → ( Base ‘ 𝑅 ) ≠ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
42 37 40 41 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( Base ‘ 𝑅 ) ≠ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
43 42 necomd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ≠ ( Base ‘ 𝑅 ) )
44 43 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ≠ ( Base ‘ 𝑅 ) )
45 44 neneqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( Base ‘ 𝑅 ) )
46 34 45 olcnd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = 𝑚 )
47 46 eqcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑚 = ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
48 5 6 7 8 dflringlem3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∈ ( MaxIdeal ‘ 𝑅 ) )
49 47 48 eqsnd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( MaxIdeal ‘ 𝑅 ) = { ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) } )
50 ensn1g ⊢ ( ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∈ ( LIdeal ‘ 𝑅 ) → { ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) } ≈ 1o )
51 9 50 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → { ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) } ≈ 1o )
52 49 51 eqbrtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ LRing ) → ( MaxIdeal ‘ 𝑅 ) ≈ 1o )
53 en1 ⊢ ( ( MaxIdeal ‘ 𝑅 ) ≈ 1o ↔ ∃ 𝑚 ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } )
54 53 bilani ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) → ∃ 𝑚 ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } )
55 1 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → 𝑅 ∈ Ring )
56 vsnid ⊢ 𝑚 ∈ { 𝑚 }
57 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } )
58 56 57 eleqtrrid ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
59 5 mxidlnzr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
60 55 58 59 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → 𝑅 ∈ NzRing )
61 simplll ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → 𝑅 ∈ CRing )
62 58 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
63 57 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } )
64 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
65 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → ¬ 𝑥 ∈ 𝑚 )
66 64 65 eldifd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑚 ) )
67 5 6 61 62 63 66 dflringlem ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ ¬ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
68 simplll ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑅 ∈ CRing )
69 58 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
70 57 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } )
71 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
72 1 ringgrpd ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
73 72 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑅 ∈ Grp )
74 36 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
75 simplr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
76 5 71 73 74 75 grpsubcld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
77 55 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → 𝑅 ∈ Ring )
78 5 35 mxidln1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑚 )
79 77 69 78 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑚 )
80 73 adantr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑅 ∈ Grp )
81 74 adantr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
82 75 adantr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
83 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
84 5 83 71 grpnpcan ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
85 80 81 82 84 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → ( ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
86 77 adantr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑅 ∈ Ring )
87 69 adantr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
88 86 87 11 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
89 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 )
90 simplr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → 𝑥 ∈ 𝑚 )
91 13 83 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ∧ 𝑥 ∈ 𝑚 ) ) → ( ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 )
92 86 88 89 90 91 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → ( ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 )
93 85 92 eqeltrrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) ∧ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 ) → ( 1r ‘ 𝑅 ) ∈ 𝑚 )
94 79 93 mtand ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ¬ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝑚 )
95 76 94 eldifd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑚 ) )
96 5 6 68 69 70 95 dflringlem ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑚 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) )
97 exmidd ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑚 ∨ ¬ 𝑥 ∈ 𝑚 ) )
98 97 orcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ¬ 𝑥 ∈ 𝑚 ∨ 𝑥 ∈ 𝑚 ) )
99 67 96 98 orim12da ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) )
100 99 ralrimiva ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) )
101 60 100 jca ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) ) )
102 101 adantlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) ∧ ( MaxIdeal ‘ 𝑅 ) = { 𝑚 } ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) ) )
103 54 102 exlimddv ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) ) )
104 5 6 35 71 dflring2 ⊢ ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∨ ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) 𝑥 ) ∈ ( Unit ‘ 𝑅 ) ) ) )
105 103 104 sylibr ⊢ ( ( 𝑅 ∈ CRing ∧ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) → 𝑅 ∈ LRing )
106 52 105 impbida ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ LRing ↔ ( MaxIdeal ‘ 𝑅 ) ≈ 1o ) )