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 
|- ( R e. CRing -> ( R e. LRing <-> ( MaxIdeal ` R ) ~~ 1o ) )

Proof

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