Metamath Proof Explorer


Theorem coeeq

Description: If A satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses coeeq.1 φ F Poly S
coeeq.2 φ N 0
coeeq.3 φ A : 0
coeeq.4 φ A N + 1 = 0
coeeq.5 φ F = z k = 0 N A k z k
Assertion coeeq φ coeff F = A

Proof

Step Hyp Ref Expression
1 coeeq.1 φ F Poly S
2 coeeq.2 φ N 0
3 coeeq.3 φ A : 0
4 coeeq.4 φ A N + 1 = 0
5 coeeq.5 φ F = z k = 0 N A k z k
6 coeval F Poly S coeff F = ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
7 1 6 syl φ coeff F = ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k
8 fvoveq1 n = N n + 1 = N + 1
9 8 imaeq2d n = N A n + 1 = A N + 1
10 9 eqeq1d n = N A n + 1 = 0 A N + 1 = 0
11 oveq2 n = N 0 n = 0 N
12 11 sumeq1d n = N k = 0 n A k z k = k = 0 N A k z k
13 12 mpteq2dv n = N z k = 0 n A k z k = z k = 0 N A k z k
14 13 eqeq2d n = N F = z k = 0 n A k z k F = z k = 0 N A k z k
15 10 14 anbi12d n = N A n + 1 = 0 F = z k = 0 n A k z k A N + 1 = 0 F = z k = 0 N A k z k
16 15 rspcev N 0 A N + 1 = 0 F = z k = 0 N A k z k n 0 A n + 1 = 0 F = z k = 0 n A k z k
17 2 4 5 16 syl12anc φ n 0 A n + 1 = 0 F = z k = 0 n A k z k
18 cnex V
19 nn0ex 0 V
20 18 19 elmap A 0 A : 0
21 3 20 sylibr φ A 0
22 coeeu F Poly S ∃! a 0 n 0 a n + 1 = 0 F = z k = 0 n a k z k
23 1 22 syl φ ∃! a 0 n 0 a n + 1 = 0 F = z k = 0 n a k z k
24 imaeq1 a = A a n + 1 = A n + 1
25 24 eqeq1d a = A a n + 1 = 0 A n + 1 = 0
26 fveq1 a = A a k = A k
27 26 oveq1d a = A a k z k = A k z k
28 27 sumeq2sdv a = A k = 0 n a k z k = k = 0 n A k z k
29 28 mpteq2dv a = A z k = 0 n a k z k = z k = 0 n A k z k
30 29 eqeq2d a = A F = z k = 0 n a k z k F = z k = 0 n A k z k
31 25 30 anbi12d a = A a n + 1 = 0 F = z k = 0 n a k z k A n + 1 = 0 F = z k = 0 n A k z k
32 31 rexbidv a = A n 0 a n + 1 = 0 F = z k = 0 n a k z k n 0 A n + 1 = 0 F = z k = 0 n A k z k
33 32 riota2 A 0 ∃! a 0 n 0 a n + 1 = 0 F = z k = 0 n a k z k 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
34 21 23 33 syl2anc φ 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
35 17 34 mpbid φ ι a 0 | n 0 a n + 1 = 0 F = z k = 0 n a k z k = A
36 7 35 eqtrd φ coeff F = A