Theorem frlmbasfn

Description: Elements of the free module are functions. (They map an index to the coordinate at that index, see frlmbasf ). (Contributed by SN, 23-Sep-2026)

	Ref	Expression
Hypotheses	frlmbasfn.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmbasfn.b	$$⊢B={\mathrm{Base}}_F$$
	frlmbasfn.i	$$⊢\phi \to I\in W$$
	frlmbasfn.x	$$⊢\phi \to X\in B$$
Assertion	frlmbasfn	$$⊢\phi \to XFnI$$

Proof

Step	Hyp	Ref	Expression
1		frlmbasfn.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmbasfn.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmbasfn.i	$$⊢\phi \to I\in W$$
4		frlmbasfn.x	$$⊢\phi \to X\in B$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	1 5 2	frlmbasf	$$⊢\left(I\in W\wedge X\in B\right)\to X:I⟶{\mathrm{Base}}_R$$
7	3 4 6	syl2anc	$$⊢\phi \to X:I⟶{\mathrm{Base}}_R$$
8	7	ffnd	$$⊢\phi \to XFnI$$