Metamath Proof Explorer


Theorem coeid

Description: Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 A = coeff F
dgrub.2 N = deg F
Assertion coeid F Poly S F = z k = 0 N A k z k

Proof

Step Hyp Ref Expression
1 dgrub.1 A = coeff F
2 dgrub.2 N = deg F
3 elply2 F Poly S S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m
4 3 simprbi F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m
5 simpll F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F Poly S
6 simplrl F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m n 0
7 simplrr F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m a S 0 0
8 simprl F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m a n + 1 = 0
9 simprr F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F = x m = 0 n a m x m
10 fveq2 m = k a m = a k
11 oveq2 m = k x m = x k
12 10 11 oveq12d m = k a m x m = a k x k
13 12 cbvsumv m = 0 n a m x m = k = 0 n a k x k
14 oveq1 x = z x k = z k
15 14 oveq2d x = z a k x k = a k z k
16 15 sumeq2sdv x = z k = 0 n a k x k = k = 0 n a k z k
17 13 16 syl5eq x = z m = 0 n a m x m = k = 0 n a k z k
18 17 cbvmptv x m = 0 n a m x m = z k = 0 n a k z k
19 9 18 eqtrdi F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F = z k = 0 n a k z k
20 1 2 5 6 7 8 19 coeidlem F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F = z k = 0 N A k z k
21 20 ex F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F = z k = 0 N A k z k
22 21 rexlimdvva F Poly S n 0 a S 0 0 a n + 1 = 0 F = x m = 0 n a m x m F = z k = 0 N A k z k
23 4 22 mpd F Poly S F = z k = 0 N A k z k