Theorem ply1bascl

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

	Ref	Expression
Hypotheses	ply1bascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1bascl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1bascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1bascl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
4	1 3	ply1val	⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
5		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
6	4 5	ressbasss	⊢ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
7	2 6	eqsstri	⊢ 𝐵 ⊆ ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
8	7	sseli	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )