Theorem rrxsuppss

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

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

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		rrxf.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
3		suppssdm	⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
4	1 2	rrxf	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )
5	3 4	fssdm	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐼 )