Theorem rrxfsupp

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

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

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		rrxf.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
3	2 1	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
4		breq1	⊢ ( ℎ = 𝐹 → ( ℎ finSupp 0 ↔ 𝐹 finSupp 0 ) )
5	4	elrab	⊢ ( 𝐹 ∈ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↔ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝐹 finSupp 0 ) )
6	3 5	sylib	⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝐹 finSupp 0 ) )
7	6	simprd	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8	7	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )