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 V I Fin F = ringLMod R 𝑠 I

Proof

Step Hyp Ref Expression
1 frlmval.f F = R freeLMod I
2 fvex ringLMod R V
3 fnconstg ringLMod R V I × ringLMod R Fn I
4 2 3 ax-mp I × ringLMod R Fn I
5 dsmmfi I × ringLMod R Fn I I Fin R m I × ringLMod R = R 𝑠 I × ringLMod R
6 4 5 mpan I Fin R m I × ringLMod R = R 𝑠 I × ringLMod R
7 6 adantl R V I Fin R m I × ringLMod R = R 𝑠 I × ringLMod R
8 rlmsca R V R = Scalar ringLMod R
9 8 adantr R V I Fin R = Scalar ringLMod R
10 9 oveq1d R V I Fin R 𝑠 I × ringLMod R = Scalar ringLMod R 𝑠 I × ringLMod R
11 7 10 eqtrd R V I Fin R m I × ringLMod R = Scalar ringLMod R 𝑠 I × ringLMod R
12 1 frlmval R V I Fin F = R m I × ringLMod R
13 eqid ringLMod R 𝑠 I = ringLMod R 𝑠 I
14 eqid Scalar ringLMod R = Scalar ringLMod R
15 13 14 pwsval ringLMod R V I Fin ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I × ringLMod R
16 2 15 mpan I Fin ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I × ringLMod R
17 16 adantl R V I Fin ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I × ringLMod R
18 11 12 17 3eqtr4d R V I Fin F = ringLMod R 𝑠 I