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

Metamath Proof Explorer

Theorem ply1lmod

Description: Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypothesis ply1lmod.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion ply1lmod ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )

Proof

Step Hyp Ref Expression
1 ply1lmod.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 eqid ⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
3 2 psr1lmod ⊢ ( 𝑅 ∈ Ring → ( PwSer1 ‘ 𝑅 ) ∈ LMod )
4 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
6 4 5 ply1bas ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
7 4 2 5 ply1lss ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) )
8 6 7 eqeltrrid ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) )
9 1 2 ply1val ⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
10 eqid ⊢ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) = ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) )
11 9 10 lsslmod ⊢ ( ( ( PwSer1 ‘ 𝑅 ) ∈ LMod ∧ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) ) → 𝑃 ∈ LMod )
12 3 8 11 syl2anc ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )