Theorem psr1lmod

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

	Ref	Expression
Hypothesis	psr1lmod.p	|- P = ( PwSer1 ` R )
Assertion	psr1lmod	|- ( R e. Ring -> P e. LMod )

Proof

Step	Hyp	Ref	Expression
1		psr1lmod.p	|- P = ( PwSer1 ` R )
2	1	psr1val	|- P = ( ( 1o ordPwSer R ) ` (/) )
3		1on	|- 1o e. On
4	3	a1i	|- ( R e. Ring -> 1o e. On )
5		id	|- ( R e. Ring -> R e. Ring )
6		0ss	|- (/) C_ ( 1o X. 1o )
7	6	a1i	|- ( R e. Ring -> (/) C_ ( 1o X. 1o ) )
8	2 4 5 7	opsrlmod	|- ( R e. Ring -> P e. LMod )