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\mathrm{freeLMod}I$$
	frlmfielbas.n	$$⊢N={\mathrm{Base}}_R$$
	frlmfielbas.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	frlmfielbas	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to \left(X\in B\leftrightarrow X:I⟶N\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmfielbas.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmfielbas.n	$$⊢N={\mathrm{Base}}_R$$
3		frlmfielbas.b	$$⊢B={\mathrm{Base}}_F$$
4	3	eleq2i	$$⊢X\in B\leftrightarrow X\in {\mathrm{Base}}_F$$
5	1 2	frlmfibas	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to N^I={\mathrm{Base}}_F$$
6	5	eleq2d	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to \left(X\in \left(N^I\right)\leftrightarrow X\in {\mathrm{Base}}_F\right)$$
7	2	fvexi	$$⊢N\in \mathrm{V}$$
8	7	a1i	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to N\in \mathrm{V}$$
9		simpr	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to I\in \mathrm{Fin}$$
10	8 9	elmapd	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to \left(X\in \left(N^I\right)\leftrightarrow X:I⟶N\right)$$
11	6 10	bitr3d	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to \left(X\in {\mathrm{Base}}_F\leftrightarrow X:I⟶N\right)$$
12	4 11	bitrid	$$⊢\left(R\in V\wedge I\in \mathrm{Fin}\right)\to \left(X\in B\leftrightarrow X:I⟶N\right)$$