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 bitrid ⊢ R ∈ V ∧ I ∈ Fin → X ∈ B ↔ X : I ⟶ N