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 ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
psr1rcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion psr1bascl ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 psr1rcl.p ⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2 psr1rcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 id ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
4 eqid ⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5 1 2 4 psr1bas2 ⊢ 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
6 3 5 eleqtrdi ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )