Metamath Proof Explorer


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 )