Theorem sniffsupp

Description: A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	sniffsupp.i	|- ( ph -> I e. V )
	sniffsupp.0	|- ( ph -> .0. e. W )
	sniffsupp.f	|- F = ( x e. I |-> if ( x = X , A , .0. ) )
Assertion	sniffsupp	|- ( ph -> F finSupp .0. )

Proof

Step	Hyp	Ref	Expression
1		sniffsupp.i	|- ( ph -> I e. V )
2		sniffsupp.0	|- ( ph -> .0. e. W )
3		sniffsupp.f	|- F = ( x e. I |-> if ( x = X , A , .0. ) )
4		snfi	|- { X } e. Fin
5		eldifsni	|- ( x e. ( I \ { X } ) -> x =/= X )
6	5	adantl	|- ( ( ph /\ x e. ( I \ { X } ) ) -> x =/= X )
7	6	neneqd	|- ( ( ph /\ x e. ( I \ { X } ) ) -> -. x = X )
8	7	iffalsed	|- ( ( ph /\ x e. ( I \ { X } ) ) -> if ( x = X , A , .0. ) = .0. )
9	8 1	suppss2	|- ( ph -> ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) C_ { X } )
10		ssfi	|- ( ( { X } e. Fin /\ ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) C_ { X } ) -> ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) e. Fin )
11	4 9 10	sylancr	|- ( ph -> ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) e. Fin )
12		funmpt	|- Fun ( x e. I |-> if ( x = X , A , .0. ) )
13	1	mptexd	|- ( ph -> ( x e. I |-> if ( x = X , A , .0. ) ) e. _V )
14		funisfsupp	|- ( ( Fun ( x e. I |-> if ( x = X , A , .0. ) ) /\ ( x e. I |-> if ( x = X , A , .0. ) ) e. _V /\ .0. e. W ) -> ( ( x e. I |-> if ( x = X , A , .0. ) ) finSupp .0. <-> ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) e. Fin ) )
15	12 13 2 14	mp3an2i	|- ( ph -> ( ( x e. I |-> if ( x = X , A , .0. ) ) finSupp .0. <-> ( ( x e. I |-> if ( x = X , A , .0. ) ) supp .0. ) e. Fin ) )
16	11 15	mpbird	|- ( ph -> ( x e. I |-> if ( x = X , A , .0. ) ) finSupp .0. )
17	3 16	eqbrtrid	|- ( ph -> F finSupp .0. )