Theorem frlmbasf

Description: Elements of the free module are functions. (They map an index to the coordinate at that index). (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmbasmap.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
	frlmbasmap.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmbasmap.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
3		frlmbasmap.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4	1 2 3	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) )
5	2	fvexi	⊢ 𝑁 ∈ V
6		elmapg	⊢ ( ( 𝑁 ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )
7	5 6	mpan	⊢ ( 𝐼 ∈ 𝑊 → ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )
8	7	adantr	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( 𝑁 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝑁 ) )
9	4 8	mpbid	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ 𝑁 )