This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )