Theorem frlmfielbas

Description: The vectors of a finite free module are the functions from I to N . (Contributed by SN, 31-Aug-2023)

	Ref	Expression
Hypotheses	frlmfielbas.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmfielbas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
	frlmfielbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	frlmfielbas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmfielbas.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmfielbas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
3		frlmfielbas.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4	3	eleq2i	⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐹 ) )
5	1 2	frlmfibas	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ 𝐹 ) )
6	5	eleq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ↔ 𝑋 ∈ ( Base ‘ 𝐹 ) ) )
7	2	fvexi	⊢ 𝑁 ∈ V
8	7	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝑁 ∈ V )
9		simpr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → 𝐼 ∈ Fin )
10	8 9	elmapd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )
11	6 10	bitr3d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ ( Base ‘ 𝐹 ) ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )
12	4 11	bitrid	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )