Metamath Proof Explorer

Theorem edompidlem

Description: Lemma for edompid : In a Euclidean domain, all (non-zero) ideals are generated by a single element. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses edompidlem.b 
|- B = ( Base ` D )
edompidlem.o 
|- .0. = ( 0g ` D )
edompidlem.k 
|- K = ( RSpan ` D )
edompidlem.e 
|- E = ( EuclF ` D )
edompidlem.m 
|- M = inf ( ( E " ( I \ { .0. } ) ) , NN0 , < )
edompidlem.d 
|- ( ph -> D e. EDomn )
edompidlem.i 
|- ( ph -> I e. ( LIdeal ` D ) )
edompidlem.1 
|- ( ph -> I =/= { .0. } )
Assertion edompidlem 
|- ( ph -> E. g e. B I = ( K ` { g } ) )

Proof

Step Hyp Ref Expression
1 edompidlem.b 
 |-  B = ( Base ` D )
2 edompidlem.o 
 |-  .0. = ( 0g ` D )
3 edompidlem.k 
 |-  K = ( RSpan ` D )
4 edompidlem.e 
 |-  E = ( EuclF ` D )
5 edompidlem.m 
 |-  M = inf ( ( E " ( I \ { .0. } ) ) , NN0 , < )
6 edompidlem.d 
 |-  ( ph -> D e. EDomn )
7 edompidlem.i 
 |-  ( ph -> I e. ( LIdeal ` D ) )
8 edompidlem.1 
 |-  ( ph -> I =/= { .0. } )
9 eqid 
 |-  ( LIdeal ` D ) = ( LIdeal ` D )
10 1 9 lidlss 
 |-  ( I e. ( LIdeal ` D ) -> I C_ B )
11 7 10 syl 
 |-  ( ph -> I C_ B )
12 11 ssdifssd 
 |-  ( ph -> ( I \ { .0. } ) C_ B )
13 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) )
14 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) /\ r = .0. ) -> r = .0. )
15 ltrel 
 |-  Rel <
16 15 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> Rel < )
17 ltwenn0 
 |-  < We NN0
18 17 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> < We NN0 )
19 4 fvexi 
 |-  E e. _V
20 19 a1i 
 |-  ( ph -> E e. _V )
