This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )