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	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmbasfn.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	frlmbasfn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	frlmbasfn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	frlmbasfn	⊢ ( 𝜑 → 𝑋 Fn 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		frlmbasfn.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmbasfn.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		frlmbasfn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		frlmbasfn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	1 5 2	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
7	3 4 6	syl2anc	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
8	7	ffnd	⊢ ( 𝜑 → 𝑋 Fn 𝐼 )