Theorem ply1bascl2

Description: A univariate polynomial is a multivariate polynomial on one index. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	ply1bascl.p	|- P = ( Poly1 ` R )
	ply1bascl.b	|- B = ( Base ` P )
Assertion	ply1bascl2	|- ( F e. B -> F e. ( Base ` ( 1o mPoly 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 2	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
5	4	eleq2i	|- ( F e. B <-> F e. ( Base ` ( 1o mPoly R ) ) )
6	5	biimpi	|- ( F e. B -> F e. ( Base ` ( 1o mPoly R ) ) )