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	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ‘ 𝑆 ) )