Metamath Proof Explorer


Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 plybss โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ ๐‘† โŠ† โ„‚ )
2 plyval โŠข ( ๐‘† โŠ† โ„‚ โ†’ ( Poly โ€˜ ๐‘† ) = { ๐‘“ โˆฃ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐‘“ = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) } )
3 2 eleq2d โŠข ( ๐‘† โŠ† โ„‚ โ†’ ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ๐น โˆˆ { ๐‘“ โˆฃ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐‘“ = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) } ) )
4 id โŠข ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
5 cnex โŠข โ„‚ โˆˆ V
6 5 mptex โŠข ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โˆˆ V
7 4 6 eqeltrdi โŠข ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ๐น โˆˆ V )
8 7 a1i โŠข ( ( ๐‘› โˆˆ โ„•0 โˆง ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ) โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ๐น โˆˆ V ) )
9 8 rexlimivv โŠข ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†’ ๐น โˆˆ V )
10 eqeq1 โŠข ( ๐‘“ = ๐น โ†’ ( ๐‘“ = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
11 10 2rexbidv โŠข ( ๐‘“ = ๐น โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐‘“ = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
12 9 11 elab3 โŠข ( ๐น โˆˆ { ๐‘“ โˆฃ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐‘“ = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) } โ†” โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
13 3 12 bitrdi โŠข ( ๐‘† โŠ† โ„‚ โ†’ ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
14 1 13 biadanii โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†” ( ๐‘† โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( ๐‘† โˆช { 0 } ) โ†‘m โ„•0 ) ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )