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 
|- F = ( R freeLMod I )
frlmfielbas.n 
|- N = ( Base ` R )
frlmfielbas.b 
|- B = ( Base ` F )
Assertion frlmfielbas 
|- ( ( R e. V /\ I e. Fin ) -> ( X e. 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 e. B <-> X e. ( Base ` F ) )
5 1 2 frlmfibas 
 |-  ( ( R e. V /\ I e. Fin ) -> ( N ^m I ) = ( Base ` F ) )
6 5 eleq2d 
 |-  ( ( R e. V /\ I e. Fin ) -> ( X e. ( N ^m I ) <-> X e. ( Base ` F ) ) )
7 2 fvexi 
 |-  N e. _V
8 7 a1i 
 |-  ( ( R e. V /\ I e. Fin ) -> N e. _V )
9 simpr 
 |-  ( ( R e. V /\ I e. Fin ) -> I e. Fin )
10 8 9 elmapd 
 |-  ( ( R e. V /\ I e. Fin ) -> ( X e. ( N ^m I ) <-> X : I --> N ) )
11 6 10 bitr3d 
 |-  ( ( R e. V /\ I e. Fin ) -> ( X e. ( Base ` F ) <-> X : I --> N ) )
12 4 11 bitrid 
 |-  ( ( R e. V /\ I e. Fin ) -> ( X e. B <-> X : I --> N ) )