Metamath Proof Explorer

Theorem ig1pdvds

Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1pval.p 
|- P = ( Poly1 ` R )
ig1pval.g 
|- G = ( idlGen1p ` R )
ig1pcl.u 
|- U = ( LIdeal ` P )
ig1pdvds.d 
|- .|| = ( ||r ` P )
Assertion ig1pdvds 
|- ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) .|| X )

Proof

Step Hyp Ref Expression
1 ig1pval.p 
 |-  P = ( Poly1 ` R )
2 ig1pval.g 
 |-  G = ( idlGen1p ` R )
3 ig1pcl.u 
 |-  U = ( LIdeal ` P )
4 ig1pdvds.d 
 |-  .|| = ( ||r ` P )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
7 5 6 syl 
 |-  ( R e. DivRing -> P e. Ring )
8 7 3ad2ant1 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> P e. Ring )
9 eqid 
 |-  ( Base ` P ) = ( Base ` P )
10 9 3 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
11 10 3ad2ant2 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> I C_ ( Base ` P ) )
12 1 2 3 ig1pcl 
 |-  ( ( R e. DivRing /\ I e. U ) -> ( G ` I ) e. I )
13 12 3adant3 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) e. I )
14 11 13 sseldd 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) e. ( Base ` P ) )
15 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
16 9 4 15 dvdsr01 
 |-  ( ( P e. Ring /\ ( G ` I ) e. ( Base ` P ) ) -> ( G ` I ) .|| ( 0g ` P ) )
17 8 14 16 syl2anc 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) .|| ( 0g ` P ) )
18 17 adantr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I = { ( 0g ` P ) } ) -> ( G ` I ) .|| ( 0g ` P ) )
19 eleq2 
 |-  ( I = { ( 0g ` P ) } -> ( X e. I <-> X e. { ( 0g ` P ) } ) )
20 19 biimpac 
 |-  ( ( X e. I /\ I = { ( 0g ` P ) } ) -> X e. { ( 0g ` P ) } )
21 20 3ad2antl3 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I = { ( 0g ` P ) } ) -> X e. { ( 0g ` P ) } )
22 elsni 
 |-  ( X e. { ( 0g ` P ) } -> X = ( 0g ` P ) )
23 21 22 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I = { ( 0g ` P ) } ) -> X = ( 0g ` P ) )
24 18 23 breqtrrd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I = { ( 0g ` P ) } ) -> ( G ` I ) .|| X )
25 simpl1 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> R e. DivRing )
26 25 5 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> R e. Ring )
27 simpl2 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> I e. U )
28 27 10 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> I C_ ( Base ` P ) )
29 simpl3 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> X e. I )
30 28 29 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> X e. ( Base ` P ) )
31 simpr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> I =/= { ( 0g ` P ) } )
32 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
33 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
34 1 2 15 3 32 33 ig1pval3 
 |-  ( ( R e. DivRing /\ I e. U /\ I =/= { ( 0g ` P ) } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` ( G ` I ) ) = inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) ) )
35 25 27 31 34 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( G ` I ) e. I /\ ( G ` I ) e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` ( G ` I ) ) = inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) ) )
36 35 simp2d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. ( Monic1p ` R ) )
37 eqid 
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
38 37 33 mon1puc1p 
 |-  ( ( R e. Ring /\ ( G ` I ) e. ( Monic1p ` R ) ) -> ( G ` I ) e. ( Unic1p ` R ) )
39 26 36 38 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. ( Unic1p ` R ) )
40 eqid 
 |-  ( rem1p ` R ) = ( rem1p ` R )
41 40 1 9 37 32 r1pdeglt 
 |-  ( ( R e. Ring /\ X e. ( Base ` P ) /\ ( G ` I ) e. ( Unic1p ` R ) ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) < ( ( deg1 ` R ) ` ( G ` I ) ) )
42 26 30 39 41 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) < ( ( deg1 ` R ) ` ( G ` I ) ) )
43 35 simp3d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) ` ( G ` I ) ) = inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) )
44 42 43 breqtrd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) < inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) )
45 32 1 9 deg1xrf 
 |-  ( deg1 ` R ) : ( Base ` P ) --> RR*
46 35 simp1d 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. I )
47 28 46 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) e. ( Base ` P ) )
48 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
49 eqid 
 |-  ( .r ` P ) = ( .r ` P )
50 eqid 
 |-  ( -g ` P ) = ( -g ` P )
51 40 1 9 48 49 50 r1pval 
 |-  ( ( X e. ( Base ` P ) /\ ( G ` I ) e. ( Base ` P ) ) -> ( X ( rem1p ` R ) ( G ` I ) ) = ( X ( -g ` P ) ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) ) )
52 30 47 51 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( rem1p ` R ) ( G ` I ) ) = ( X ( -g ` P ) ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) ) )
53 26 6 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> P e. Ring )
54 48 1 9 37 q1pcl 
 |-  ( ( R e. Ring /\ X e. ( Base ` P ) /\ ( G ` I ) e. ( Unic1p ` R ) ) -> ( X ( quot1p ` R ) ( G ` I ) ) e. ( Base ` P ) )
55 26 30 39 54 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( quot1p ` R ) ( G ` I ) ) e. ( Base ` P ) )
56 3 9 49 lidlmcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( ( X ( quot1p ` R ) ( G ` I ) ) e. ( Base ` P ) /\ ( G ` I ) e. I ) ) -> ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) e. I )
57 53 27 55 46 56 syl22anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) e. I )
58 3 50 lidlsubcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( X e. I /\ ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) e. I ) ) -> ( X ( -g ` P ) ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) ) e. I )
59 53 27 29 57 58 syl22anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( -g ` P ) ( ( X ( quot1p ` R ) ( G ` I ) ) ( .r ` P ) ( G ` I ) ) ) e. I )
60 52 59 eqeltrd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( rem1p ` R ) ( G ` I ) ) e. I )
61 28 60 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( rem1p ` R ) ( G ` I ) ) e. ( Base ` P ) )
62 ffvelcdm 
 |-  ( ( ( deg1 ` R ) : ( Base ` P ) --> RR* /\ ( X ( rem1p ` R ) ( G ` I ) ) e. ( Base ` P ) ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. RR* )
63 45 61 62 sylancr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. RR* )
64 28 ssdifd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( I \ { ( 0g ` P ) } ) C_ ( ( Base ` P ) \ { ( 0g ` P ) } ) )
65 imass2 
 |-  ( ( I \ { ( 0g ` P ) } ) C_ ( ( Base ` P ) \ { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ( deg1 ` R ) " ( ( Base ` P ) \ { ( 0g ` P ) } ) ) )
66 64 65 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ( deg1 ` R ) " ( ( Base ` P ) \ { ( 0g ` P ) } ) ) )
67 32 1 15 9 deg1n0ima 
 |-  ( R e. Ring -> ( ( deg1 ` R ) " ( ( Base ` P ) \ { ( 0g ` P ) } ) ) C_ NN0 )
68 26 67 syl 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( ( Base ` P ) \ { ( 0g ` P ) } ) ) C_ NN0 )
69 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
70 68 69 sseqtrdi 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( ( Base ` P ) \ { ( 0g ` P ) } ) ) C_ ( ZZ>= ` 0 ) )
71 66 70 sstrd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ZZ>= ` 0 ) )
72 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
73 zssre 
 |-  ZZ C_ RR
74 ressxr 
 |-  RR C_ RR*
75 73 74 sstri 
 |-  ZZ C_ RR*
76 72 75 sstri 
 |-  ( ZZ>= ` 0 ) C_ RR*
77 71 76 sstrdi 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ RR* )
78 3 15 lidl0cl 
 |-  ( ( P e. Ring /\ I e. U ) -> ( 0g ` P ) e. I )
79 53 27 78 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( 0g ` P ) e. I )
80 79 snssd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> { ( 0g ` P ) } C_ I )
81 31 necomd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> { ( 0g ` P ) } =/= I )
82 pssdifn0 
 |-  ( ( { ( 0g ` P ) } C_ I /\ { ( 0g ` P ) } =/= I ) -> ( I \ { ( 0g ` P ) } ) =/= (/) )
83 80 81 82 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( I \ { ( 0g ` P ) } ) =/= (/) )
84 ffn 
 |-  ( ( deg1 ` R ) : ( Base ` P ) --> RR* -> ( deg1 ` R ) Fn ( Base ` P ) )
85 45 84 ax-mp 
 |-  ( deg1 ` R ) Fn ( Base ` P )
86 28 ssdifssd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( I \ { ( 0g ` P ) } ) C_ ( Base ` P ) )
87 fnimaeq0 
 |-  ( ( ( deg1 ` R ) Fn ( Base ` P ) /\ ( I \ { ( 0g ` P ) } ) C_ ( Base ` P ) ) -> ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) = (/) <-> ( I \ { ( 0g ` P ) } ) = (/) ) )
88 85 86 87 sylancr 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) = (/) <-> ( I \ { ( 0g ` P ) } ) = (/) ) )
89 88 necon3bid 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) =/= (/) <-> ( I \ { ( 0g ` P ) } ) =/= (/) ) )
90 83 89 mpbird 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) =/= (/) )
91 infssuzcl 
 |-  ( ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ZZ>= ` 0 ) /\ ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) =/= (/) ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) e. ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) )
92 71 90 91 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) e. ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) )
93 77 92 sseldd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) e. RR* )
94 xrltnle 
 |-  ( ( ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. RR* /\ inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) e. RR* ) -> ( ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) < inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <-> -. inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) ) )
