Theorem frlmfibas

Description: The base set of the finite free module as a set exponential. (Contributed by AV, 6-Dec-2018)

	Ref	Expression
Hypotheses	frlmfibas.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmfibas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
Assertion	frlmfibas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmfibas.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmfibas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
3		elmapi	⊢ ( 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝑁 )
4	3	adantl	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝑁 )
5		simpl	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝐼 ∈ Fin )
6		fvexd	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
7	4 5 6	fdmfifsupp	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝑎 finSupp ( 0g ‘ 𝑅 ) )
8	7	ralrimiva	⊢ ( 𝐼 ∈ Fin → ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
9	8	adantl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
10		rabid2	⊢ ( ( 𝑁 ↑m 𝐼 ) = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } ↔ ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
11	9 10	sylibr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } )
12		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13		eqid	⊢ { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) }
14	1 2 12 13	frlmbas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝐹 ) )
15	11 14	eqtrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ 𝐹 ) )