Theorem rrxfsupp

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

	Ref	Expression
Hypotheses	rrxmval.1	|- X = { h e. ( RR ^m I ) | h finSupp 0 }
	rrxf.1	|- ( ph -> F e. X )
Assertion	rrxfsupp	|- ( ph -> ( F supp 0 ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	|- X = { h e. ( RR ^m I ) | h finSupp 0 }
2		rrxf.1	|- ( ph -> F e. X )
3	2 1	eleqtrdi	|- ( ph -> F e. { h e. ( RR ^m I ) | h finSupp 0 } )
4		breq1	|- ( h = F -> ( h finSupp 0 <-> F finSupp 0 ) )
5	4	elrab	|- ( F e. { h e. ( RR ^m I ) | h finSupp 0 } <-> ( F e. ( RR ^m I ) /\ F finSupp 0 ) )
6	3 5	sylib	|- ( ph -> ( F e. ( RR ^m I ) /\ F finSupp 0 ) )
7	6	simprd	|- ( ph -> F finSupp 0 )
8	7	fsuppimpd	|- ( ph -> ( F supp 0 ) e. Fin )