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={\mathrm{Base}}_M$$
	suppmptcfin.r	$$⊢R=\mathrm{Scalar}\left(M\right)$$
	suppmptcfin.0	$$⊢\underset{\dot{}}{0}=0_R$$
	suppmptcfin.1	$$⊢\underset{\dot{}}{1}=1_R$$
	suppmptcfin.f	$$⊢F=\left(x\in V⟼if\left(x=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
Assertion	suppmptcfin	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		suppmptcfin.b	$$⊢B={\mathrm{Base}}_M$$
2		suppmptcfin.r	$$⊢R=\mathrm{Scalar}\left(M\right)$$
3		suppmptcfin.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		suppmptcfin.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		suppmptcfin.f	$$⊢F=\left(x\in V⟼if\left(x=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
6		eqeq1	$$⊢x=v\to \left(x=X\leftrightarrow v=X\right)$$
7	6	ifbid	$$⊢x=v\to if\left(x=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
8	7	cbvmptv	$$⊢\left(x\in V⟼if\left(x=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(v\in V⟼if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
9	5 8	eqtri	$$⊢F=\left(v\in V⟼if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
10		simp2	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to V\in 𝒫B$$
11	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
12	11	a1i	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
13	4	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
14	13	a1i	$$⊢\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to \underset{\dot{}}{1}\in \mathrm{V}$$
15	11	a1i	$$⊢\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
16	14 15	ifcld	$$⊢\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
17	9 10 12 16	mptsuppd	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to F\mathrm{supp}\underset{\dot{}}{0}=\left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}$$
18		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
19		2a1	$$⊢v=X\to \left(\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to \left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)\right)$$
20		iffalse	$$⊢\neg v=X\to if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
21	20	adantr	$$⊢\left(\neg v=X\wedge \left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\right)\to if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
22	21	neeq1d	$$⊢\left(\neg v=X\wedge \left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\right)\to \left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}\ne \underset{\dot{}}{0}\right)$$
23		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
24		eqneqall	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{0}\ne \underset{\dot{}}{0}\to v=X\right)$$
25	23 24	ax-mp	$$⊢\underset{\dot{}}{0}\ne \underset{\dot{}}{0}\to v=X$$
26	22 25	syl6bi	$$⊢\left(\neg v=X\wedge \left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\right)\to \left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)$$
27	26	ex	$$⊢\neg v=X\to \left(\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to \left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)\right)$$
28	19 27	pm2.61i	$$⊢\left(\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\wedge v\in V\right)\to \left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)$$
29	28	ralrimiva	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to \forall v\in V\left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)$$
30		rabsssn	$$⊢\left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}\subseteq \left\{X\right\}\leftrightarrow \forall v\in V\left(if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\to v=X\right)$$
31	29 30	sylibr	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to \left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}\subseteq \left\{X\right\}$$
32		ssfi	$$⊢\left(\left\{X\right\}\in \mathrm{Fin}\wedge \left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}\subseteq \left\{X\right\}\right)\to \left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
33	18 31 32	sylancr	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to \left\{v\in V|if\left(v=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
34	17 33	eqeltrd	$$⊢\left(M\in \mathrm{LMod}\wedge V\in 𝒫B\wedge X\in V\right)\to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$