95 63 93 94 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) < inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <-> -. inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) ) )
96 44 95 mpbid 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> -. inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) )
97 71 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ZZ>= ` 0 ) )
98 60 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> ( X ( rem1p ` R ) ( G ` I ) ) e. I )
99 simpr 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) )
100 eldifsn 
 |-  ( ( X ( rem1p ` R ) ( G ` I ) ) e. ( I \ { ( 0g ` P ) } ) <-> ( ( X ( rem1p ` R ) ( G ` I ) ) e. I /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) )
101 98 99 100 sylanbrc 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> ( X ( rem1p ` R ) ( G ` I ) ) e. ( I \ { ( 0g ` P ) } ) )
102 fnfvima 
 |-  ( ( ( deg1 ` R ) Fn ( Base ` P ) /\ ( I \ { ( 0g ` P ) } ) C_ ( Base ` P ) /\ ( X ( rem1p ` R ) ( G ` I ) ) e. ( I \ { ( 0g ` P ) } ) ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) )
103 85 86 101 102 mp3an2ani 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) )
104 infssuzle 
 |-  ( ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) C_ ( ZZ>= ` 0 ) /\ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) e. ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) )
105 97 103 104 syl2anc 
 |-  ( ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) /\ ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) )
106 105 ex 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( X ( rem1p ` R ) ( G ` I ) ) =/= ( 0g ` P ) -> inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) ) )
107 106 necon1bd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( -. inf ( ( ( deg1 ` R ) " ( I \ { ( 0g ` P ) } ) ) , RR , < ) <_ ( ( deg1 ` R ) ` ( X ( rem1p ` R ) ( G ` I ) ) ) -> ( X ( rem1p ` R ) ( G ` I ) ) = ( 0g ` P ) ) )
108 96 107 mpd 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( X ( rem1p ` R ) ( G ` I ) ) = ( 0g ` P ) )
109 1 4 9 37 15 40 dvdsr1p 
 |-  ( ( R e. Ring /\ X e. ( Base ` P ) /\ ( G ` I ) e. ( Unic1p ` R ) ) -> ( ( G ` I ) .|| X <-> ( X ( rem1p ` R ) ( G ` I ) ) = ( 0g ` P ) ) )
110 26 30 39 109 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( ( G ` I ) .|| X <-> ( X ( rem1p ` R ) ( G ` I ) ) = ( 0g ` P ) ) )
111 108 110 mpbird 
 |-  ( ( ( R e. DivRing /\ I e. U /\ X e. I ) /\ I =/= { ( 0g ` P ) } ) -> ( G ` I ) .|| X )
112 24 111 pm2.61dane 
 |-  ( ( R e. DivRing /\ I e. U /\ X e. I ) -> ( G ` I ) .|| X )