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