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 freeLMod I )
	frlmbasfn.b	|- B = ( Base ` F )
	frlmbasfn.i	|- ( ph -> I e. W )
	frlmbasfn.x	|- ( ph -> X e. B )
Assertion	frlmbasfn	|- ( ph -> X Fn I )

Proof

Step	Hyp	Ref	Expression
1		frlmbasfn.f	|- F = ( R freeLMod I )
2		frlmbasfn.b	|- B = ( Base ` F )
3		frlmbasfn.i	|- ( ph -> I e. W )
4		frlmbasfn.x	|- ( ph -> X e. B )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	1 5 2	frlmbasf	|- ( ( I e. W /\ X e. B ) -> X : I --> ( Base ` R ) )
7	3 4 6	syl2anc	|- ( ph -> X : I --> ( Base ` R ) )
8	7	ffnd	|- ( ph -> X Fn I )