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

Metamath Proof Explorer

Theorem psr1bascl

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

Ref Expression
Hypotheses psr1rcl.p ⊢ P = PwSer 1 ⁡ R
psr1rcl.b ⊢ B = Base P
Assertion psr1bascl ⊢ F ∈ B → F ∈ Base 1 𝑜 mPwSer R

Proof

Step Hyp Ref Expression
1 psr1rcl.p ⊢ P = PwSer 1 ⁡ R
2 psr1rcl.b ⊢ B = Base P
3 id ⊢ F ∈ B → F ∈ B
4 eqid ⊢ 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
5 1 2 4 psr1bas2 ⊢ B = Base 1 𝑜 mPwSer R
6 3 5 eleqtrdi ⊢ F ∈ B → F ∈ Base 1 𝑜 mPwSer R