Metamath Proof Explorer


Theorem mpllss

Description: The set of polynomials is closed under scalar multiplication, i.e. it is a linear subspace of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubg.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubg.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mplsubg.u 𝑈 = ( Base ‘ 𝑃 )
mplsubg.i ( 𝜑𝐼𝑊 )
mpllss.r ( 𝜑𝑅 ∈ Ring )
Assertion mpllss ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mplsubg.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubg.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mplsubg.u 𝑈 = ( Base ‘ 𝑃 )
4 mplsubg.i ( 𝜑𝐼𝑊 )
5 mpllss.r ( 𝜑𝑅 ∈ Ring )
6 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ( 0g𝑅 ) = ( 0g𝑅 )
8 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
9 0fin ∅ ∈ Fin
10 9 a1i ( 𝜑 → ∅ ∈ Fin )
11 unfi ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 𝑥𝑦 ) ∈ Fin )
12 11 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) ) → ( 𝑥𝑦 ) ∈ Fin )
13 ssfi ( ( 𝑥 ∈ Fin ∧ 𝑦𝑥 ) → 𝑦 ∈ Fin )
14 13 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ 𝑦𝑥 ) ) → 𝑦 ∈ Fin )
15 1 2 3 4 mplsubglem2 ( 𝜑𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g𝑅 ) ) ∈ Fin } )
16 1 6 7 8 4 10 12 14 15 5 mpllsslem ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑆 ) )