Metamath Proof Explorer

Theorem mxidlirred

Description: In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses mxidlirred.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mxidlirred.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
mxidlirred.0 ⊢ 0 = ( 0g ‘ 𝑅 )
mxidlirred.m ⊢ 𝑀 = ( 𝐾 ‘ { 𝑋 } )
mxidlirred.r ⊢ ( 𝜑 → 𝑅 ∈ PID )
mxidlirred.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mxidlirred.y ⊢ ( 𝜑 → 𝑋 ≠ 0 )
mxidlirred.1 ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion mxidlirred ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 mxidlirred.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mxidlirred.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 mxidlirred.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 mxidlirred.m ⊢ 𝑀 = ( 𝐾 ‘ { 𝑋 } )
5 mxidlirred.r ⊢ ( 𝜑 → 𝑅 ∈ PID )
6 mxidlirred.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mxidlirred.y ⊢ ( 𝜑 → 𝑋 ≠ 0 )
8 mxidlirred.1 ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
9 df-pid ⊢ PID = ( IDomn ∩ LPIR )
10 5 9 eleqtrdi ⊢ ( 𝜑 → 𝑅 ∈ ( IDomn ∩ LPIR ) )
11 10 elin1d ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ IDomn )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
14 7 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑋 ≠ 0 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
16 1 2 3 4 12 13 14 15 mxidlirredi ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑋 ∈ ( Irred ‘ 𝑅 ) )
17 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
18 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝐵 )
19 18 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑥 ∈ 𝐵 )
20 6 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑋 ∈ 𝐵 )
21 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
22 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23 11 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
24 23 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑅 ∈ Ring )
25 24 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑅 ∈ Ring )
26 25 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑅 ∈ Ring )
27 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑡 ∈ 𝐵 )
28 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) )
29 simp-8r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑋 ∈ ( Irred ‘ 𝑅 ) )
30 28 29 eqeltrrd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Irred ‘ 𝑅 ) )
31 eqid ⊢ ( Irred ‘ 𝑅 ) = ( Irred ‘ 𝑅 )
32 31 1 21 22 irredmul ⊢ ( ( 𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Irred ‘ 𝑅 ) ) → ( 𝑡 ∈ ( Unit ‘ 𝑅 ) ∨ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) )
33 27 19 30 32 syl3anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑡 ∈ ( Unit ‘ 𝑅 ) ∨ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) )
34 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
35 34 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
36 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
37 annim ⊢ ( ( 𝑀 ⊆ 𝑘 ∧ ¬ ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ↔ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
38 36 37 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ( 𝑀 ⊆ 𝑘 ∧ ¬ ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
39 38 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ¬ ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) )
40 ioran ⊢ ( ¬ ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ↔ ( ¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵 ) )
41 39 40 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ( ¬ 𝑘 = 𝑀 ∧ ¬ 𝑘 = 𝐵 ) )
42 41 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ¬ 𝑘 = 𝐵 )
43 42 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑘 ≠ 𝐵 )
44 43 ad4antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑘 ≠ 𝐵 )
45 35 44 eqnetrrd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝐾 ‘ { 𝑥 } ) ≠ 𝐵 )
46 45 neneqd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ ( 𝐾 ‘ { 𝑥 } ) = 𝐵 )
47 eqid ⊢ ( 𝐾 ‘ { 𝑥 } ) = ( 𝐾 ‘ { 𝑥 } )
48 11 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑅 ∈ IDomn )
49 21 2 47 1 19 48 unitpidl1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( 𝐾 ‘ { 𝑥 } ) = 𝐵 ↔ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) )
50 46 49 mtbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ 𝑥 ∈ ( Unit ‘ 𝑅 ) )
51 33 50 olcnd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑡 ∈ ( Unit ‘ 𝑅 ) )
52 28 eqcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑋 )
53 1 2 17 19 20 21 22 26 51 52 dvdsruassoi ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑥 ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ) )
54 1 2 17 19 20 26 rspsnasso ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ) ↔ ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑥 } ) ) )
55 53 54 mpbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑥 } ) )
56 55 35 eqtr4d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝐾 ‘ { 𝑋 } ) = 𝑘 )
57 4 56 eqtr2id ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑘 = 𝑀 )
58 41 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ¬ 𝑘 = 𝑀 )
59 58 ad4antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ 𝑘 = 𝑀 )
60 57 59 pm2.21dd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
61 38 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑀 ⊆ 𝑘 )
62 61 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑀 ⊆ 𝑘 )
63 6 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
64 2 1 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
65 23 63 64 syl2anc ⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
66 65 4 sseqtrrdi ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑀 )
67 snssg ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝑀 ↔ { 𝑋 } ⊆ 𝑀 ) )
68 67 biimpar ⊢ ( ( 𝑋 ∈ 𝐵 ∧ { 𝑋 } ⊆ 𝑀 ) → 𝑋 ∈ 𝑀 )
69 6 66 68 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
70 69 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ 𝑀 )
71 62 70 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ 𝑘 )
72 71 34 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) )
73 1 22 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) ↔ ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) )
74 73 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) ) → ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) )
75 25 18 72 74 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) )
76 60 75 r19.29a ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
77 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
78 10 elin2d ⊢ ( 𝜑 → 𝑅 ∈ LPIR )
79 eqid ⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
80 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
81 79 80 islpir ⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) ) )
82 81 simprbi ⊢ ( 𝑅 ∈ LPIR → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
83 78 82 syl ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
84 83 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
85 77 84 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) )
86 79 2 1 islpidl ⊢ ( 𝑅 ∈ Ring → ( 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) )
87 86 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
88 24 85 87 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
89 76 88 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
90 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
91 31 21 irrednu ⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
93 21 2 4 1 6 11 unitpidl1 ⊢ ( 𝜑 → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
95 94 necon3abid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ( 𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
96 92 95 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
98 90 97 jca ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) )
99 1 ismxidl ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
100 23 99 syl ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
101 df-3an ⊢ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ↔ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
102 100 101 bitrdi ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
103 102 notbid ⊢ ( 𝜑 → ( ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
104 103 biimpa ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
105 104 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
106 98 105 mpnanrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
107 rexnal ⊢ ( ∃ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ↔ ¬ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
108 106 107 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ∃ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
109 89 108 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
110 109 pm2.18da ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
111 16 110 impbida ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) )