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 𝐹 = ( 𝑅 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 syl5bb ( ( 𝑅𝑉𝐼 ∈ Fin ) → ( 𝑋𝐵𝑋 : 𝐼𝑁 ) )