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 ) )