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