Metamath Proof Explorer


Theorem psrmulcl

Description: Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrmulcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmulcl.b 𝐵 = ( Base ‘ 𝑆 )
psrmulcl.t · = ( .r𝑆 )
psrmulcl.r ( 𝜑𝑅 ∈ Ring )
psrmulcl.x ( 𝜑𝑋𝐵 )
psrmulcl.y ( 𝜑𝑌𝐵 )
Assertion psrmulcl ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psrmulcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmulcl.b 𝐵 = ( Base ‘ 𝑆 )
3 psrmulcl.t · = ( .r𝑆 )
4 psrmulcl.r ( 𝜑𝑅 ∈ Ring )
5 psrmulcl.x ( 𝜑𝑋𝐵 )
6 psrmulcl.y ( 𝜑𝑌𝐵 )
7 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
8 1 2 3 4 5 6 7 psrmulcllem ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )