This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrxsuppss

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

Ref Expression
Hypotheses rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
rrxf.1 ⊢ φ → F ∈ X
Assertion rrxsuppss ⊢ φ → F supp 0 ⊆ I

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
2 rrxf.1 ⊢ φ → F ∈ X
3 suppssdm ⊢ F supp 0 ⊆ dom ⁡ F
4 1 2 rrxf ⊢ φ → F : I ⟶ ℝ
5 3 4 fssdm ⊢ φ → F supp 0 ⊆ I