Metamath Proof Explorer


Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coelem F Poly S coeff F 0 n 0 coeff F n + 1 = 0 F = z k = 0 n coeff F k z k

Proof

Step Hyp Ref Expression
1 coeval F Poly S coeff F = ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
2 coeeu F Poly S ∃! a 0 n 0 a n + 1 = 0 F = z k = 0 n a k z k
3 riotacl2 ∃! a 0 n 0 a n + 1 = 0 F = z k = 0 n a k z k ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
4 2 3 syl F Poly S ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
5 1 4 eqeltrd F Poly S coeff F a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
6 imaeq1 a = coeff F a n + 1 = coeff F n + 1
7 6 eqeq1d a = coeff F a n + 1 = 0 coeff F n + 1 = 0
8 fveq1 a = coeff F a k = coeff F k
9 8 oveq1d a = coeff F a k z k = coeff F k z k
10 9 sumeq2sdv a = coeff F k = 0 n a k z k = k = 0 n coeff F k z k
11 10 mpteq2dv a = coeff F z k = 0 n a k z k = z k = 0 n coeff F k z k
12 11 eqeq2d a = coeff F F = z k = 0 n a k z k F = z k = 0 n coeff F k z k
13 7 12 anbi12d a = coeff F a n + 1 = 0 F = z k = 0 n a k z k coeff F n + 1 = 0 F = z k = 0 n coeff F k z k
14 13 rexbidv a = coeff F n 0 a n + 1 = 0 F = z k = 0 n a k z k n 0 coeff F n + 1 = 0 F = z k = 0 n coeff F k z k
15 14 elrab coeff F a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k coeff F 0 n 0 coeff F n + 1 = 0 F = z k = 0 n coeff F k z k
16 5 15 sylib F Poly S coeff F 0 n 0 coeff F n + 1 = 0 F = z k = 0 n coeff F k z k