This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion frlmpwsfi ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝐹 = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 fvex ⊢ ( ringLMod ‘ 𝑅 ) ∈ V
3 fnconstg ⊢ ( ( ringLMod ‘ 𝑅 ) ∈ V → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 )
4 2 3 ax-mp ⊢ ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼
5 dsmmfi ⊢ ( ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
6 4 5 mpan ⊢ ( 𝐼 ∈ Fin → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
7 6 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
8 rlmsca ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
9 8 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
10 9 oveq1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑅 Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
11 7 10 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
12 1 frlmval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
13 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
14 eqid ⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
15 13 14 pwsval ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ Fin ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
16 2 15 mpan ⊢ ( 𝐼 ∈ Fin → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
17 16 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) Xs ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
18 11 12 17 3eqtr4d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝐹 = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )