Metamath Proof Explorer

Theorem elply2

Description: The coefficient function can be assumed to have zeroes outside 0 ... n . (Contributed by Mario Carneiro, 20-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion elply2 ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elply โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
2 simpr โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) )
3 simpll โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ๐‘† โŠ† โ„‚ )
4 cnex โŠข โ„‚ โˆˆ V
5 ssexg โŠข ( ( ๐‘† โŠ† โ„‚ โˆง โ„‚ โˆˆ V ) โ†’ ๐‘† โˆˆ V )
6 3 4 5 sylancl โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ๐‘† โˆˆ V )
7 snex โŠข { 0 } โˆˆ V
8 unexg โŠข ( ( ๐‘† โˆˆ V โˆง { 0 } โˆˆ V ) โ†’ ( ๐‘† โˆช { 0 } ) โˆˆ V )
9 6 7 8 sylancl โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘† โˆช { 0 } ) โˆˆ V )
10 nn0ex โŠข โ„•0 โˆˆ V
11 elmapg โŠข ( ( ( ๐‘† โˆช { 0 } ) โˆˆ V โˆง โ„•0 โˆˆ V ) โ†’ ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โ†” ๐‘“ : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) ) )
12 9 10 11 sylancl โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โ†” ๐‘“ : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) ) )
13 2 12 mpbid โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ๐‘“ : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) )
14 13 ffvelcdmda โŠข ( ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘“ โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘† โˆช { 0 } ) )
15 ssun2 โŠข { 0 } โŠ† ( ๐‘† โˆช { 0 } )
16 c0ex โŠข 0 โˆˆ V
17 16 snss โŠข ( 0 โˆˆ ( ๐‘† โˆช { 0 } ) โ†” { 0 } โŠ† ( ๐‘† โˆช { 0 } ) )
18 15 17 mpbir โŠข 0 โˆˆ ( ๐‘† โˆช { 0 } )
19 ifcl โŠข ( ( ( ๐‘“ โ€˜ ๐‘ฅ ) โˆˆ ( ๐‘† โˆช { 0 } ) โˆง 0 โˆˆ ( ๐‘† โˆช { 0 } ) ) โ†’ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) โˆˆ ( ๐‘† โˆช { 0 } ) )
20 14 18 19 sylancl โŠข ( ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) โˆˆ ( ๐‘† โˆช { 0 } ) )
21 20 fmpttd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) )
22 elmapg โŠข ( ( ( ๐‘† โˆช { 0 } ) โˆˆ V โˆง โ„•0 โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โ†” ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) ) )
23 9 10 22 sylancl โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โ†” ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) : โ„•0 โŸถ ( ๐‘† โˆช { 0 } ) ) )
24 21 23 mpbird โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) )
25 eleq1w โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) โ†” ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ) )
26 fveq2 โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ๐‘“ โ€˜ ๐‘ฅ ) = ( ๐‘“ โ€˜ ๐‘˜ ) )
27 25 26 ifbieq1d โŠข ( ๐‘ฅ = ๐‘˜ โ†’ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) = if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) )
28 eqid โŠข ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) )
29 fvex โŠข ( ๐‘“ โ€˜ ๐‘˜ ) โˆˆ V
30 29 16 ifex โŠข if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) โˆˆ V
31 27 28 30 fvmpt โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) )
32 31 ad2antll โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โˆง ๐‘˜ โˆˆ โ„•0 ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) )
33 iffalse โŠข ( ยฌ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) = 0 )
34 33 eqeq2d โŠข ( ยฌ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) โ†” ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = 0 ) )
35 32 34 syl5ibcom โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โˆง ๐‘˜ โˆˆ โ„•0 ) ) โ†’ ( ยฌ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = 0 ) )
36 35 necon1ad โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โˆง ๐‘˜ โˆˆ โ„•0 ) ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ) )
37 elfzle2 โŠข ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ๐‘˜ โ‰ค ๐‘› )
38 36 37 syl6 โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ( ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โˆง ๐‘˜ โˆˆ โ„•0 ) ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โ‰ค ๐‘› ) )
39 38 anassrs โŠข ( ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โ‰ค ๐‘› ) )
40 39 ralrimiva โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ โˆ€ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โ‰ค ๐‘› ) )
41 simplr โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ๐‘› โˆˆ โ„•0 )
42 0cnd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ 0 โˆˆ โ„‚ )
43 42 snssd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ { 0 } โŠ† โ„‚ )
44 3 43 unssd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘† โˆช { 0 } ) โŠ† โ„‚ )
45 21 44 fssd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) : โ„•0 โŸถ โ„‚ )
46 plyco0 โŠข ( ( ๐‘› โˆˆ โ„•0 โˆง ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) : โ„•0 โŸถ โ„‚ ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” โˆ€ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โ‰ค ๐‘› ) ) )
47 41 45 46 syl2anc โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” โˆ€ ๐‘˜ โˆˆ โ„•0 ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โ‰ค ๐‘› ) ) )
48 40 47 mpbird โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } )
49 eqidd โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
50 imaeq1 โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) )
51 50 eqeq1d โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } ) )
52 fveq1 โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ๐‘Ž โ€˜ ๐‘˜ ) = ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) )
53 elfznn0 โŠข ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ๐‘˜ โˆˆ โ„•0 )
54 53 31 syl โŠข ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) )
55 iftrue โŠข ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ if ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘˜ ) , 0 ) = ( ๐‘“ โ€˜ ๐‘˜ ) )
56 54 55 eqtrd โŠข ( ๐‘˜ โˆˆ ( 0 ... ๐‘› ) โ†’ ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€˜ ๐‘˜ ) = ( ๐‘“ โ€˜ ๐‘˜ ) )
57 52 56 sylan9eq โŠข ( ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ) โ†’ ( ๐‘Ž โ€˜ ๐‘˜ ) = ( ๐‘“ โ€˜ ๐‘˜ ) )
58 57 oveq1d โŠข ( ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ) โ†’ ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
59 58 sumeq2dv โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
60 59 mpteq2dv โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
61 60 eqeq2d โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
62 51 61 anbi12d โŠข ( ๐‘Ž = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ†’ ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
63 62 rspcev โŠข ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) โˆง ( ( ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐‘ฅ โˆˆ ( 0 ... ๐‘› ) , ( ๐‘“ โ€˜ ๐‘ฅ ) , 0 ) ) โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
64 24 48 49 63 syl12anc โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
65 eqeq1 โŠข ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
66 65 anbi2d โŠข ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
67 66 rexbidv โŠข ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ( โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
68 64 67 syl5ibrcom โŠข ( ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โˆง ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
69 68 rexlimdva โŠข ( ( ๐‘† โŠ† โ„‚ โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( โˆƒ ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
70 69 reximdva โŠข ( ๐‘† โŠ† โ„‚ โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
71 70 imdistani โŠข ( ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘“ โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†’ ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
72 1 71 sylbi โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
73 simpr โŠข ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
74 73 reximi โŠข ( โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
75 74 reximi โŠข ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
76 75 anim2i โŠข ( ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
77 elply โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
78 76 77 sylibr โŠข ( ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐น โˆˆ ( Poly โ€˜ ๐‘† ) )
79 72 78 impbii โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )