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 5 idomcringd 
 |-  ( ph -> R e. CRing )
14 12 2 4 1 6 13 unitpidl1 
 |-  ( ph -> ( M = B <-> X e. ( Unit ` R ) ) )
15 14 necon3abid 
 |-  ( ph -> ( M =/= B <-> -. X e. ( Unit ` R ) ) )
16 11 15 mpbid 
 |-  ( ph -> -. X e. ( Unit ` R ) )
17 6 16 eldifd 
 |-  ( ph -> X e. ( B \ ( Unit ` R ) ) )
18 9 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> R e. Ring )
19 8 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> M e. ( MaxIdeal ` R ) )
20 simplr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( B \ ( Unit ` R ) ) )
21 20 eldifad 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. B )
22 21 snssd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> { g } C_ B )
23 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
24 2 1 23 rspcl 
 |-  ( ( R e. Ring /\ { g } C_ B ) -> ( K ` { g } ) e. ( LIdeal ` R ) )
25 18 22 24 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( K ` { g } ) e. ( LIdeal ` R ) )
26 9 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ x e. M ) -> R e. Ring )
27 26 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 )
28 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 ) ) )
29 28 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 )
30 oveq1 
 |-  ( y = ( q ( .r ` R ) f ) -> ( y ( .r ` R ) g ) = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) )
31 30 eqeq2d 
 |-  ( y = ( q ( .r ` R ) f ) -> ( x = ( y ( .r ` R ) g ) <-> x = ( ( q ( .r ` R ) f ) ( .r ` R ) g ) ) )
32 eqid 
 |-  ( .r ` R ) = ( .r ` R )
33 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 )
34 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 ) ) )
35 34 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 )
36 1 32 27 33 35 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 )
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 32 27 33 35 29 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 31 36 41 rspcedvdw 
 |-  ( ( ( ( ( ( ( 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 32 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 27 29 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 32 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 26 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 18 22 58 syl2anc 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( K ` { g } ) )
60 13 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 )
61 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 )
62 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 ) ) )
63 62 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 )
64 18 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> R e. Ring )
65 64 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 )
66 1 32 65 61 63 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 )
67 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
68 1 67 9 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. B )
69 68 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 )
70 21 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 )
71 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. )
72 71 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. ) )
73 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 )
74 64 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 )
75 63 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 )
76 1 32 3 74 75 ringrzd 
 |-  ( ( ( ( ( ( ( ( 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. )
77 72 73 76 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. )
78 7 neneqd 
 |-  ( ph -> -. X = .0. )
79 78 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. )
80 77 79 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. )
81 80 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. )
82 70 81 eldifsnd 
 |-  ( ( ( ( ( ( ( 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. } ) )
83 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 )
84 1 32 67 65 70 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 )
85 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 ) )
86 1 32 65 61 63 70 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 ) ) )
87 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 )
88 87 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 ) )
89 86 88 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 ) )
90 84 85 89 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 ) )
91 1 3 32 66 69 82 83 90 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 ) )
92 12 67 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
93 9 92 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Unit ` R ) )
94 93 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 ) )
95 91 94 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 ) )
96 12 32 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 ) ) ) )
97 96 simplbda 
 |-  ( ( ( R e. CRing /\ r e. B /\ f e. B ) /\ ( r ( .r ` R ) f ) e. ( Unit ` R ) ) -> f e. ( Unit ` R ) )
98 60 61 63 95 97 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 ) )
99 6 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> X e. B )
100 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> g e. M )
101 100 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 } ) )
102 1 32 2 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( g e. ( K ` { X } ) <-> E. r e. B g = ( r ( .r ` R ) X ) ) )
103 102 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ g e. ( K ` { X } ) ) -> E. r e. B g = ( r ( .r ` R ) X ) )
104 64 99 101 103 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 ) )
105 98 104 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 ) )
106 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 ) ) )
107 106 eldifbd 
 |-  ( ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) /\ g e. M ) -> -. f e. ( Unit ` R ) )
108 105 107 pm2.65da 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> -. g e. M )
109 59 108 eldifd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( ( K ` { g } ) \ M ) )
110 1 18 19 25 54 109 mxidlmaxv 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( K ` { g } ) = B )
111 eqid 
 |-  ( K ` { g } ) = ( K ` { g } )
112 13 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> R e. CRing )
113 12 2 111 1 21 112 unitpidl1 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> ( ( K ` { g } ) = B <-> g e. ( Unit ` R ) ) )
114 110 113 mpbid 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> g e. ( Unit ` R ) )
115 20 eldifbd 
 |-  ( ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) /\ ( f ( .r ` R ) g ) = X ) -> -. g e. ( Unit ` R ) )
116 114 115 pm2.65da 
 |-  ( ( ( ph /\ f e. ( B \ ( Unit ` R ) ) ) /\ g e. ( B \ ( Unit ` R ) ) ) -> -. ( f ( .r ` R ) g ) = X )
117 116 anasss 
 |-  ( ( ph /\ ( f e. ( B \ ( Unit ` R ) ) /\ g e. ( B \ ( Unit ` R ) ) ) ) -> -. ( f ( .r ` R ) g ) = X )
118 117 neqned 
 |-  ( ( ph /\ ( f e. ( B \ ( Unit ` R ) ) /\ g e. ( B \ ( Unit ` R ) ) ) ) -> ( f ( .r ` R ) g ) =/= X )
119 118 ralrimivva 
 |-  ( ph -> A. f e. ( B \ ( Unit ` R ) ) A. g e. ( B \ ( Unit ` R ) ) ( f ( .r ` R ) g ) =/= X )
120 eqid 
 |-  ( Irred ` R ) = ( Irred ` R )
121 eqid 
 |-  ( B \ ( Unit ` R ) ) = ( B \ ( Unit ` R ) )
122 1 12 120 121 32 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 ) )
123 17 119 122 sylanbrc 
 |-  ( ph -> X e. ( Irred ` R ) )