Metamath Proof Explorer

Theorem hbtlem1

Description: Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Hypotheses hbtlem.p 
|- P = ( Poly1 ` R )
hbtlem.u 
|- U = ( LIdeal ` P )
hbtlem.s 
|- S = ( ldgIdlSeq ` R )
hbtlem.d 
|- D = ( deg1 ` R )
Assertion hbtlem1 
|- ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } )

Proof

Step Hyp Ref Expression
1 hbtlem.p 
 |-  P = ( Poly1 ` R )
2 hbtlem.u 
 |-  U = ( LIdeal ` P )
3 hbtlem.s 
 |-  S = ( ldgIdlSeq ` R )
4 hbtlem.d 
 |-  D = ( deg1 ` R )
5 elex 
 |-  ( R e. V -> R e. _V )
6 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
7 6 1 eqtr4di 
 |-  ( r = R -> ( Poly1 ` r ) = P )
8 7 fveq2d 
 |-  ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = ( LIdeal ` P ) )
9 8 2 eqtr4di 
 |-  ( r = R -> ( LIdeal ` ( Poly1 ` r ) ) = U )
10 fveq2 
 |-  ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) )
11 10 4 eqtr4di 
 |-  ( r = R -> ( deg1 ` r ) = D )
12 11 fveq1d 
 |-  ( r = R -> ( ( deg1 ` r ) ` k ) = ( D ` k ) )
13 12 breq1d 
 |-  ( r = R -> ( ( ( deg1 ` r ) ` k ) <_ x <-> ( D ` k ) <_ x ) )
14 13 anbi1d 
 |-  ( r = R -> ( ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) <-> ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) ) )
15 14 rexbidv 
 |-  ( r = R -> ( E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) <-> E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) ) )
16 15 abbidv 
 |-  ( r = R -> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } = { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } )
17 16 mpteq2dv 
 |-  ( r = R -> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) = ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) )
18 9 17 mpteq12dv 
 |-  ( r = R -> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) = ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
19 df-ldgis 
 |-  ldgIdlSeq = ( r e. _V |-> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
20 18 19 2 mptfvmpt 
 |-  ( R e. _V -> ( ldgIdlSeq ` R ) = ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
21 5 20 syl 
 |-  ( R e. V -> ( ldgIdlSeq ` R ) = ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
22 3 21 syl5eq 
 |-  ( R e. V -> S = ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
23 22 fveq1d 
 |-  ( R e. V -> ( S ` I ) = ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) )
24 23 fveq1d 
 |-  ( R e. V -> ( ( S ` I ) ` X ) = ( ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) ` X ) )
25 24 3ad2ant1 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = ( ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) ` X ) )
26 rexeq 
 |-  ( i = I -> ( E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) <-> E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) ) )
27 26 abbidv 
 |-  ( i = I -> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } = { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } )
28 27 mpteq2dv 
 |-  ( i = I -> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) = ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) )
29 eqid 
 |-  ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) = ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) )
30 nn0ex 
 |-  NN0 e. _V
31 30 mptex 
 |-  ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) e. _V
32 28 29 31 fvmpt 
 |-  ( I e. U -> ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) = ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) )
33 32 fveq1d 
 |-  ( I e. U -> ( ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) ` X ) = ( ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ` X ) )
34 33 3ad2ant2 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( ( i e. U |-> ( x e. NN0 |-> { j | E. k e. i ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) ` I ) ` X ) = ( ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ` X ) )
35 eqid 
 |-  ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) = ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } )
36 breq2 
 |-  ( x = X -> ( ( D ` k ) <_ x <-> ( D ` k ) <_ X ) )
37 fveq2 
 |-  ( x = X -> ( ( coe1 ` k ) ` x ) = ( ( coe1 ` k ) ` X ) )
38 37 eqeq2d 
 |-  ( x = X -> ( j = ( ( coe1 ` k ) ` x ) <-> j = ( ( coe1 ` k ) ` X ) ) )
39 36 38 anbi12d 
 |-  ( x = X -> ( ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) <-> ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) ) )
40 39 rexbidv 
 |-  ( x = X -> ( E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) <-> E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) ) )
41 40 abbidv 
 |-  ( x = X -> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } )
42 simp3 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> X e. NN0 )
43 simpr 
 |-  ( ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) -> j = ( ( coe1 ` k ) ` X ) )
44 43 reximi 
 |-  ( E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) -> E. k e. I j = ( ( coe1 ` k ) ` X ) )
45 44 ss2abi 
 |-  { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } C_ { j | E. k e. I j = ( ( coe1 ` k ) ` X ) }
46 abrexexg 
 |-  ( I e. U -> { j | E. k e. I j = ( ( coe1 ` k ) ` X ) } e. _V )
47 46 3ad2ant2 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> { j | E. k e. I j = ( ( coe1 ` k ) ` X ) } e. _V )
48 ssexg 
 |-  ( ( { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } C_ { j | E. k e. I j = ( ( coe1 ` k ) ` X ) } /\ { j | E. k e. I j = ( ( coe1 ` k ) ` X ) } e. _V ) -> { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } e. _V )
49 45 47 48 sylancr 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } e. _V )
50 35 41 42 49 fvmptd3 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( x e. NN0 |-> { j | E. k e. I ( ( D ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ` X ) = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } )
51 25 34 50 3eqtrd 
 |-  ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( ( coe1 ` k ) ` X ) ) } )