21 20 imaexd 
 |-  ( ph -> ( E " ( I \ { .0. } ) ) e. _V )
22 21 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( E " ( I \ { .0. } ) ) e. _V )
23 11 ssdifd 
 |-  ( ph -> ( I \ { .0. } ) C_ ( B \ { .0. } ) )
24 imass2 
 |-  ( ( I \ { .0. } ) C_ ( B \ { .0. } ) -> ( E " ( I \ { .0. } ) ) C_ ( E " ( B \ { .0. } ) ) )
25 23 24 syl 
 |-  ( ph -> ( E " ( I \ { .0. } ) ) C_ ( E " ( B \ { .0. } ) ) )
26 resima 
 |-  ( ( E |` ( B \ { .0. } ) ) " ( B \ { .0. } ) ) = ( E " ( B \ { .0. } ) )
27 eqid 
 |-  ( +g ` D ) = ( +g ` D )
28 eqid 
 |-  ( .r ` D ) = ( .r ` D )
29 4 reseq1i 
 |-  ( E |` ( B \ { .0. } ) ) = ( ( EuclF ` D ) |` ( B \ { .0. } ) )
30 1 2 27 28 29 isedom 
 |-  ( D e. EDomn <-> ( D e. IDomn /\ ( ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` D ) q ) ( +g ` D ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) ) )
31 6 30 sylib 
 |-  ( ph -> ( D e. IDomn /\ ( ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` D ) q ) ( +g ` D ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) ) )
32 31 simprld 
 |-  ( ph -> ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 )
33 32 fimassd 
 |-  ( ph -> ( ( E |` ( B \ { .0. } ) ) " ( B \ { .0. } ) ) C_ NN0 )
34 26 33 eqsstrrid 
 |-  ( ph -> ( E " ( B \ { .0. } ) ) C_ NN0 )
35 25 34 sstrd 
 |-  ( ph -> ( E " ( I \ { .0. } ) ) C_ NN0 )
36 35 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( E " ( I \ { .0. } ) ) C_ NN0 )
37 31 simpld 
 |-  ( ph -> D e. IDomn )
38 37 idomringd 
 |-  ( ph -> D e. Ring )
39 9 2 lidl0cl 
 |-  ( ( D e. Ring /\ I e. ( LIdeal ` D ) ) -> .0. e. I )
40 38 7 39 syl2anc 
 |-  ( ph -> .0. e. I )
41 40 snssd 
 |-  ( ph -> { .0. } C_ I )
42 8 necomd 
 |-  ( ph -> { .0. } =/= I )
43 pssdifn0 
 |-  ( ( { .0. } C_ I /\ { .0. } =/= I ) -> ( I \ { .0. } ) =/= (/) )
44 41 42 43 syl2anc 
 |-  ( ph -> ( I \ { .0. } ) =/= (/) )
45 32 ffnd 
 |-  ( ph -> ( E |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) )
46 45 adantr 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> ( E |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) )
47 23 sselda 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> x e. ( B \ { .0. } ) )
48 simpr 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> x e. ( I \ { .0. } ) )
49 46 47 48 fnfvimad 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> ( ( E |` ( B \ { .0. } ) ) ` x ) e. ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) )
50 resima2 
 |-  ( ( I \ { .0. } ) C_ ( B \ { .0. } ) -> ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) = ( E " ( I \ { .0. } ) ) )
51 23 50 syl 
 |-  ( ph -> ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) = ( E " ( I \ { .0. } ) ) )
52 51 adantr 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) = ( E " ( I \ { .0. } ) ) )
53 49 52 eleqtrd 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> ( ( E |` ( B \ { .0. } ) ) ` x ) e. ( E " ( I \ { .0. } ) ) )
54 53 ne0d 
 |-  ( ( ph /\ x e. ( I \ { .0. } ) ) -> ( E " ( I \ { .0. } ) ) =/= (/) )
55 44 54 n0limd 
 |-  ( ph -> ( E " ( I \ { .0. } ) ) =/= (/) )
56 55 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( E " ( I \ { .0. } ) ) =/= (/) )
57 45 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( E |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) )
58 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r e. B )
59 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r =/= .0. )
60 58 59 eldifsnd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r e. ( B \ { .0. } ) )
61 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) )
62 61 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( a ( -g ` D ) ( g ( .r ` D ) q ) ) = ( ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ( -g ` D ) ( g ( .r ` D ) q ) ) )
63 38 ringabld 
 |-  ( ph -> D e. Abel )
64 63 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> D e. Abel )
65 38 ad2antrr 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> D e. Ring )
66 65 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> D e. Ring )
67 23 sselda 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> g e. ( B \ { .0. } ) )
68 67 eldifad 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> g e. B )
69 68 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> g e. B )
70 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> q e. B )
71 1 28 66 69 70 ringcld 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( g ( .r ` D ) q ) e. B )
72 eqid 
 |-  ( -g ` D ) = ( -g ` D )
73 1 27 72 ablpncan2 
 |-  ( ( D e. Abel /\ ( g ( .r ` D ) q ) e. B /\ r e. B ) -> ( ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ( -g ` D ) ( g ( .r ` D ) q ) ) = r )
74 64 71 58 73 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ( -g ` D ) ( g ( .r ` D ) q ) ) = r )
75 62 74 eqtr2d 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r = ( a ( -g ` D ) ( g ( .r ` D ) q ) ) )
76 7 ad2antrr 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> I e. ( LIdeal ` D ) )
77 76 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> I e. ( LIdeal ` D ) )
78 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> a e. I )
79 37 idomcringd 
 |-  ( ph -> D e. CRing )
