Metamath Proof Explorer

Theorem mxidlirredi

Description: In an integral domain, the generator of a maximal ideal is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses mxidlirredi.b 
|- B = ( Base ` R )
mxidlirredi.k 
|- K = ( RSpan ` R )
mxidlirredi.0 
|- .0. = ( 0g ` R )
mxidlirredi.m 
|- M = ( K ` { X } )
mxidlirredi.r 
|- ( ph -> R e. IDomn )
mxidlirredi.x 
|- ( ph -> X e. B )
mxidlirredi.y 
|- ( ph -> X =/= .0. )
mxidlirredi.1 
|- ( ph -> M e. ( MaxIdeal ` R ) )
Assertion mxidlirredi 
|- ( ph -> X e. ( Irred ` R ) )

Proof

Step Hyp Ref Expression
1 mxidlirredi.b 
 |-  B = ( Base ` R )
2 mxidlirredi.k 
 |-  K = ( RSpan ` R )
3 mxidlirredi.0 
 |-  .0. = ( 0g ` R )
4 mxidlirredi.m 
 |-  M = ( K ` { X } )
5 mxidlirredi.r 
 |-  ( ph -> R e. IDomn )
6 mxidlirredi.x 
 |-  ( ph -> X e. B )
7 mxidlirredi.y 
 |-  ( ph -> X =/= .0. )
8 mxidlirredi.1 
 |-  ( ph -> M e. ( MaxIdeal ` R ) )
9 5 idomringd 
 |-  ( ph -> R e. Ring )
10 1 mxidlnr 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B )
11 9 8 10 syl2anc 
 |-  ( ph -> M =/= B )
12 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
13 12 2 4 1 6 5 unitpidl1 
 |-  ( ph -> ( M = B <-> X e. ( Unit ` R ) ) )
14 13 necon3abid 
 |-  ( ph -> ( M =/= B <-> -. X e. ( Unit ` R ) ) )
15 11 14 mpbid 
 |-  ( ph -> -. X e. ( Unit ` R ) )
16 6 15 eldifd 
 |-  ( ph -> X e. ( B \ ( Unit ` R ) ) )
17 9 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> R e. Ring )
18 8 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> M e. ( MaxIdeal ` R ) )
19 simplr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( B \ ( Unit ` R ) ) )
20 19 eldifad 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. B )
21 20 snssd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> { g } C_ B )
22 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
23 2 1 22 rspcl 
 |-  ( ( R e. Ring /\ { g } C_ B ) -> ( K ` { g } ) e. ( LIdeal ` R ) )
24 17 21 23 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( K ` { g } ) e. ( LIdeal ` R ) )
25 9 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> R e. Ring )
26 25 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> R e. Ring )
27 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> g e. ( B \ ( Unit ` R ) ) )
28 27 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> g e. B )
29 eqid 
 |-  ( .r ` R ) = ( .r ` R )
30 simplr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> q e. B )
31 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> f e. ( B \ ( Unit ` R ) ) )
32 31 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> f e. B )
33 1 29 26 30 32 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> ( q ( .r ` R ) f ) e. B )
34 oveq1 
 |-  ( y = ( q ( .r ` R ) f ) -> ( y ( .r ` R ) g ) = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) )
35 34 eqeq2d 
 |-  ( y = ( q ( .r ` R ) f ) -> ( x = ( y ( .r ` R ) g ) <-> x = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) ) )
36 35 adantl 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) /\ y = ( q ( .r ` R ) f ) ) -> ( x = ( y ( .r ` R ) g ) <-> x = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) ) )
37 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> ( f ( .r ` R ) g ) = X )
38 37 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> ( q ( .r ` R ) ( f ( .r ` R ) g ) ) = ( q ( .r ` R ) X ) )
39 1 29 26 30 32 28 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> ( ( q ( .r ` R ) f ) ( .r ` R ) g ) = ( q ( .r ` R ) ( f ( .r ` R ) g ) ) )
40 simpr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> x = ( q ( .r ` R ) X ) )
41 38 39 40 3eqtr4rd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> x = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) )
42 33 36 41 rspcedvd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> E. y e. B x = ( y ( .r ` R ) g ) )
43 1 29 2 elrspsn 
 |-  ( ( R e. Ring /\ g e. B ) -> ( x e. ( K ` { g } ) <-> E. y e. B x = ( y ( .r ` R ) g ) ) )
