This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- B = ( Base ` R )
mxidlirred.k 
|- K = ( RSpan ` R )
mxidlirred.0 
|- .0. = ( 0g ` R )
mxidlirred.m 
|- M = ( K ` { X } )
mxidlirred.r 
|- ( ph -> R e. PID )
mxidlirred.x 
|- ( ph -> X e. B )
mxidlirred.y 
|- ( ph -> X =/= .0. )
mxidlirred.1 
|- ( ph -> M e. ( LIdeal ` R ) )
Assertion mxidlirred 
|- ( ph -> ( M e. ( MaxIdeal ` R ) <-> X e. ( Irred ` R ) ) )

Proof

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