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 )