mptscmfsupp0

Description: A mapping to a scalar product is finitely supported if the mapping to the scalar is finitely supported. (Contributed by AV, 5-Oct-2019)

	Ref	Expression
Hypotheses	mptscmfsupp0.d	$⊢ φ \to D \in V$
	mptscmfsupp0.q	$⊢ φ \to Q \in LMod$
	mptscmfsupp0.r	$⊢ φ \to R = Scalar (Q)$
	mptscmfsupp0.k	$⊢ K = {Base}_{Q}$
	mptscmfsupp0.s	$⊢ (φ \land k \in D) \to S \in B$
	mptscmfsupp0.w	$⊢ (φ \land k \in D) \to W \in K$
	mptscmfsupp0.0	$⊢ \underset{˙}{0} = 0_{Q}$
	mptscmfsupp0.z	$⊢ Z = 0_{R}$
	mptscmfsupp0.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	mptscmfsupp0.f	$⊢ φ \to {finSupp}_{Z} ((k \in D ⟼ S))$
Assertion	mptscmfsupp0	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in D ⟼ S \underset{˙}{*} W))$

Proof

Step	Hyp	Ref	Expression
1		mptscmfsupp0.d	$⊢ φ \to D \in V$
2		mptscmfsupp0.q	$⊢ φ \to Q \in LMod$
3		mptscmfsupp0.r	$⊢ φ \to R = Scalar (Q)$
4		mptscmfsupp0.k	$⊢ K = {Base}_{Q}$
5		mptscmfsupp0.s	$⊢ (φ \land k \in D) \to S \in B$
6		mptscmfsupp0.w	$⊢ (φ \land k \in D) \to W \in K$
7		mptscmfsupp0.0	$⊢ \underset{˙}{0} = 0_{Q}$
8		mptscmfsupp0.z	$⊢ Z = 0_{R}$
9		mptscmfsupp0.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
10		mptscmfsupp0.f	$⊢ φ \to {finSupp}_{Z} ((k \in D ⟼ S))$
11	1	mptexd	$⊢ φ \to (k \in D ⟼ S \underset{˙}{*} W) \in V$
12		funmpt	$⊢ Fun (k \in D ⟼ S \underset{˙}{*} W)$
13	12	a1i	$⊢ φ \to Fun (k \in D ⟼ S \underset{˙}{*} W)$
14	7	fvexi	$⊢ \underset{˙}{0} \in V$
15	14	a1i	$⊢ φ \to \underset{˙}{0} \in V$
16	10	fsuppimpd	$⊢ φ \to (k \in D ⟼ S) supp Z \in Fin$
17		simpr	$⊢ (φ \land d \in D) \to d \in D$
18	5	ralrimiva	$⊢ φ \to \forall k \in D S \in B$
19	18	adantr	$⊢ (φ \land d \in D) \to \forall k \in D S \in B$
20		rspcsbela	$⊢ (d \in D \land \forall k \in D S \in B) \to ⦋ d / k ⦌ S \in B$
21	17 19 20	syl2anc	$⊢ (φ \land d \in D) \to ⦋ d / k ⦌ S \in B$
22		eqid	$⊢ (k \in D ⟼ S) = (k \in D ⟼ S)$
23	22	fvmpts	$⊢ (d \in D \land ⦋ d / k ⦌ S \in B) \to (k \in D ⟼ S) (d) = ⦋ d / k ⦌ S$
24	17 21 23	syl2anc	$⊢ (φ \land d \in D) \to (k \in D ⟼ S) (d) = ⦋ d / k ⦌ S$
25	24	eqeq1d	$⊢ (φ \land d \in D) \to ((k \in D ⟼ S) (d) = Z \leftrightarrow ⦋ d / k ⦌ S = Z)$
26		oveq1	$⊢ ⦋ d / k ⦌ S = Z \to ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W = Z \underset{˙}{} ⦋ d / k ⦌ W$
27	3	adantr	$⊢ (φ \land d \in D) \to R = Scalar (Q)$
28	27	fveq2d	$⊢ (φ \land d \in D) \to 0_{R} = 0_{Scalar (Q)}$
29	8 28	syl5eq	$⊢ (φ \land d \in D) \to Z = 0_{Scalar (Q)}$
30	29	oveq1d	$⊢ (φ \land d \in D) \to Z \underset{˙}{} ⦋ d / k ⦌ W = 0_{Scalar (Q)} \underset{˙}{} ⦋ d / k ⦌ W$
31	2	adantr	$⊢ (φ \land d \in D) \to Q \in LMod$
32	6	ralrimiva	$⊢ φ \to \forall k \in D W \in K$
33	32	adantr	$⊢ (φ \land d \in D) \to \forall k \in D W \in K$
34		rspcsbela	$⊢ (d \in D \land \forall k \in D W \in K) \to ⦋ d / k ⦌ W \in K$
35	17 33 34	syl2anc	$⊢ (φ \land d \in D) \to ⦋ d / k ⦌ W \in K$
36		eqid	$⊢ Scalar (Q) = Scalar (Q)$
37		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
38	4 36 9 37 7	lmod0vs	$⊢ (Q \in LMod \land ⦋ d / k ⦌ W \in K) \to 0_{Scalar (Q)} \underset{˙}{*} ⦋ d / k ⦌ W = \underset{˙}{0}$
39	31 35 38	syl2anc	$⊢ (φ \land d \in D) \to 0_{Scalar (Q)} \underset{˙}{*} ⦋ d / k ⦌ W = \underset{˙}{0}$
40	30 39	eqtrd	$⊢ (φ \land d \in D) \to Z \underset{˙}{*} ⦋ d / k ⦌ W = \underset{˙}{0}$
41	26 40	sylan9eqr	$⊢ ((φ \land d \in D) \land ⦋ d / k ⦌ S = Z) \to ⦋ d / k ⦌ S \underset{˙}{*} ⦋ d / k ⦌ W = \underset{˙}{0}$
42		csbov12g	$⊢ d \in D \to ⦋ d / k ⦌ (S \underset{˙}{} W) = ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W$
43	42	adantl	$⊢ (φ \land d \in D) \to ⦋ d / k ⦌ (S \underset{˙}{} W) = ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W$
44		ovex	$⊢ ⦋ d / k ⦌ S \underset{˙}{*} ⦋ d / k ⦌ W \in V$
45	43 44	eqeltrdi	$⊢ (φ \land d \in D) \to ⦋ d / k ⦌ (S \underset{˙}{*} W) \in V$
46		eqid	$⊢ (k \in D ⟼ S \underset{˙}{} W) = (k \in D ⟼ S \underset{˙}{} W)$
47	46	fvmpts	$⊢ (d \in D \land ⦋ d / k ⦌ (S \underset{˙}{} W) \in V) \to (k \in D ⟼ S \underset{˙}{} W) (d) = ⦋ d / k ⦌ (S \underset{˙}{*} W)$
48	17 45 47	syl2anc	$⊢ (φ \land d \in D) \to (k \in D ⟼ S \underset{˙}{} W) (d) = ⦋ d / k ⦌ (S \underset{˙}{} W)$
49	48 43	eqtrd	$⊢ (φ \land d \in D) \to (k \in D ⟼ S \underset{˙}{} W) (d) = ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W$
50	49	eqeq1d	$⊢ (φ \land d \in D) \to ((k \in D ⟼ S \underset{˙}{} W) (d) = \underset{˙}{0} \leftrightarrow ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W = \underset{˙}{0})$
51	50	adantr	$⊢ ((φ \land d \in D) \land ⦋ d / k ⦌ S = Z) \to ((k \in D ⟼ S \underset{˙}{} W) (d) = \underset{˙}{0} \leftrightarrow ⦋ d / k ⦌ S \underset{˙}{} ⦋ d / k ⦌ W = \underset{˙}{0})$
52	41 51	mpbird	$⊢ ((φ \land d \in D) \land ⦋ d / k ⦌ S = Z) \to (k \in D ⟼ S \underset{˙}{*} W) (d) = \underset{˙}{0}$
53	52	ex	$⊢ (φ \land d \in D) \to (⦋ d / k ⦌ S = Z \to (k \in D ⟼ S \underset{˙}{*} W) (d) = \underset{˙}{0})$
54	25 53	sylbid	$⊢ (φ \land d \in D) \to ((k \in D ⟼ S) (d) = Z \to (k \in D ⟼ S \underset{˙}{*} W) (d) = \underset{˙}{0})$
55	54	necon3d	$⊢ (φ \land d \in D) \to ((k \in D ⟼ S \underset{˙}{*} W) (d) \neq \underset{˙}{0} \to (k \in D ⟼ S) (d) \neq Z)$
56	55	ss2rabdv	$⊢ φ \to \{d \in D \| (k \in D ⟼ S \underset{˙}{*} W) (d) \neq \underset{˙}{0}\} \subseteq \{d \in D \| (k \in D ⟼ S) (d) \neq Z\}$
57		ovex	$⊢ S \underset{˙}{*} W \in V$
58	57	rgenw	$⊢ \forall k \in D S \underset{˙}{*} W \in V$
59	46	fnmpt	$⊢ \forall k \in D S \underset{˙}{} W \in V \to (k \in D ⟼ S \underset{˙}{} W) Fn D$
60	58 59	mp1i	$⊢ φ \to (k \in D ⟼ S \underset{˙}{*} W) Fn D$
61		suppvalfn	$⊢ ((k \in D ⟼ S \underset{˙}{} W) Fn D \land D \in V \land \underset{˙}{0} \in V) \to (k \in D ⟼ S \underset{˙}{} W) supp \underset{˙}{0} = \{d \in D \| (k \in D ⟼ S \underset{˙}{*} W) (d) \neq \underset{˙}{0}\}$
62	60 1 15 61	syl3anc	$⊢ φ \to (k \in D ⟼ S \underset{˙}{} W) supp \underset{˙}{0} = \{d \in D \| (k \in D ⟼ S \underset{˙}{} W) (d) \neq \underset{˙}{0}\}$
63	22	fnmpt	$⊢ \forall k \in D S \in B \to (k \in D ⟼ S) Fn D$
64	18 63	syl	$⊢ φ \to (k \in D ⟼ S) Fn D$
65	8	fvexi	$⊢ Z \in V$
66	65	a1i	$⊢ φ \to Z \in V$
67		suppvalfn	$⊢ ((k \in D ⟼ S) Fn D \land D \in V \land Z \in V) \to (k \in D ⟼ S) supp Z = \{d \in D \| (k \in D ⟼ S) (d) \neq Z\}$
68	64 1 66 67	syl3anc	$⊢ φ \to (k \in D ⟼ S) supp Z = \{d \in D \| (k \in D ⟼ S) (d) \neq Z\}$
69	56 62 68	3sstr4d	$⊢ φ \to (k \in D ⟼ S \underset{˙}{*} W) supp \underset{˙}{0} \subseteq (k \in D ⟼ S) supp Z$
70		suppssfifsupp	$⊢ (((k \in D ⟼ S \underset{˙}{} W) \in V \land Fun (k \in D ⟼ S \underset{˙}{} W) \land \underset{˙}{0} \in V) \land ((k \in D ⟼ S) supp Z \in Fin \land (k \in D ⟼ S \underset{˙}{} W) supp \underset{˙}{0} \subseteq (k \in D ⟼ S) supp Z)) \to {finSupp}_{\underset{˙}{0}} ((k \in D ⟼ S \underset{˙}{} W))$
71	11 13 15 16 69 70	syl32anc	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in D ⟼ S \underset{˙}{*} W))$

Metamath Proof Explorer

Theorem mptscmfsupp0

Proof