Metamath Proof Explorer

Theorem plybss

Description: Reverse closure of the parameter S of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Assertion	plybss	\|- ( F e. ( Poly ` S ) -> S C_ CC )

Proof

Step	Hyp	Ref	Expression
1		df-ply	\|- Poly = ( x e. ~P CC \|-> { f \| E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC \|-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
2	1	mptrcl	\|- ( F e. ( Poly ` S ) -> S e. ~P CC )
3	2	elpwid	\|- ( F e. ( Poly ` S ) -> S C_ CC )

Step

Hyp

Ref

Expression

df-ply

 |-  Poly = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )

mptrcl

 |-  ( F e. ( Poly ` S ) -> S e. ~P CC )

elpwid

 |-  ( F e. ( Poly ` S ) -> S C_ CC )