Metamath Proof Explorer


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 F = R freeLMod I
frlmfielbas.n N = Base R
frlmfielbas.b B = Base F
Assertion frlmfielbas R V I Fin X B X : I N

Proof

Step Hyp Ref Expression
1 frlmfielbas.f F = R freeLMod I
2 frlmfielbas.n N = Base R
3 frlmfielbas.b B = Base F
4 3 eleq2i X B X Base F
5 1 2 frlmfibas R V I Fin N I = Base F
6 5 eleq2d R V I Fin X N I X Base F
7 2 fvexi N V
8 7 a1i R V I Fin N V
9 simpr R V I Fin I Fin
10 8 9 elmapd R V I Fin X N I X : I N
11 6 10 bitr3d R V I Fin X Base F X : I N
12 4 11 syl5bb R V I Fin X B X : I N