44 43 biimpar 
 |-  ( ( ( R e. Ring /\ g e. B ) /\ E. y e. B x = ( y ( .r ` R ) g ) ) -> x e. ( K ` { g } ) )
45 26 28 42 44 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) /\ q e. B ) /\ x = ( q ( .r ` R ) X ) ) -> x e. ( K ` { g } ) )
46 6 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> X e. B )
47 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> x e. M )
48 47 4 eleqtrdi 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> x e. ( K ` { X } ) )
49 1 29 2 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( x e. ( K ` { X } ) <-> E. q e. B x = ( q ( .r ` R ) X ) ) )
50 49 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ x e. ( K ` { X } ) ) -> E. q e. B x = ( q ( .r ` R ) X ) )
51 25 46 48 50 syl21anc 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> E. q e. B x = ( q ( .r ` R ) X ) )
52 45 51 r19.29a 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> x e. ( K ` { g } ) )
53 52 ex 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( x e. M -> x e. ( K ` { g } ) ) )
54 53 ssrdv 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> M C_ ( K ` { g } ) )
55 2 1 rspssid 
 |-  ( ( R e. Ring /\ { g } C_ B ) -> { g } C_ ( K ` { g } ) )
56 vex 
 |-  g e. _V
57 56 snss 
 |-  ( g e. ( K ` { g } ) <-> { g } C_ ( K ` { g } ) )
58 55 57 sylibr 
 |-  ( ( R e. Ring /\ { g } C_ B ) -> g e. ( K ` { g } ) )
59 17 21 58 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( K ` { g } ) )
60 df-idom 
 |-  IDomn = ( CRing i^i Domn )
61 5 60 eleqtrdi 
 |-  ( ph -> R e. ( CRing i^i Domn ) )
62 61 elin1d 
 |-  ( ph -> R e. CRing )
63 62 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> R e. CRing )
64 simplr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> r e. B )
65 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> f e. ( B \ ( Unit ` R ) ) )
66 65 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> f e. B )
67 17 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> R e. Ring )
68 67 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> R e. Ring )
69 1 29 68 64 66 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( r ( .r ` R ) f ) e. B )
70 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
71 1 70 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
72 9 71 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
73 72 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( 1r ` R ) e. B )
74 20 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> g e. B )
75 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> g = .0. )
76 75 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> ( f ( .r ` R ) g ) = ( f ( .r ` R ) .0. ) )
77 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> ( f ( .r ` R ) g ) = X )
78 67 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> R e. Ring )
79 66 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> f e. B )
80 1 29 3 ringrz 
 |-  ( ( R e. Ring /\ f e. B ) -> ( f ( .r ` R ) .0. ) = .0. )
81 78 79 80 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> ( f ( .r ` R ) .0. ) = .0. )
82 76 77 81 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> X = .0. )
83 7 neneqd 
 |-  ( ph -> -. X = .0. )
84 83 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) /\ g = .0. ) -> -. X = .0. )
85 82 84 pm2.65da 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> -. g = .0. )
86 85 neqned 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> g =/= .0. )
87 eldifsn 
 |-  ( g e. ( B \ { .0. } ) <-> ( g e. B /\ g =/= .0. ) )
88 74 86 87 sylanbrc 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> g e. ( B \ { .0. } ) )
89 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> R e. IDomn )
90 1 29 70 68 74 ringlidmd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( ( 1r ` R ) ( .r ` R ) g ) = g )
91 simpr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> g = ( r ( .r ` R ) X ) )
92 1 29 68 64 66 74 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( ( r ( .r ` R ) f ) ( .r ` R ) g ) = ( r ( .r ` R ) ( f ( .r ` R ) g ) ) )
93 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( f ( .r ` R ) g ) = X )
94 93 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( r ( .r ` R ) ( f ( .r ` R ) g ) ) = ( r ( .r ` R ) X ) )
95 92 94 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( r ( .r ` R ) X ) = ( ( r ( .r ` R ) f ) ( .r ` R ) g ) )
96 90 91 95 3eqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( ( r ( .r ` R ) f ) ( .r ` R ) g ) = ( ( 1r ` R ) ( .r ` R ) g ) )
97 1 3 29 69 73 88 89 96 idomrcan 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( r ( .r ` R ) f ) = ( 1r ` R ) )
98 12 70 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
99 9 98 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Unit ` R ) )
100 99 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( 1r ` R ) e. ( Unit ` R ) )
101 97 100 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> ( r ( .r ` R ) f ) e. ( Unit ` R ) )
102 12 29 1 unitmulclb 
 |-  ( ( R e. CRing /\ r e. B /\ f e. B ) -> ( ( r ( .r ` R ) f ) e. ( Unit ` R ) <-> ( r e. ( Unit ` R ) /\ f e. ( Unit ` R ) ) ) )
103 102 simplbda 
 |-  ( ( ( R e. CRing /\ r e. B /\ f e. B ) /\ ( r ( .r ` R ) f ) e. ( Unit ` R ) ) -> f e. ( Unit ` R ) )
104 63 64 66 101 103 syl31anc 
 |-  ( ( ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) /\ r e. B ) /\ g = ( r ( .r ` R ) X ) ) -> f e. ( Unit ` R ) )
105 6 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> X e. B )
106 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> g e. M )
107 106 4 eleqtrdi 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> g e. ( K ` { X } ) )
108 1 29 2 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( g e. ( K ` { X } ) <-> E. r e. B g = ( r ( .r ` R ) X ) ) )
109 108 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ g e. ( K ` { X } ) ) -> E. r e. B g = ( r ( .r ` R ) X ) )
110 67 105 107 109 syl21anc 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> E. r e. B g = ( r ( .r ` R ) X ) )
111 104 110 r19.29a 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> f e. ( Unit ` R ) )
112 simp-4r 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> f e. ( B \ ( Unit ` R ) ) )
113 112 eldifbd 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> -. f e. ( Unit ` R ) )
114 111 113 pm2.65da 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> -. g e. M )
115 59 114 eldifd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( ( K ` { g } ) \ M ) )
116 1 17 18 24 54 115 mxidlmaxv 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( K ` { g } ) = B )
117 eqid 
 |-  ( K ` { g } ) = ( K ` { g } )
118 5 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> R e. IDomn )
119 12 2 117 1 20 118 unitpidl1 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( ( K ` { g } ) = B <-> g e. ( Unit ` R ) ) )
120 116 119 mpbid 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( Unit ` R ) )
121 19 eldifbd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> -. g e. ( Unit ` R ) )
122 120 121 pm2.65da 
 |-  ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) -> -. ( f ( .r ` R ) g ) = X )
123 122 anasss 
 |-  ( ( ph /\ ( f e. ( B \ ( Unit ` R ) ) /\ g e. ( B \ ( Unit ` R ) ) ) ) -> -. ( f ( .r ` R ) g ) = X )
124 123 neqned 
 |-  ( ( ph /\ ( f e. ( B \ ( Unit ` R ) ) /\ g e. ( B \ ( Unit ` R ) ) ) ) -> ( f ( .r ` R ) g ) =/= X )
125 124 ralrimivva 
 |-  ( ph -> A. f e. ( B \ ( Unit ` R ) ) A. g e. ( B \ ( Unit ` R ) ) ( f ( .r ` R ) g ) =/= X )
126 eqid 
 |-  ( Irred ` R ) = ( Irred ` R )
127 eqid 
 |-  ( B \ ( Unit ` R ) ) = ( B \ ( Unit ` R ) )
128 1 12 126 127 29 isirred 
 |-  ( X e. ( Irred ` R ) <-> ( X e. ( B \ ( Unit ` R ) ) /\ A. f e. ( B \ ( Unit ` R ) ) A. g e. ( B \ ( Unit ` R ) ) ( f ( .r ` R ) g ) =/= X ) )
129 16 125 128 sylanbrc 
 |-  ( ph -> X e. ( Irred ` R ) )