Metamath Proof Explorer

Theorem dflringlem

Description: Lemma for dflring3 . If a ring R has a single maximal ideal M , then any element X outside of M is a unit. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypotheses dflringlem.b 
|- B = ( Base ` R )
dflringlem.u 
|- U = ( Unit ` R )
dflringlem.r 
|- ( ph -> R e. CRing )
dflringlem.m 
|- ( ph -> M e. ( MaxIdeal ` R ) )
dflringlem.1 
|- ( ph -> ( MaxIdeal ` R ) = { M } )
dflringlem.x 
|- ( ph -> X e. ( B \ M ) )
Assertion dflringlem 
|- ( ph -> X e. U )

Proof

Step Hyp Ref Expression
1 dflringlem.b 
 |-  B = ( Base ` R )
2 dflringlem.u 
 |-  U = ( Unit ` R )
3 dflringlem.r 
 |-  ( ph -> R e. CRing )
4 dflringlem.m 
 |-  ( ph -> M e. ( MaxIdeal ` R ) )
5 dflringlem.1 
 |-  ( ph -> ( MaxIdeal ` R ) = { M } )
6 dflringlem.x 
 |-  ( ph -> X e. ( B \ M ) )
7 4 adantr 
 |-  ( ( ph /\ -. X e. U ) -> M e. ( MaxIdeal ` R ) )
8 3 crngringd 
 |-  ( ph -> R e. Ring )
9 8 adantr 
 |-  ( ( ph /\ -. X e. U ) -> R e. Ring )
10 6 eldifad 
 |-  ( ph -> X e. B )
11 10 snssd 
 |-  ( ph -> { X } C_ B )
12 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
13 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
14 12 1 13 rspcl 
 |-  ( ( R e. Ring /\ { X } C_ B ) -> ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) )
15 8 11 14 syl2anc 
 |-  ( ph -> ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) )
16 15 adantr 
 |-  ( ( ph /\ -. X e. U ) -> ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) )
17 eqid 
 |-  ( ( RSpan ` R ) ` { X } ) = ( ( RSpan ` R ) ` { X } )
18 2 12 17 1 10 3 unitpidl1 
 |-  ( ph -> ( ( ( RSpan ` R ) ` { X } ) = B <-> X e. U ) )
19 18 notbid 
 |-  ( ph -> ( -. ( ( RSpan ` R ) ` { X } ) = B <-> -. X e. U ) )
20 19 biimpar 
 |-  ( ( ph /\ -. X e. U ) -> -. ( ( RSpan ` R ) ` { X } ) = B )
21 20 neqned 
 |-  ( ( ph /\ -. X e. U ) -> ( ( RSpan ` R ) ` { X } ) =/= B )
22 1 ssmxidl 
 |-  ( ( R e. Ring /\ ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) /\ ( ( RSpan ` R ) ` { X } ) =/= B ) -> E. m e. ( MaxIdeal ` R ) ( ( RSpan ` R ) ` { X } ) C_ m )
23 9 16 21 22 syl3anc 
 |-  ( ( ph /\ -. X e. U ) -> E. m e. ( MaxIdeal ` R ) ( ( RSpan ` R ) ` { X } ) C_ m )
24 5 adantr 
 |-  ( ( ph /\ -. X e. U ) -> ( MaxIdeal ` R ) = { M } )
25 23 24 rexeqtrdv 
 |-  ( ( ph /\ -. X e. U ) -> E. m e. { M } ( ( RSpan ` R ) ` { X } ) C_ m )
26 sseq2 
 |-  ( m = M -> ( ( ( RSpan ` R ) ` { X } ) C_ m <-> ( ( RSpan ` R ) ` { X } ) C_ M ) )
27 26 rexsng 
 |-  ( M e. ( MaxIdeal ` R ) -> ( E. m e. { M } ( ( RSpan ` R ) ` { X } ) C_ m <-> ( ( RSpan ` R ) ` { X } ) C_ M ) )
28 27 biimpa 
 |-  ( ( M e. ( MaxIdeal ` R ) /\ E. m e. { M } ( ( RSpan ` R ) ` { X } ) C_ m ) -> ( ( RSpan ` R ) ` { X } ) C_ M )
29 7 25 28 syl2anc 
 |-  ( ( ph /\ -. X e. U ) -> ( ( RSpan ` R ) ` { X } ) C_ M )
30 1 12 rspsnid 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. ( ( RSpan ` R ) ` { X } ) )
31 8 10 30 syl2anc 
 |-  ( ph -> X e. ( ( RSpan ` R ) ` { X } ) )
32 6 eldifbd 
 |-  ( ph -> -. X e. M )
33 nelss 
 |-  ( ( X e. ( ( RSpan ` R ) ` { X } ) /\ -. X e. M ) -> -. ( ( RSpan ` R ) ` { X } ) C_ M )
34 31 32 33 syl2anc 
 |-  ( ph -> -. ( ( RSpan ` R ) ` { X } ) C_ M )
35 34 adantr 
 |-  ( ( ph /\ -. X e. U ) -> -. ( ( RSpan ` R ) ` { X } ) C_ M )
36 29 35 condan 
 |-  ( ph -> X e. U )