This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Poly 1 ⁡ R
ply1bascl.b ⊢ B = Base P
Assertion ply1bascl ⊢ F ∈ B → F ∈ Base PwSer 1 ⁡ R

Proof

Step Hyp Ref Expression
1 ply1bascl.p ⊢ P = Poly 1 ⁡ R
2 ply1bascl.b ⊢ B = Base P
3 eqid ⊢ PwSer 1 ⁡ R = PwSer 1 ⁡ R
4 1 3 ply1val ⊢ P = PwSer 1 ⁡ R ↾ 𝑠 Base 1 𝑜 mPoly R
5 eqid ⊢ Base PwSer 1 ⁡ R = Base PwSer 1 ⁡ R
6 4 5 ressbasss ⊢ Base P ⊆ Base PwSer 1 ⁡ R
7 2 6 eqsstri ⊢ B ⊆ Base PwSer 1 ⁡ R
8 7 sseli ⊢ F ∈ B → F ∈ Base PwSer 1 ⁡ R