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

Metamath Proof Explorer

Theorem rrxfsupp

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

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

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
2 rrxf.1 ⊢ φ → F ∈ X
3 2 1 eleqtrdi ⊢ φ → F ∈ h ∈ ℝ I | finSupp 0 ⁡ h
4 breq1 ⊢ h = F → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ F
5 4 elrab ⊢ F ∈ h ∈ ℝ I | finSupp 0 ⁡ h ↔ F ∈ ℝ I ∧ finSupp 0 ⁡ F
6 3 5 sylib ⊢ φ → F ∈ ℝ I ∧ finSupp 0 ⁡ F
7 6 simprd ⊢ φ → finSupp 0 ⁡ F
8 7 fsuppimpd ⊢ φ → F supp 0 ∈ Fin