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 ) )