Step |
Hyp |
Ref |
Expression |
1 |
|
hbtlem.p |
|- P = ( Poly1 ` R ) |
2 |
|
hbtlem.u |
|- U = ( LIdeal ` P ) |
3 |
|
hbtlem.s |
|- S = ( ldgIdlSeq ` R ) |
4 |
|
hbtlem7.t |
|- T = ( LIdeal ` R ) |
5 |
|
simpr |
|- ( ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) -> y = ( ( coe1 ` j ) ` x ) ) |
6 |
5
|
reximi |
|- ( E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) -> E. j e. I y = ( ( coe1 ` j ) ` x ) ) |
7 |
6
|
ss2abi |
|- { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } C_ { y | E. j e. I y = ( ( coe1 ` j ) ` x ) } |
8 |
|
abrexexg |
|- ( I e. U -> { y | E. j e. I y = ( ( coe1 ` j ) ` x ) } e. _V ) |
9 |
|
ssexg |
|- ( ( { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } C_ { y | E. j e. I y = ( ( coe1 ` j ) ` x ) } /\ { y | E. j e. I y = ( ( coe1 ` j ) ` x ) } e. _V ) -> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } e. _V ) |
10 |
7 8 9
|
sylancr |
|- ( I e. U -> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } e. _V ) |
11 |
10
|
ralrimivw |
|- ( I e. U -> A. x e. NN0 { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } e. _V ) |
12 |
11
|
adantl |
|- ( ( R e. Ring /\ I e. U ) -> A. x e. NN0 { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } e. _V ) |
13 |
|
eqid |
|- ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) = ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) |
14 |
13
|
fnmpt |
|- ( A. x e. NN0 { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } e. _V -> ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) Fn NN0 ) |
15 |
12 14
|
syl |
|- ( ( R e. Ring /\ I e. U ) -> ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) Fn NN0 ) |
16 |
|
elex |
|- ( R e. Ring -> R e. _V ) |
17 |
|
fveq2 |
|- ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) ) |
18 |
17 1
|
eqtr4di |
|- ( r = R -> ( Poly1 ` r ) = P ) |
19 |
18
|
fveq2d |
|- ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = ( LIdeal ` P ) ) |
20 |
19 2
|
eqtr4di |
|- ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = U ) |
21 |
|
fveq2 |
|- ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) ) |
22 |
21
|
fveq1d |
|- ( r = R -> ( ( deg1 ` r ) ` j ) = ( ( deg1 ` R ) ` j ) ) |
23 |
22
|
breq1d |
|- ( r = R -> ( ( ( deg1 ` r ) ` j ) <_ x <-> ( ( deg1 ` R ) ` j ) <_ x ) ) |
24 |
23
|
anbi1d |
|- ( r = R -> ( ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) <-> ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) ) ) |
25 |
24
|
rexbidv |
|- ( r = R -> ( E. j e. i ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) <-> E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) ) ) |
26 |
25
|
abbidv |
|- ( r = R -> { y | E. j e. i ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } = { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) |
27 |
26
|
mpteq2dv |
|- ( r = R -> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) = ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) |
28 |
20 27
|
mpteq12dv |
|- ( r = R -> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) = ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ) |
29 |
|
df-ldgis |
|- ldgIdlSeq = ( r e. _V |-> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` r ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ) |
30 |
28 29 2
|
mptfvmpt |
|- ( R e. _V -> ( ldgIdlSeq ` R ) = ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ) |
31 |
16 30
|
syl |
|- ( R e. Ring -> ( ldgIdlSeq ` R ) = ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ) |
32 |
3 31
|
syl5eq |
|- ( R e. Ring -> S = ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ) |
33 |
32
|
fveq1d |
|- ( R e. Ring -> ( S ` I ) = ( ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ` I ) ) |
34 |
|
rexeq |
|- ( i = I -> ( E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) <-> E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) ) ) |
35 |
34
|
abbidv |
|- ( i = I -> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } = { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) |
36 |
35
|
mpteq2dv |
|- ( i = I -> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) = ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) |
37 |
|
eqid |
|- ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) = ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) |
38 |
|
nn0ex |
|- NN0 e. _V |
39 |
38
|
mptex |
|- ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) e. _V |
40 |
36 37 39
|
fvmpt |
|- ( I e. U -> ( ( i e. U |-> ( x e. NN0 |-> { y | E. j e. i ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) ` I ) = ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) |
41 |
33 40
|
sylan9eq |
|- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) = ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) ) |
42 |
41
|
fneq1d |
|- ( ( R e. Ring /\ I e. U ) -> ( ( S ` I ) Fn NN0 <-> ( x e. NN0 |-> { y | E. j e. I ( ( ( deg1 ` R ) ` j ) <_ x /\ y = ( ( coe1 ` j ) ` x ) ) } ) Fn NN0 ) ) |
43 |
15 42
|
mpbird |
|- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) Fn NN0 ) |
44 |
1 2 3 4
|
hbtlem2 |
|- ( ( R e. Ring /\ I e. U /\ x e. NN0 ) -> ( ( S ` I ) ` x ) e. T ) |
45 |
44
|
3expa |
|- ( ( ( R e. Ring /\ I e. U ) /\ x e. NN0 ) -> ( ( S ` I ) ` x ) e. T ) |
46 |
45
|
ralrimiva |
|- ( ( R e. Ring /\ I e. U ) -> A. x e. NN0 ( ( S ` I ) ` x ) e. T ) |
47 |
|
ffnfv |
|- ( ( S ` I ) : NN0 --> T <-> ( ( S ` I ) Fn NN0 /\ A. x e. NN0 ( ( S ` I ) ` x ) e. T ) ) |
48 |
43 46 47
|
sylanbrc |
|- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) : NN0 --> T ) |