Metamath Proof Explorer

Theorem hbtlem2

Description: Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p 
|- P = ( Poly1 ` R )
hbtlem.u 
|- U = ( LIdeal ` P )
hbtlem.s 
|- S = ( ldgIdlSeq ` R )
hbtlem2.t 
|- T = ( LIdeal ` R )
Assertion hbtlem2 
|- ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) e. T )

Proof

Step Hyp Ref Expression
1 hbtlem.p 
 |-  P = ( Poly1 ` R )
2 hbtlem.u 
 |-  U = ( LIdeal ` P )
3 hbtlem.s 
 |-  S = ( ldgIdlSeq ` R )
4 hbtlem2.t 
 |-  T = ( LIdeal ` R )
5 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
6 1 2 3 5 hbtlem1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
8 7 2 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
9 8 3ad2ant2 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> I C_ ( Base ` P ) )
10 9 sselda 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> b e. ( Base ` P ) )
11 eqid 
 |-  ( coe1 ` b ) = ( coe1 ` b )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 11 7 1 12 coe1f 
 |-  ( b e. ( Base ` P ) -> ( coe1 ` b ) : NN0 --> ( Base ` R ) )
14 10 13 syl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> ( coe1 ` b ) : NN0 --> ( Base ` R ) )
15 simpl3 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> X e. NN0 )
16 14 15 ffvelcdmd 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> ( ( coe1 ` b ) ` X ) e. ( Base ` R ) )
17 eleq1a 
 |-  ( ( ( coe1 ` b ) ` X ) e. ( Base ` R ) -> ( a = ( ( coe1 ` b ) ` X ) -> a e. ( Base ` R ) ) )
18 16 17 syl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> ( a = ( ( coe1 ` b ) ` X ) -> a e. ( Base ` R ) ) )
19 18 adantld 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ b e. I ) -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) -> a e. ( Base ` R ) ) )
20 19 rexlimdva 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) -> a e. ( Base ` R ) ) )
21 20 abssdv 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } C_ ( Base ` R ) )
22 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
23 22 3ad2ant1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> P e. Ring )
24 simp2 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> I e. U )
25 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
26 2 25 lidl0cl 
 |-  ( ( P e. Ring /\ I e. U ) -> ( 0g ` P ) e. I )
27 23 24 26 syl2anc 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( 0g ` P ) e. I )
28 5 1 25 deg1z 
 |-  ( R e. Ring -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
29 28 3ad2ant1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
30 nn0ssre 
 |-  NN0 C_ RR
31 ressxr 
 |-  RR C_ RR*
32 30 31 sstri 
 |-  NN0 C_ RR*
33 simp3 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> X e. NN0 )
34 32 33 sselid 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> X e. RR* )
35 mnfle 
 |-  ( X e. RR* -> -oo <_ X )
36 34 35 syl 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> -oo <_ X )
37 29 36 eqbrtrd 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( deg1 ` R ) ` ( 0g ` P ) ) <_ X )
38 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
39 1 25 38 coe1z 
 |-  ( R e. Ring -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
40 39 3ad2ant1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
41 40 fveq1d 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( coe1 ` ( 0g ` P ) ) ` X ) = ( ( NN0 X. { ( 0g ` R ) } ) ` X ) )
42 fvex 
 |-  ( 0g ` R ) e. _V
43 42 fvconst2 
 |-  ( X e. NN0 -> ( ( NN0 X. { ( 0g ` R ) } ) ` X ) = ( 0g ` R ) )
44 43 3ad2ant3 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` X ) = ( 0g ` R ) )
45 41 44 eqtr2d 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( 0g ` R ) = ( ( coe1 ` ( 0g ` P ) ) ` X ) )
46 fveq2 
 |-  ( b = ( 0g ` P ) -> ( ( deg1 ` R ) ` b ) = ( ( deg1 ` R ) ` ( 0g ` P ) ) )
47 46 breq1d 
 |-  ( b = ( 0g ` P ) -> ( ( ( deg1 ` R ) ` b ) <_ X <-> ( ( deg1 ` R ) ` ( 0g ` P ) ) <_ X ) )
48 fveq2 
 |-  ( b = ( 0g ` P ) -> ( coe1 ` b ) = ( coe1 ` ( 0g ` P ) ) )
49 48 fveq1d 
 |-  ( b = ( 0g ` P ) -> ( ( coe1 ` b ) ` X ) = ( ( coe1 ` ( 0g ` P ) ) ` X ) )
50 49 eqeq2d 
 |-  ( b = ( 0g ` P ) -> ( ( 0g ` R ) = ( ( coe1 ` b ) ` X ) <-> ( 0g ` R ) = ( ( coe1 ` ( 0g ` P ) ) ` X ) ) )
51 47 50 anbi12d 
 |-  ( b = ( 0g ` P ) -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` ( 0g ` P ) ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` ( 0g ` P ) ) ` X ) ) ) )
52 51 rspcev 
 |-  ( ( ( 0g ` P ) e. I /\ ( ( ( deg1 ` R ) ` ( 0g ` P ) ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` ( 0g ` P ) ) ` X ) ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) )
53 27 37 45 52 syl12anc 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) )
54 eqeq1 
 |-  ( a = ( 0g ` R ) -> ( a = ( ( coe1 ` b ) ` X ) <-> ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) )
55 54 anbi2d 
 |-  ( a = ( 0g ` R ) -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) ) )
56 55 rexbidv 
 |-  ( a = ( 0g ` R ) -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) ) )
57 42 56 elab 
 |-  ( ( 0g ` R ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( 0g ` R ) = ( ( coe1 ` b ) ` X ) ) )
58 53 57 sylibr 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( 0g ` R ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
59 58 ne0d 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } =/= (/) )
60 23 adantr 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> P e. Ring )
61 simpl2 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> I e. U )
62 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
63 1 62 12 7 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
64 63 3ad2ant1 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
65 64 adantr 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
66 simprl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> c e. ( Base ` R ) )
67 65 66 ffvelcdmd 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( algSc ` P ) ` c ) e. ( Base ` P ) )
68 simprll 
 |-  ( ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) -> f e. I )
69 68 adantl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> f e. I )
70 eqid 
 |-  ( .r ` P ) = ( .r ` P )
71 2 7 70 lidlmcl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( ( ( algSc ` P ) ` c ) e. ( Base ` P ) /\ f e. I ) ) -> ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. I )
72 60 61 67 69 71 syl22anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. I )
73 simprrl 
 |-  ( ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) -> g e. I )
74 73 adantl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> g e. I )
75 eqid 
 |-  ( +g ` P ) = ( +g ` P )
76 2 75 lidlacl 
 |-  ( ( ( P e. Ring /\ I e. U ) /\ ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. I /\ g e. I ) ) -> ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) e. I )
77 60 61 72 74 76 syl22anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) e. I )
78 simpl1 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> R e. Ring )
79 9 adantr 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> I C_ ( Base ` P ) )
80 79 69 sseldd 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> f e. ( Base ` P ) )
81 7 70 ringcl 
 |-  ( ( P e. Ring /\ ( ( algSc ` P ) ` c ) e. ( Base ` P ) /\ f e. ( Base ` P ) ) -> ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. ( Base ` P ) )
82 60 67 80 81 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. ( Base ` P ) )
83 79 74 sseldd 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> g e. ( Base ` P ) )
84 simpl3 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> X e. NN0 )
85 32 84 sselid 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> X e. RR* )
86 5 1 7 deg1xrcl 
 |-  ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. ( Base ` P ) -> ( ( deg1 ` R ) ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) e. RR* )
87 82 86 syl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) e. RR* )
88 5 1 7 deg1xrcl 
 |-  ( f e. ( Base ` P ) -> ( ( deg1 ` R ) ` f ) e. RR* )
89 80 88 syl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` f ) e. RR* )
90 5 1 12 7 70 62 deg1mul3le 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) /\ f e. ( Base ` P ) ) -> ( ( deg1 ` R ) ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) <_ ( ( deg1 ` R ) ` f ) )
91 78 66 80 90 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) <_ ( ( deg1 ` R ) ` f ) )
92 simprlr 
 |-  ( ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) -> ( ( deg1 ` R ) ` f ) <_ X )
93 92 adantl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` f ) <_ X )
94 87 89 85 91 93 xrletrd 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) <_ X )
95 simprrr 
 |-  ( ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) -> ( ( deg1 ` R ) ` g ) <_ X )
96 95 adantl 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` g ) <_ X )
97 1 5 78 7 75 82 83 85 94 96 deg1addle2 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) <_ X )
98 eqid 
 |-  ( +g ` R ) = ( +g ` R )
99 1 7 75 98 coe1addfv 
 |-  ( ( ( R e. Ring /\ ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) e. ( Base ` P ) /\ g e. ( Base ` P ) ) /\ X e. NN0 ) -> ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) = ( ( ( coe1 ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) ` X ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) )
