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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dflringlem.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dflringlem.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
dflringlem.m ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
dflringlem.1 ⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑅 ) = { 𝑀 } )
dflringlem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑀 ) )
Assertion dflringlem ( 𝜑 → 𝑋 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 dflringlem.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dflringlem.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dflringlem.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 dflringlem.m ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
5 dflringlem.1 ⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑅 ) = { 𝑀 } )
6 dflringlem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑀 ) )
7 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
8 3 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ Ring )
10 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 10 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
12 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
13 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
14 12 1 13 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
15 8 11 14 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
17 eqid ⊢ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } )
18 2 12 17 1 10 3 unitpidl1 ⊢ ( 𝜑 → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) = 𝐵 ↔ 𝑋 ∈ 𝑈 ) )
19 18 notbid ⊢ ( 𝜑 → ( ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) = 𝐵 ↔ ¬ 𝑋 ∈ 𝑈 ) )
20 19 biimpar ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) = 𝐵 )
21 20 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ≠ 𝐵 )
22 1 ssmxidl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 )
23 9 16 21 22 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 )
24 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( MaxIdeal ‘ 𝑅 ) = { 𝑀 } )
25 23 24 rexeqtrdv ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ∃ 𝑚 ∈ { 𝑀 } ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 )
26 sseq2 ⊢ ( 𝑚 = 𝑀 → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 ) )
27 26 rexsng ⊢ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) → ( ∃ 𝑚 ∈ { 𝑀 } ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 ) )
28 27 biimpa ⊢ ( ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ { 𝑀 } ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑚 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 )
29 7 25 28 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 )
30 1 12 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
31 8 10 30 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
32 6 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑀 )
33 nelss ⊢ ( ( 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∧ ¬ 𝑋 ∈ 𝑀 ) → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 )
34 31 32 33 syl2anc ⊢ ( 𝜑 → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 )
35 34 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑈 ) → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑀 )
36 29 35 condan ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )