Theorem mptscmfsuppd

Description: A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe . (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 8-Aug-2019) (Proof shortened by AV, 18-Oct-2019)

	Ref	Expression
Hypotheses	mptscmfsuppd.b	$$⊢B={\mathrm{Base}}_P$$
	mptscmfsuppd.s	$$⊢S=\mathrm{Scalar}\left(P\right)$$
	mptscmfsuppd.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	mptscmfsuppd.p	$$⊢\phi \to P\in \mathrm{LMod}$$
	mptscmfsuppd.x	$$⊢\phi \to X\in V$$
	mptscmfsuppd.z	$$⊢\left(\phi \wedge k\in X\right)\to Z\in B$$
	mptscmfsuppd.a	$$⊢\phi \to A:X⟶Y$$
	mptscmfsuppd.f	$$⊢\phi \to {finSupp}_{0_S}\left(A\right)$$
Assertion	mptscmfsuppd	$$⊢\phi \to {finSupp}_{0_P}\left(\left(k\in X⟼A\left(k\right)\underset{\dot{}}{·}Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptscmfsuppd.b	$$⊢B={\mathrm{Base}}_P$$
2		mptscmfsuppd.s	$$⊢S=\mathrm{Scalar}\left(P\right)$$
3		mptscmfsuppd.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
4		mptscmfsuppd.p	$$⊢\phi \to P\in \mathrm{LMod}$$
5		mptscmfsuppd.x	$$⊢\phi \to X\in V$$
6		mptscmfsuppd.z	$$⊢\left(\phi \wedge k\in X\right)\to Z\in B$$
7		mptscmfsuppd.a	$$⊢\phi \to A:X⟶Y$$
8		mptscmfsuppd.f	$$⊢\phi \to {finSupp}_{0_S}\left(A\right)$$
9	2	a1i	$$⊢\phi \to S=\mathrm{Scalar}\left(P\right)$$
10		fvexd	$$⊢\left(\phi \wedge k\in X\right)\to A\left(k\right)\in \mathrm{V}$$
11		eqid	$$⊢0_P=0_P$$
12		eqid	$$⊢0_S=0_S$$
13	7	feqmptd	$$⊢\phi \to A=\left(k\in X⟼A\left(k\right)\right)$$
14	13 8	eqbrtrrd	$$⊢\phi \to {finSupp}_{0_S}\left(\left(k\in X⟼A\left(k\right)\right)\right)$$
15	5 4 9 1 10 6 11 12 3 14	mptscmfsupp0	$$⊢\phi \to {finSupp}_{0_P}\left(\left(k\in X⟼A\left(k\right)\underset{\dot{}}{·}Z\right)\right)$$