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=Poly1R
hbtlem.u U=LIdealP
hbtlem.s S=ldgIdlSeqR
hbtlem.d D=deg1R
Assertion hbtlem1 RVIUX0SIX=j|kIDkXj=coe1kX

Proof

Step Hyp Ref Expression
1 hbtlem.p P=Poly1R
2 hbtlem.u U=LIdealP
3 hbtlem.s S=ldgIdlSeqR
4 hbtlem.d D=deg1R
5 elex RVRV
6 fveq2 r=RPoly1r=Poly1R
7 6 1 eqtr4di r=RPoly1r=P
8 7 fveq2d r=RLIdealPoly1r=LIdealP
9 8 2 eqtr4di r=RLIdealPoly1r=U
10 fveq2 r=Rdeg1r=deg1R
11 10 4 eqtr4di r=Rdeg1r=D
12 11 fveq1d r=Rdeg1rk=Dk
13 12 breq1d r=Rdeg1rkxDkx
14 13 anbi1d r=Rdeg1rkxj=coe1kxDkxj=coe1kx
15 14 rexbidv r=Rkideg1rkxj=coe1kxkiDkxj=coe1kx
16 15 abbidv r=Rj|kideg1rkxj=coe1kx=j|kiDkxj=coe1kx
17 16 mpteq2dv r=Rx0j|kideg1rkxj=coe1kx=x0j|kiDkxj=coe1kx
18 9 17 mpteq12dv r=RiLIdealPoly1rx0j|kideg1rkxj=coe1kx=iUx0j|kiDkxj=coe1kx
19 df-ldgis ldgIdlSeq=rViLIdealPoly1rx0j|kideg1rkxj=coe1kx
20 18 19 2 mptfvmpt RVldgIdlSeqR=iUx0j|kiDkxj=coe1kx
21 5 20 syl RVldgIdlSeqR=iUx0j|kiDkxj=coe1kx
22 3 21 eqtrid RVS=iUx0j|kiDkxj=coe1kx
23 22 fveq1d RVSI=iUx0j|kiDkxj=coe1kxI
24 23 fveq1d RVSIX=iUx0j|kiDkxj=coe1kxIX
25 24 3ad2ant1 RVIUX0SIX=iUx0j|kiDkxj=coe1kxIX
26 rexeq i=IkiDkxj=coe1kxkIDkxj=coe1kx
27 26 abbidv i=Ij|kiDkxj=coe1kx=j|kIDkxj=coe1kx
28 27 mpteq2dv i=Ix0j|kiDkxj=coe1kx=x0j|kIDkxj=coe1kx
29 eqid iUx0j|kiDkxj=coe1kx=iUx0j|kiDkxj=coe1kx
30 nn0ex 0V
31 30 mptex x0j|kIDkxj=coe1kxV
32 28 29 31 fvmpt IUiUx0j|kiDkxj=coe1kxI=x0j|kIDkxj=coe1kx
33 32 fveq1d IUiUx0j|kiDkxj=coe1kxIX=x0j|kIDkxj=coe1kxX
34 33 3ad2ant2 RVIUX0iUx0j|kiDkxj=coe1kxIX=x0j|kIDkxj=coe1kxX
35 eqid x0j|kIDkxj=coe1kx=x0j|kIDkxj=coe1kx
36 breq2 x=XDkxDkX
37 fveq2 x=Xcoe1kx=coe1kX
38 37 eqeq2d x=Xj=coe1kxj=coe1kX
39 36 38 anbi12d x=XDkxj=coe1kxDkXj=coe1kX
40 39 rexbidv x=XkIDkxj=coe1kxkIDkXj=coe1kX
41 40 abbidv x=Xj|kIDkxj=coe1kx=j|kIDkXj=coe1kX
42 simp3 RVIUX0X0
43 simpr DkXj=coe1kXj=coe1kX
44 43 reximi kIDkXj=coe1kXkIj=coe1kX
45 44 ss2abi j|kIDkXj=coe1kXj|kIj=coe1kX
46 abrexexg IUj|kIj=coe1kXV
47 46 3ad2ant2 RVIUX0j|kIj=coe1kXV
48 ssexg j|kIDkXj=coe1kXj|kIj=coe1kXj|kIj=coe1kXVj|kIDkXj=coe1kXV
49 45 47 48 sylancr RVIUX0j|kIDkXj=coe1kXV
50 35 41 42 49 fvmptd3 RVIUX0x0j|kIDkxj=coe1kxX=j|kIDkXj=coe1kX
51 25 34 50 3eqtrd RVIUX0SIX=j|kIDkXj=coe1kX