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

Metamath Proof Explorer

Theorem frlmbasf

Description: Elements of the free module are functions. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses frlmval.f ⊢ F = R freeLMod I
frlmbasmap.n ⊢ N = Base R
frlmbasmap.b ⊢ B = Base F
Assertion frlmbasf ⊢ I ∈ W ∧ X ∈ B → X : I ⟶ N

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 frlmbasmap.n ⊢ N = Base R
3 frlmbasmap.b ⊢ B = Base F
4 1 2 3 frlmbasmap ⊢ I ∈ W ∧ X ∈ B → X ∈ N I
5 2 fvexi ⊢ N ∈ V
6 elmapg ⊢ N ∈ V ∧ I ∈ W → X ∈ N I ↔ X : I ⟶ N
7 5 6 mpan ⊢ I ∈ W → X ∈ N I ↔ X : I ⟶ N
8 7 adantr ⊢ I ∈ W ∧ X ∈ B → X ∈ N I ↔ X : I ⟶ N
9 4 8 mpbid ⊢ I ∈ W ∧ X ∈ B → X : I ⟶ N