Theorem mptcfsupp

Description: A mapping with value 0 except of one is finitely supported. (Contributed by AV, 9-Jun-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	mptcfsupp	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F finSupp .0. )

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	5	funmpt2	|- Fun F
7	6	a1i	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> Fun F )
8	1 2 3 4 5	suppmptcfin	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F supp .0. ) e. Fin )
9		mptexg	|- ( V e. ~P B -> ( x e. V |-> if ( x = X , .1. , .0. ) ) e. _V )
10	5 9	eqeltrid	|- ( V e. ~P B -> F e. _V )
11	10	3ad2ant2	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F e. _V )
12	3	fvexi	|- .0. e. _V
13		isfsupp	|- ( ( F e. _V /\ .0. e. _V ) -> ( F finSupp .0. <-> ( Fun F /\ ( F supp .0. ) e. Fin ) ) )
14	11 12 13	sylancl	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F finSupp .0. <-> ( Fun F /\ ( F supp .0. ) e. Fin ) ) )
15	7 8 14	mpbir2and	|- ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> F finSupp .0. )