80 79 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) -> D e. CRing )
81 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) -> q e. B )
82 68 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) -> g e. B )
83 1 28 80 81 82 crngcomd 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) -> ( q ( .r ` D ) g ) = ( g ( .r ` D ) q ) )
84 83 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( q ( .r ` D ) g ) = ( g ( .r ` D ) q ) )
85 simplr 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> g e. ( I \ { .0. } ) )
86 85 eldifad 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> g e. I )
87 86 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> g e. I )
88 9 1 28 66 77 70 87 lidlmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( q ( .r ` D ) g ) e. I )
89 84 88 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( g ( .r ` D ) q ) e. I )
90 9 72 lidlsubcl 
 |-  ( ( ( D e. Ring /\ I e. ( LIdeal ` D ) ) /\ ( a e. I /\ ( g ( .r ` D ) q ) e. I ) ) -> ( a ( -g ` D ) ( g ( .r ` D ) q ) ) e. I )
91 66 77 78 89 90 syl22anc 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( a ( -g ` D ) ( g ( .r ` D ) q ) ) e. I )
92 75 91 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r e. I )
93 92 59 eldifsnd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> r e. ( I \ { .0. } ) )
94 57 60 93 fnfvimad 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` r ) e. ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) )
95 60 fvresd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` r ) = ( E ` r ) )
96 51 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) = ( E " ( I \ { .0. } ) ) )
97 94 95 96 3eltr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( E ` r ) e. ( E " ( I \ { .0. } ) ) )
98 16 18 22 36 56 97 weinflb 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> -. ( E ` r ) < inf ( ( E " ( I \ { .0. } ) ) , NN0 , < ) )
99 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` g ) = M )
100 67 ad2antrr 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> g e. ( B \ { .0. } ) )
101 100 fvresd 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> ( ( E |` ( B \ { .0. } ) ) ` g ) = ( E ` g ) )
102 101 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` g ) = ( E ` g ) )
103 5 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> M = inf ( ( E " ( I \ { .0. } ) ) , NN0 , < ) )
104 99 102 103 3eqtr3rd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> inf ( ( E " ( I \ { .0. } ) ) , NN0 , < ) = ( E ` g ) )
105 98 104 brneqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ r =/= .0. ) -> -. ( E ` r ) < ( E ` g ) )
106 105 ex 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) -> ( r =/= .0. -> -. ( E ` r ) < ( E ` g ) ) )
107 106 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( r =/= .0. -> -. ( E ` r ) < ( E ` g ) ) )
108 107 necon4ad 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( ( E ` r ) < ( E ` g ) -> r = .0. ) )
109 108 imp 
 |-  ( ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) /\ ( E ` r ) < ( E ` g ) ) -> r = .0. )
110 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( r = .0. \/ ( E ` r ) < ( E ` g ) ) )
111 14 109 110 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> r = .0. )
112 111 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( ( g ( .r ` D ) q ) ( +g ` D ) r ) = ( ( g ( .r ` D ) q ) ( +g ` D ) .0. ) )
113 38 ringgrpd 
 |-  ( ph -> D e. Grp )
114 113 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> D e. Grp )
115 65 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> D e. Ring )
116 68 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> g e. B )
117 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> q e. B )
118 1 28 115 116 117 ringcld 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( g ( .r ` D ) q ) e. B )
119 1 27 2 114 118 grpridd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( ( g ( .r ` D ) q ) ( +g ` D ) .0. ) = ( g ( .r ` D ) q ) )
120 13 112 119 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> a = ( g ( .r ` D ) q ) )
121 83 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( q ( .r ` D ) g ) = ( g ( .r ` D ) q ) )
122 120 121 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> a = ( q ( .r ` D ) g ) )
123 38 adantr 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> D e. Ring )
124 68 snssd 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> { g } C_ B )
125 3 1 9 rspcl 
 |-  ( ( D e. Ring /\ { g } C_ B ) -> ( K ` { g } ) e. ( LIdeal ` D ) )
