Theorem ply1bascl

Description: A univariate polynomial is a univariate power series. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	ply1bascl.p	|- P = ( Poly1 ` R )
	ply1bascl.b	|- B = ( Base ` P )
Assertion	ply1bascl	|- ( F e. B -> F e. ( Base ` ( PwSer1 ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1bascl.p	|- P = ( Poly1 ` R )
2		ply1bascl.b	|- B = ( Base ` P )
3		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
4	1 3	ply1val	|- P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
5		eqid	|- ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
6	4 5	ressbasss	|- ( Base ` P ) C_ ( Base ` ( PwSer1 ` R ) )
7	2 6	eqsstri	|- B C_ ( Base ` ( PwSer1 ` R ) )
8	7	sseli	|- ( F e. B -> F e. ( Base ` ( PwSer1 ` R ) ) )