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 48 idomcringd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑅 ∈ CRing )
50 21 2 47 1 19 49 unitpidl1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( 𝐾 ‘ { 𝑥 } ) = 𝐵 ↔ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) )
51 46 50 mtbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ 𝑥 ∈ ( Unit ‘ 𝑅 ) )
52 33 51 olcnd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑡 ∈ ( Unit ‘ 𝑅 ) )
53 28 eqcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑋 )
54 1 2 17 19 20 21 22 26 52 53 dvdsruassoi ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑥 ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ) )
55 1 2 17 19 20 26 rspsnasso ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ) ↔ ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑥 } ) ) )
56 54 55 mpbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑥 } ) )
57 56 35 eqtr4d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝐾 ‘ { 𝑋 } ) = 𝑘 )
58 4 57 eqtr2id ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑘 = 𝑀 )
59 41 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ¬ 𝑘 = 𝑀 )
60 59 ad4antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ 𝑘 = 𝑀 )
61 58 60 pm2.21dd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
62 38 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑀 ⊆ 𝑘 )
63 62 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑀 ⊆ 𝑘 )
64 6 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
65 2 1 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
66 23 64 65 syl2anc ⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
67 66 4 sseqtrrdi ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑀 )
68 snssg ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝑀 ↔ { 𝑋 } ⊆ 𝑀 ) )
69 68 biimpar ⊢ ( ( 𝑋 ∈ 𝐵 ∧ { 𝑋 } ⊆ 𝑀 ) → 𝑋 ∈ 𝑀 )
70 6 67 69 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
71 70 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ 𝑀 )
72 63 71 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ 𝑘 )
73 72 34 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) )
74 1 22 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) ↔ ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) ) )
75 74 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑋 ∈ ( 𝐾 ‘ { 𝑥 } ) ) → ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) )
76 25 18 73 75 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → ∃ 𝑡 ∈ 𝐵 𝑋 = ( 𝑡 ( .r ‘ 𝑅 ) 𝑥 ) )
77 61 76 r19.29a ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
78 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
79 10 elin2d ⊢ ( 𝜑 → 𝑅 ∈ LPIR )
80 eqid ⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
81 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
82 80 81 islpir ⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) ) )
83 82 simprbi ⊢ ( 𝑅 ∈ LPIR → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
84 79 83 syl ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
85 84 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
86 78 85 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) )
87 80 2 1 islpidl ⊢ ( 𝑅 ∈ Ring → ( 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) ) )
88 87 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LPIdeal ‘ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
89 24 86 88 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝑘 = ( 𝐾 ‘ { 𝑥 } ) )
90 77 89 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
91 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
92 31 21 irrednu ⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
94 11 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
95 21 2 4 1 6 94 unitpidl1 ⊢ ( 𝜑 → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
97 96 necon3abid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → ( 𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
98 93 97 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
100 91 99 jca ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) )
101 1 ismxidl ⊢ ( 𝑅 ∈ Ring → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
102 23 101 syl ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
103 df-3an ⊢ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ↔ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
104 102 103 bitrdi ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
105 104 notbid ⊢ ( 𝜑 → ( ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) ) )
106 105 biimpa ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
107 106 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ≠ 𝐵 ) ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ) )
108 100 107 mpnanrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
109 rexnal ⊢ ( ∃ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) ↔ ¬ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
110 108 109 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ∃ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ¬ ( 𝑀 ⊆ 𝑘 → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝐵 ) ) )
111 90 110 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) ∧ ¬ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
112 111 pm2.18da ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
113 16 112 impbida ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑋 ∈ ( Irred ‘ 𝑅 ) ) )