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 = {Base}_{P}$
	mptscmfsuppd.s	$⊢ S = Scalar (P)$
	mptscmfsuppd.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mptscmfsuppd.p	$⊢ φ \to P \in LMod$
	mptscmfsuppd.x	$⊢ φ \to X \in V$
	mptscmfsuppd.z	$⊢ (φ \land k \in X) \to Z \in B$
	mptscmfsuppd.a	$⊢ φ \to A : X ⟶ Y$
	mptscmfsuppd.f	$⊢ φ \to {finSupp}_{0_{S}} (A)$
Assertion	mptscmfsuppd	$⊢ φ \to {finSupp}_{0_{P}} ((k \in X ⟼ A (k) \underset{˙}{\cdot} Z))$

Proof

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

Metamath Proof Explorer

Theorem mptscmfsuppd

Proof