Theorem rrxsuppss

Description: Support of Euclidean vectors. (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	rrxsuppss	|- ( ph -> ( F supp 0 ) C_ I )

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		suppssdm	|- ( F supp 0 ) C_ dom F
4	1 2	rrxf	|- ( ph -> F : I --> RR )
5	3 4	fssdm	|- ( ph -> ( F supp 0 ) C_ I )