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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1bascl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	ply1bascl2	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1bascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1bascl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
4	1 3 2	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
5	4	eleq2i	⊢ ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
6	5	biimpi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )