Theorem rrxf

Description: Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019)

	Ref	Expression
Hypotheses	rrxmval.1	⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	rrxf.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
Assertion	rrxf	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		rrxf.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
3	1	ssrab3	⊢ 𝑋 ⊆ ( ℝ ↑m 𝐼 )
4	3 2	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
5		elmapi	⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
6	4 5	syl	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )