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	$⊢ \underset{˙}{0} = 0_{R}$
	suppmptcfin.1	$⊢ \underset{˙}{1} = 1_{R}$
	suppmptcfin.f	$⊢ F = (x \in V ⟼ if (x = X, \underset{˙}{1}, \underset{˙}{0}))$
Assertion	mptcfsupp	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to {finSupp}_{\underset{˙}{0}} (F)$

Step	Hyp	Ref	Expression
1		suppmptcfin.b	$⊢ B = {Base}_{M}$
2		suppmptcfin.r	$⊢ R = Scalar (M)$
3		suppmptcfin.0	$⊢ \underset{˙}{0} = 0_{R}$
4		suppmptcfin.1	$⊢ \underset{˙}{1} = 1_{R}$
5		suppmptcfin.f	$⊢ F = (x \in V ⟼ if (x = X, \underset{˙}{1}, \underset{˙}{0}))$
6	5	funmpt2	$⊢ Fun F$
7	6	a1i	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to Fun F$
8	1 2 3 4 5	suppmptcfin	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F supp \underset{˙}{0} \in Fin$
9		mptexg	$⊢ V \in 𝒫 B \to (x \in V ⟼ if (x = X, \underset{˙}{1}, \underset{˙}{0})) \in V$
10	5 9	eqeltrid	$⊢ V \in 𝒫 B \to F \in V$
11	10	3ad2ant2	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to F \in V$
12	3	fvexi	$⊢ \underset{˙}{0} \in V$
13		isfsupp	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow (Fun F \land F supp \underset{˙}{0} \in Fin))$
14	11 12 13	sylancl	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow (Fun F \land F supp \underset{˙}{0} \in Fin))$
15	7 8 14	mpbir2and	$⊢ (M \in LMod \land V \in 𝒫 B \land X \in V) \to {finSupp}_{\underset{˙}{0}} (F)$

Metamath Proof Explorer