126 123 124 125 syl2anc 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> ( K ` { g } ) e. ( LIdeal ` D ) )
127 126 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( K ` { g } ) e. ( LIdeal ` D ) )
128 1 3 rspsnid 
 |-  ( ( D e. Ring /\ g e. B ) -> g e. ( K ` { g } ) )
129 123 68 128 syl2anc 
 |-  ( ( ph /\ g e. ( I \ { .0. } ) ) -> g e. ( K ` { g } ) )
130 129 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> g e. ( K ` { g } ) )
131 9 1 28 115 127 117 130 lidlmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> ( q ( .r ` D ) g ) e. ( K ` { g } ) )
132 122 131 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) -> a e. ( K ` { g } ) )
133 132 anasss 
 |-  ( ( ( ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) /\ q e. B ) /\ r e. B ) /\ ( a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) ) -> a e. ( K ` { g } ) )
134 6 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> D e. EDomn )
135 76 10 syl 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> I C_ B )
136 135 sselda 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> a e. B )
137 1 2 27 28 4 134 136 100 edomediv 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> E. q e. B E. r e. B ( a = ( ( g ( .r ` D ) q ) ( +g ` D ) r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` g ) ) ) )
138 133 137 r19.29vva 
 |-  ( ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) /\ a e. I ) -> a e. ( K ` { g } ) )
139 138 ex 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> ( a e. I -> a e. ( K ` { g } ) ) )
140 139 ssrdv 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> I C_ ( K ` { g } ) )
141 86 snssd 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> { g } C_ I )
142 3 9 rspssp 
 |-  ( ( D e. Ring /\ I e. ( LIdeal ` D ) /\ { g } C_ I ) -> ( K ` { g } ) C_ I )
143 65 76 141 142 syl3anc 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> ( K ` { g } ) C_ I )
144 140 143 eqssd 
 |-  ( ( ( ph /\ g e. ( I \ { .0. } ) ) /\ ( ( E |` ( B \ { .0. } ) ) ` g ) = M ) -> I = ( K ` { g } ) )
145 nfcv 
 |-  F/_ g ( E |` ( B \ { .0. } ) )
146 17 a1i 
 |-  ( ph -> < We NN0 )
147 146 21 35 55 weinfcl 
 |-  ( ph -> inf ( ( E " ( I \ { .0. } ) ) , NN0 , < ) e. ( E " ( I \ { .0. } ) ) )
148 5 147 eqeltrid 
 |-  ( ph -> M e. ( E " ( I \ { .0. } ) ) )
149 148 51 eleqtrrd 
 |-  ( ph -> M e. ( ( E |` ( B \ { .0. } ) ) " ( I \ { .0. } ) ) )
150 145 45 149 fvelimad 
 |-  ( ph -> E. g e. ( ( B \ { .0. } ) i^i ( I \ { .0. } ) ) ( ( E |` ( B \ { .0. } ) ) ` g ) = M )
151 sseqin2 
 |-  ( ( I \ { .0. } ) C_ ( B \ { .0. } ) <-> ( ( B \ { .0. } ) i^i ( I \ { .0. } ) ) = ( I \ { .0. } ) )
152 23 151 sylib 
 |-  ( ph -> ( ( B \ { .0. } ) i^i ( I \ { .0. } ) ) = ( I \ { .0. } ) )
153 150 152 rexeqtrdv 
 |-  ( ph -> E. g e. ( I \ { .0. } ) ( ( E |` ( B \ { .0. } ) ) ` g ) = M )
154 144 153 reximddv3 
 |-  ( ph -> E. g e. ( I \ { .0. } ) I = ( K ` { g } ) )
155 ssrexv 
 |-  ( ( I \ { .0. } ) C_ B -> ( E. g e. ( I \ { .0. } ) I = ( K ` { g } ) -> E. g e. B I = ( K ` { g } ) ) )
156 12 154 155 sylc 
 |-  ( ph -> E. g e. B I = ( K ` { g } ) )