100 78 82 83 84 99 syl31anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) = ( ( ( coe1 ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) ` X ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) )
101 eqid 
 |-  ( .r ` R ) = ( .r ` R )
102 1 7 12 62 70 101 coe1sclmulfv 
 |-  ( ( R e. Ring /\ ( c e. ( Base ` R ) /\ f e. ( Base ` P ) ) /\ X e. NN0 ) -> ( ( coe1 ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) ` X ) = ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) )
103 78 66 80 84 102 syl121anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( coe1 ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) ` X ) = ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) )
104 103 oveq1d 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( ( coe1 ` ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ) ` X ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) )
105 100 104 eqtr2d 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) )
106 fveq2 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( ( deg1 ` R ) ` b ) = ( ( deg1 ` R ) ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) )
107 106 breq1d 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( ( ( deg1 ` R ) ` b ) <_ X <-> ( ( deg1 ` R ) ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) <_ X ) )
108 fveq2 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( coe1 ` b ) = ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) )
109 108 fveq1d 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( ( coe1 ` b ) ` X ) = ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) )
110 109 eqeq2d 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) <-> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) ) )
111 107 110 anbi12d 
 |-  ( b = ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) ) ) )
112 111 rspcev 
 |-  ( ( ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) e. I /\ ( ( ( deg1 ` R ) ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` ( ( ( ( algSc ` P ) ` c ) ( .r ` P ) f ) ( +g ` P ) g ) ) ` X ) ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) )
113 77 97 105 112 syl12anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) )
114 ovex 
 |-  ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. _V
115 eqeq1 
 |-  ( a = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) -> ( a = ( ( coe1 ` b ) ` X ) <-> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) )
116 115 anbi2d 
 |-  ( a = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) ) )
117 116 rexbidv 
 |-  ( a = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) ) )
118 114 117 elab 
 |-  ( ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) = ( ( coe1 ` b ) ` X ) ) )
119 113 118 sylibr 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ ( c e. ( Base ` R ) /\ ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) ) ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
120 119 exp45 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( c e. ( Base ` R ) -> ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) -> ( ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) ) ) )
121 120 imp 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) -> ( ( f e. I /\ ( ( deg1 ` R ) ` f ) <_ X ) -> ( ( g e. I /\ ( ( deg1 ` R ) ` g ) <_ X ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) ) )
122 121 exp5c 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) -> ( f e. I -> ( ( ( deg1 ` R ) ` f ) <_ X -> ( g e. I -> ( ( ( deg1 ` R ) ` g ) <_ X -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) ) ) ) )
123 122 imp 
 |-  ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) -> ( ( ( deg1 ` R ) ` f ) <_ X -> ( g e. I -> ( ( ( deg1 ` R ) ` g ) <_ X -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) ) ) )
124 123 imp41 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ g e. I ) /\ ( ( deg1 ` R ) ` g ) <_ X ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
125 oveq2 
 |-  ( e = ( ( coe1 ` g ) ` X ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) )
126 125 eleq1d 
 |-  ( e = ( ( coe1 ` g ) ` X ) -> ( ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) ( ( coe1 ` g ) ` X ) ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
127 124 126 syl5ibrcom 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ g e. I ) /\ ( ( deg1 ` R ) ` g ) <_ X ) -> ( e = ( ( coe1 ` g ) ` X ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
128 127 expimpd 
 |-  ( ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) /\ g e. I ) -> ( ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
129 128 rexlimdva 
 |-  ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) -> ( E. g e. I ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
130 129 alrimiv 
 |-  ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) -> A. e ( E. g e. I ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
131 eqeq1 
 |-  ( a = e -> ( a = ( ( coe1 ` b ) ` X ) <-> e = ( ( coe1 ` b ) ` X ) ) )
132 131 anbi2d 
 |-  ( a = e -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) ) )
133 132 rexbidv 
 |-  ( a = e -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) ) )
134 fveq2 
 |-  ( b = g -> ( ( deg1 ` R ) ` b ) = ( ( deg1 ` R ) ` g ) )
135 134 breq1d 
 |-  ( b = g -> ( ( ( deg1 ` R ) ` b ) <_ X <-> ( ( deg1 ` R ) ` g ) <_ X ) )
136 fveq2 
 |-  ( b = g -> ( coe1 ` b ) = ( coe1 ` g ) )
137 136 fveq1d 
 |-  ( b = g -> ( ( coe1 ` b ) ` X ) = ( ( coe1 ` g ) ` X ) )
138 137 eqeq2d 
 |-  ( b = g -> ( e = ( ( coe1 ` b ) ` X ) <-> e = ( ( coe1 ` g ) ` X ) ) )
139 135 138 anbi12d 
 |-  ( b = g -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) ) )
140 139 cbvrexvw 
 |-  ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) <-> E. g e. I ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) )
141 133 140 bitrdi 
 |-  ( a = e -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. g e. I ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) ) )
142 141 ralab 
 |-  ( A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> A. e ( E. g e. I ( ( ( deg1 ` R ) ` g ) <_ X /\ e = ( ( coe1 ` g ) ` X ) ) -> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
143 130 142 sylibr 
 |-  ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
144 oveq2 
 |-  ( d = ( ( coe1 ` f ) ` X ) -> ( c ( .r ` R ) d ) = ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) )
145 144 oveq1d 
 |-  ( d = ( ( coe1 ` f ) ` X ) -> ( ( c ( .r ` R ) d ) ( +g ` R ) e ) = ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) )
146 145 eleq1d 
 |-  ( d = ( ( coe1 ` f ) ` X ) -> ( ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
147 146 ralbidv 
 |-  ( d = ( ( coe1 ` f ) ` X ) -> ( A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) ( ( coe1 ` f ) ` X ) ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
148 143 147 syl5ibrcom 
 |-  ( ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) /\ ( ( deg1 ` R ) ` f ) <_ X ) -> ( d = ( ( coe1 ` f ) ` X ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
149 148 expimpd 
 |-  ( ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) /\ f e. I ) -> ( ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
150 149 rexlimdva 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) -> ( E. f e. I ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
151 150 alrimiv 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) -> A. d ( E. f e. I ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
152 eqeq1 
 |-  ( a = d -> ( a = ( ( coe1 ` b ) ` X ) <-> d = ( ( coe1 ` b ) ` X ) ) )
153 152 anbi2d 
 |-  ( a = d -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) ) )
154 153 rexbidv 
 |-  ( a = d -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) ) )
155 fveq2 
 |-  ( b = f -> ( ( deg1 ` R ) ` b ) = ( ( deg1 ` R ) ` f ) )
156 155 breq1d 
 |-  ( b = f -> ( ( ( deg1 ` R ) ` b ) <_ X <-> ( ( deg1 ` R ) ` f ) <_ X ) )
157 fveq2 
 |-  ( b = f -> ( coe1 ` b ) = ( coe1 ` f ) )
158 157 fveq1d 
 |-  ( b = f -> ( ( coe1 ` b ) ` X ) = ( ( coe1 ` f ) ` X ) )
159 158 eqeq2d 
 |-  ( b = f -> ( d = ( ( coe1 ` b ) ` X ) <-> d = ( ( coe1 ` f ) ` X ) ) )
160 156 159 anbi12d 
 |-  ( b = f -> ( ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) <-> ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) ) )
161 160 cbvrexvw 
 |-  ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) <-> E. f e. I ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) )
162 154 161 bitrdi 
 |-  ( a = d -> ( E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) <-> E. f e. I ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) ) )
163 162 ralab 
 |-  ( A. d e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } <-> A. d ( E. f e. I ( ( ( deg1 ` R ) ` f ) <_ X /\ d = ( ( coe1 ` f ) ` X ) ) -> A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
164 151 163 sylibr 
 |-  ( ( ( R e. Ring /\ I e. U /\ X e. NN0 ) /\ c e. ( Base ` R ) ) -> A. d e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
165 164 ralrimiva 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> A. c e. ( Base ` R ) A. d e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } )
166 4 12 98 101 islidl 
 |-  ( { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } e. T <-> ( { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } C_ ( Base ` R ) /\ { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } =/= (/) /\ A. c e. ( Base ` R ) A. d e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } A. e e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ( ( c ( .r ` R ) d ) ( +g ` R ) e ) e. { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } ) )
167 21 59 165 166 syl3anbrc 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> { a | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ a = ( ( coe1 ` b ) ` X ) ) } e. T )
168 6 167 eqeltrd 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) e. T )