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	1 2	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
4	3	eleq2i	⊢ ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
5	4	biimpi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )