# 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}\mathrm{freeLMod}{I}$
frlmbasmap.n ${⊢}{N}={\mathrm{Base}}_{{R}}$
frlmbasmap.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
Assertion frlmbasf ${⊢}\left({I}\in {W}\wedge {X}\in {B}\right)\to {X}:{I}⟶{N}$

### Proof

Step Hyp Ref Expression
1 frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 frlmbasmap.n ${⊢}{N}={\mathrm{Base}}_{{R}}$
3 frlmbasmap.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 1 2 3 frlmbasmap ${⊢}\left({I}\in {W}\wedge {X}\in {B}\right)\to {X}\in \left({{N}}^{{I}}\right)$
5 2 fvexi ${⊢}{N}\in \mathrm{V}$
6 elmapg ${⊢}\left({N}\in \mathrm{V}\wedge {I}\in {W}\right)\to \left({X}\in \left({{N}}^{{I}}\right)↔{X}:{I}⟶{N}\right)$
7 5 6 mpan ${⊢}{I}\in {W}\to \left({X}\in \left({{N}}^{{I}}\right)↔{X}:{I}⟶{N}\right)$
8 7 adantr ${⊢}\left({I}\in {W}\wedge {X}\in {B}\right)\to \left({X}\in \left({{N}}^{{I}}\right)↔{X}:{I}⟶{N}\right)$
9 4 8 mpbid ${⊢}\left({I}\in {W}\wedge {X}\in {B}\right)\to {X}:{I}⟶{N}$