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 eqtrid 
 |-  ( 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 )