Metamath Proof Explorer

Theorem frlmpwsfi

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

Ref Expression
Hypothesis frlmval.f 
|- F = ( R freeLMod I )
Assertion frlmpwsfi 
|- ( ( R e. V /\ I e. Fin ) -> F = ( ( ringLMod ` R ) ^s I ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 fvex 
 |-  ( ringLMod ` R ) e. _V
3 fnconstg 
 |-  ( ( ringLMod ` R ) e. _V -> ( I X. { ( ringLMod ` R ) } ) Fn I )
4 2 3 ax-mp 
 |-  ( I X. { ( ringLMod ` R ) } ) Fn I
5 dsmmfi 
 |-  ( ( ( I X. { ( ringLMod ` R ) } ) Fn I /\ I e. Fin ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
6 4 5 mpan 
 |-  ( I e. Fin -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
7 6 adantl 
 |-  ( ( R e. V /\ I e. Fin ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
8 rlmsca 
 |-  ( R e. V -> R = ( Scalar ` ( ringLMod ` R ) ) )
9 8 adantr 
 |-  ( ( R e. V /\ I e. Fin ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
10 9 oveq1d 
 |-  ( ( R e. V /\ I e. Fin ) -> ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
11 7 10 eqtrd 
 |-  ( ( R e. V /\ I e. Fin ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
12 1 frlmval 
 |-  ( ( R e. V /\ I e. Fin ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
13 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
14 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
15 13 14 pwsval 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. Fin ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
16 2 15 mpan 
 |-  ( I e. Fin -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
17 16 adantl 
 |-  ( ( R e. V /\ I e. Fin ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
18 11 12 17 3eqtr4d 
 |-  ( ( R e. V /\ I e. Fin ) -> F = ( ( ringLMod ` R ) ^s I ) )