Theorem mpllvec

Description: The polynomial ring is a vector space. (Contributed by SN, 29-Feb-2024)

	Ref	Expression
Hypothesis	mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion	mpllvec	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝑃 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3	1	mpllmod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
4	2 3	sylan2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝑃 ∈ LMod )
5		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝐼 ∈ 𝑉 )
6		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝑅 ∈ DivRing )
7	1 5 6	mplsca	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
8	7 6	eqeltrrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → ( Scalar ‘ 𝑃 ) ∈ DivRing )
9		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
10	9	islvec	⊢ ( 𝑃 ∈ LVec ↔ ( 𝑃 ∈ LMod ∧ ( Scalar ‘ 𝑃 ) ∈ DivRing ) )
11	4 8 10	sylanbrc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ DivRing ) → 𝑃 ∈ LVec )