Metamath Proof Explorer

Theorem suppmptcfin

Description: The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019)

Ref Expression
Hypotheses suppmptcfin.b 
|- B = ( Base ` M )
suppmptcfin.r 
|- R = ( Scalar ` M )
suppmptcfin.0 
|- .0. = ( 0g ` R )
suppmptcfin.1 
|- .1. = ( 1r ` R )
suppmptcfin.f 
|- F = ( x e. V |-> if ( x = X , .1. , .0. ) )
Assertion suppmptcfin 
|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F supp .0. ) e. Fin )

Proof

Step Hyp Ref Expression
1 suppmptcfin.b 
 |-  B = ( Base ` M )
2 suppmptcfin.r 
 |-  R = ( Scalar ` M )
3 suppmptcfin.0 
 |-  .0. = ( 0g ` R )
4 suppmptcfin.1 
 |-  .1. = ( 1r ` R )
5 suppmptcfin.f 
 |-  F = ( x e. V |-> if ( x = X , .1. , .0. ) )
6 eqeq1 
 |-  ( x = v -> ( x = X <-> v = X ) )
7 6 ifbid 
 |-  ( x = v -> if ( x = X , .1. , .0. ) = if ( v = X , .1. , .0. ) )
8 7 cbvmptv 
 |-  ( x e. V |-> if ( x = X , .1. , .0. ) ) = ( v e. V |-> if ( v = X , .1. , .0. ) )
9 5 8 eqtri 
 |-  F = ( v e. V |-> if ( v = X , .1. , .0. ) )
10 simp2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> V e. ~P B )
11 3 fvexi 
 |-  .0. e. _V
12 11 a1i 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> .0. e. _V )
13 4 fvexi 
 |-  .1. e. _V
14 13 a1i 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> .1. e. _V )
15 11 a1i 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> .0. e. _V )
16 14 15 ifcld 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> if ( v = X , .1. , .0. ) e. _V )
17 9 10 12 16 mptsuppd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F supp .0. ) = { v e. V | if ( v = X , .1. , .0. ) =/= .0. } )
18 snfi 
 |-  { X } e. Fin
19 2a1 
 |-  ( v = X -> ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) ) )
20 iffalse 
 |-  ( -. v = X -> if ( v = X , .1. , .0. ) = .0. )
21 20 adantr 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> if ( v = X , .1. , .0. ) = .0. )
22 21 neeq1d 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( if ( v = X , .1. , .0. ) =/= .0. <-> .0. =/= .0. ) )
23 eqid 
 |-  .0. = .0.
24 eqneqall 
 |-  ( .0. = .0. -> ( .0. =/= .0. -> v = X ) )
25 23 24 ax-mp 
 |-  ( .0. =/= .0. -> v = X )
26 22 25 syl6bi 
 |-  ( ( -. v = X /\ ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) ) -> ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) )
27 26 ex 
 |-  ( -. v = X -> ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) ) )
28 19 27 pm2.61i 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ v e. V ) -> ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) )
29 28 ralrimiva 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> A. v e. V ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) )
30 rabsssn 
 |-  ( { v e. V | if ( v = X , .1. , .0. ) =/= .0. } C_ { X } <-> A. v e. V ( if ( v = X , .1. , .0. ) =/= .0. -> v = X ) )
31 29 30 sylibr 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> { v e. V | if ( v = X , .1. , .0. ) =/= .0. } C_ { X } )
32 ssfi 
 |-  ( ( { X } e. Fin /\ { v e. V | if ( v = X , .1. , .0. ) =/= .0. } C_ { X } ) -> { v e. V | if ( v = X , .1. , .0. ) =/= .0. } e. Fin )
33 18 31 32 sylancr 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> { v e. V | if ( v = X , .1. , .0. ) =/= .0. } e. Fin )
34 17 33 eqeltrd 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F supp .0. ) e. Fin )