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 โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( Poly โ€˜ ๐‘† ) )
coeeq.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
coeeq.3 โŠข ( ๐œ‘ โ†’ ๐ด : โ„•0 โŸถ โ„‚ )
coeeq.4 โŠข ( ๐œ‘ โ†’ ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = { 0 } )
coeeq.5 โŠข ( ๐œ‘ โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
Assertion coeeq ( ๐œ‘ โ†’ ( coeff โ€˜ ๐น ) = ๐ด )

Proof

Step Hyp Ref Expression
1 coeeq.1 โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( Poly โ€˜ ๐‘† ) )
2 coeeq.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
3 coeeq.3 โŠข ( ๐œ‘ โ†’ ๐ด : โ„•0 โŸถ โ„‚ )
4 coeeq.4 โŠข ( ๐œ‘ โ†’ ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = { 0 } )
5 coeeq.5 โŠข ( ๐œ‘ โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
6 coeval โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ ( coeff โ€˜ ๐น ) = ( โ„ฉ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
7 1 6 syl โŠข ( ๐œ‘ โ†’ ( coeff โ€˜ ๐น ) = ( โ„ฉ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
8 fvoveq1 โŠข ( ๐‘› = ๐‘ โ†’ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) = ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) )
9 8 imaeq2d โŠข ( ๐‘› = ๐‘ โ†’ ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) )
10 9 eqeq1d โŠข ( ๐‘› = ๐‘ โ†’ ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = { 0 } ) )
11 oveq2 โŠข ( ๐‘› = ๐‘ โ†’ ( 0 ... ๐‘› ) = ( 0 ... ๐‘ ) )
12 11 sumeq1d โŠข ( ๐‘› = ๐‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
13 12 mpteq2dv โŠข ( ๐‘› = ๐‘ โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
14 13 eqeq2d โŠข ( ๐‘› = ๐‘ โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
15 10 14 anbi12d โŠข ( ๐‘› = ๐‘ โ†’ ( ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
16 15 rspcev โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘ + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘ ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
17 2 4 5 16 syl12anc โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
18 cnex โŠข โ„‚ โˆˆ V
19 nn0ex โŠข โ„•0 โˆˆ V
20 18 19 elmap โŠข ( ๐ด โˆˆ ( โ„‚ โ†‘m โ„•0 ) โ†” ๐ด : โ„•0 โŸถ โ„‚ )
21 3 20 sylibr โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ( โ„‚ โ†‘m โ„•0 ) )
22 coeeu โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
23 1 22 syl โŠข ( ๐œ‘ โ†’ โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
24 imaeq1 โŠข ( ๐‘Ž = ๐ด โ†’ ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) )
25 24 eqeq1d โŠข ( ๐‘Ž = ๐ด โ†’ ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } ) )
26 fveq1 โŠข ( ๐‘Ž = ๐ด โ†’ ( ๐‘Ž โ€˜ ๐‘˜ ) = ( ๐ด โ€˜ ๐‘˜ ) )
27 26 oveq1d โŠข ( ๐‘Ž = ๐ด โ†’ ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
28 27 sumeq2sdv โŠข ( ๐‘Ž = ๐ด โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
29 28 mpteq2dv โŠข ( ๐‘Ž = ๐ด โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
30 29 eqeq2d โŠข ( ๐‘Ž = ๐ด โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
31 25 30 anbi12d โŠข ( ๐‘Ž = ๐ด โ†’ ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
32 31 rexbidv โŠข ( ๐‘Ž = ๐ด โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
33 32 riota2 โŠข ( ( ๐ด โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( โ„ฉ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) = ๐ด ) )
34 21 23 33 syl2anc โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐ด โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐ด โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( โ„ฉ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) = ๐ด ) )
35 17 34 mpbid โŠข ( ๐œ‘ โ†’ ( โ„ฉ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) = ๐ด )
36 7 35 eqtrd โŠข ( ๐œ‘ โ†’ ( coeff โ€˜ ๐น ) = ๐ด )