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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	suppmptcfin.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	suppmptcfin.0	⊢ 0 = ( 0g ‘ 𝑅 )
	suppmptcfin.1	⊢ 1 = ( 1r ‘ 𝑅 )
	suppmptcfin.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
Assertion	mptcfsupp	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		suppmptcfin.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		suppmptcfin.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3		suppmptcfin.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		suppmptcfin.1	⊢ 1 = ( 1r ‘ 𝑅 )
5		suppmptcfin.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
6	5	funmpt2	⊢ Fun 𝐹
7	6	a1i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → Fun 𝐹 )
8	1 2 3 4 5	suppmptcfin	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 supp 0 ) ∈ Fin )
9		mptexg	⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) ∈ V )
10	5 9	eqeltrid	⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝐹 ∈ V )
11	10	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ V )
12	3	fvexi	⊢ 0 ∈ V
13		isfsupp	⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 finSupp 0 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) ) )
14	11 12 13	sylancl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 finSupp 0 ↔ ( Fun 𝐹 ∧ ( 𝐹 supp 0 ) ∈ Fin ) ) )
15	7 8 14	mpbir2and	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 finSupp 0 )