Theorem pwslmod

Description: A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypothesis	pwslmod.y	|- Y = ( R ^s I )
Assertion	pwslmod	|- ( ( R e. LMod /\ I e. V ) -> Y e. LMod )

Proof

Step	Hyp	Ref	Expression
1		pwslmod.y	|- Y = ( R ^s I )
2		eqid	|- ( Scalar ` R ) = ( Scalar ` R )
3	1 2	pwsval	|- ( ( R e. LMod /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
4		eqid	|- ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
5	2	lmodring	|- ( R e. LMod -> ( Scalar ` R ) e. Ring )
6	5	adantr	|- ( ( R e. LMod /\ I e. V ) -> ( Scalar ` R ) e. Ring )
7		simpr	|- ( ( R e. LMod /\ I e. V ) -> I e. V )
8		fconst6g	|- ( R e. LMod -> ( I X. { R } ) : I --> LMod )
9	8	adantr	|- ( ( R e. LMod /\ I e. V ) -> ( I X. { R } ) : I --> LMod )
10		fvconst2g	|- ( ( R e. LMod /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
11	10	adantlr	|- ( ( ( R e. LMod /\ I e. V ) /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
12	11	fveq2d	|- ( ( ( R e. LMod /\ I e. V ) /\ x e. I ) -> ( Scalar ` ( ( I X. { R } ) ` x ) ) = ( Scalar ` R ) )
13	4 6 7 9 12	prdslmodd	|- ( ( R e. LMod /\ I e. V ) -> ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) e. LMod )
14	3 13	eqeltrd	|- ( ( R e. LMod /\ I e. V ) -> Y e. LMod )