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

Metamath Proof Explorer

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. )