Metamath Proof Explorer


Theorem hbtlem7

Description: Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses hbtlem.p
|- P = ( Poly1 ` R )
hbtlem.u
|- U = ( LIdeal ` P )
hbtlem.s
|- S = ( ldgIdlSeq ` R )
hbtlem7.t
|- T = ( LIdeal ` R )
Assertion hbtlem7
|- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) : NN0 --> 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 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 )