Metamath Proof Explorer

Theorem frlmpws

Description: The free module as a restriction of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses frlmval.f 
|- F = ( R freeLMod I )
frlmpws.b 
|- B = ( Base ` F )
Assertion frlmpws 
|- ( ( R e. V /\ I e. W ) -> F = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlmpws.b 
 |-  B = ( Base ` F )
3 eqid 
 |-  ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
4 3 dsmmval2 
 |-  ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) |`s ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
5 rlmsca 
 |-  ( R e. V -> R = ( Scalar ` ( ringLMod ` R ) ) )
6 5 adantr 
 |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
7 6 oveq1d 
 |-  ( ( R e. V /\ I e. W ) -> ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
8 1 frlmval 
 |-  ( ( R e. V /\ I e. W ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
9 8 eqcomd 
 |-  ( ( R e. V /\ I e. W ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = F )
10 9 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) = ( Base ` F ) )
11 10 2 eqtr4di 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) = B )
12 7 11 oveq12d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) |`s ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) ) = ( ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) |`s B ) )
13 4 12 syl5eq 
 |-  ( ( R e. V /\ I e. W ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) |`s B ) )
14 fvex 
 |-  ( ringLMod ` R ) e. _V
15 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
16 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
17 15 16 pwsval 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
18 14 17 mpan 
 |-  ( I e. W -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
19 18 adantl 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
20 19 oveq1d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ( ringLMod ` R ) ^s I ) |`s B ) = ( ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) |`s B ) )
21 13 8 20 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> F = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )