Theorem 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	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	mptscmfsupp0.q	⊢ ( 𝜑 → 𝑄 ∈ LMod )
	mptscmfsupp0.r	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑄 ) )
	mptscmfsupp0.k	⊢ 𝐾 = ( Base ‘ 𝑄 )
	mptscmfsupp0.s	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑆 ∈ 𝐵 )
	mptscmfsupp0.w	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑊 ∈ 𝐾 )
	mptscmfsupp0.0	⊢ 0 = ( 0g ‘ 𝑄 )
	mptscmfsupp0.z	⊢ 𝑍 = ( 0g ‘ 𝑅 )
	mptscmfsupp0.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	mptscmfsupp0.f	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) finSupp 𝑍 )
Assertion	mptscmfsupp0	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		mptscmfsupp0.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
2		mptscmfsupp0.q	⊢ ( 𝜑 → 𝑄 ∈ LMod )
3		mptscmfsupp0.r	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑄 ) )
4		mptscmfsupp0.k	⊢ 𝐾 = ( Base ‘ 𝑄 )
5		mptscmfsupp0.s	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑆 ∈ 𝐵 )
6		mptscmfsupp0.w	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑊 ∈ 𝐾 )
7		mptscmfsupp0.0	⊢ 0 = ( 0g ‘ 𝑄 )
8		mptscmfsupp0.z	⊢ 𝑍 = ( 0g ‘ 𝑅 )
9		mptscmfsupp0.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
10		mptscmfsupp0.f	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) finSupp 𝑍 )
11	1	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ∈ V )
12		funmpt	⊢ Fun ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) )
13	12	a1i	⊢ ( 𝜑 → Fun ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) )
14	7	fvexi	⊢ 0 ∈ V
15	14	a1i	⊢ ( 𝜑 → 0 ∈ V )
16	10	fsuppimpd	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) ∈ Fin )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ 𝐷 )
18	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐷 𝑆 ∈ 𝐵 )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ∀ 𝑘 ∈ 𝐷 𝑆 ∈ 𝐵 )
20		rspcsbela	⊢ ( ( 𝑑 ∈ 𝐷 ∧ ∀ 𝑘 ∈ 𝐷 𝑆 ∈ 𝐵 ) → ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∈ 𝐵 )
21	17 19 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∈ 𝐵 )
22		eqid	⊢ ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) = ( 𝑘 ∈ 𝐷 ↦ 𝑆 )
23	22	fvmpts	⊢ ( ( 𝑑 ∈ 𝐷 ∧ ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) = ⦋ 𝑑 / 𝑘 ⦌ 𝑆 )
24	17 21 23	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) = ⦋ 𝑑 / 𝑘 ⦌ 𝑆 )
25	24	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) = 𝑍 ↔ ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 ) )
26		oveq1	⊢ ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 → ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = ( 𝑍 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) )
27	3	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑅 = ( Scalar ‘ 𝑄 ) )
28	27	fveq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
29	8 28	eqtrid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑍 = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
30	29	oveq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑍 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) )
31	2	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑄 ∈ LMod )
32	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐷 𝑊 ∈ 𝐾 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ∀ 𝑘 ∈ 𝐷 𝑊 ∈ 𝐾 )
34		rspcsbela	⊢ ( ( 𝑑 ∈ 𝐷 ∧ ∀ 𝑘 ∈ 𝐷 𝑊 ∈ 𝐾 ) → ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ∈ 𝐾 )
35	17 33 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ∈ 𝐾 )
36		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
37		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
38	4 36 9 37 7	lmod0vs	⊢ ( ( 𝑄 ∈ LMod ∧ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ∈ 𝐾 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 )
39	31 35 38	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 )
40	30 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑍 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 )
41	26 40	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 ) → ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 )
42		csbov12g	⊢ ( 𝑑 ∈ 𝐷 → ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) = ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) = ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) )
44		ovex	⊢ ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) ∈ V
45	43 44	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) ∈ V )
46		eqid	⊢ ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) )
47	46	fvmpts	⊢ ( ( 𝑑 ∈ 𝐷 ∧ ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) ∈ V ) → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) )
48	17 45 47	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = ⦋ 𝑑 / 𝑘 ⦌ ( 𝑆 ∗ 𝑊 ) )
49	48 43	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) )
50	49	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = 0 ↔ ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 ) )
51	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 ) → ( ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = 0 ↔ ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 ∗ ⦋ 𝑑 / 𝑘 ⦌ 𝑊 ) = 0 ) )
52	41 51	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) ∧ ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 ) → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = 0 )
53	52	ex	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ⦋ 𝑑 / 𝑘 ⦌ 𝑆 = 𝑍 → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = 0 ) )
54	25 53	sylbid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) = 𝑍 → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) = 0 ) )
55	54	necon3d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) ≠ 0 → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) ≠ 𝑍 ) )
56	55	ss2rabdv	⊢ ( 𝜑 → { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) ≠ 0 } ⊆ { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) ≠ 𝑍 } )
57		ovex	⊢ ( 𝑆 ∗ 𝑊 ) ∈ V
58	57	rgenw	⊢ ∀ 𝑘 ∈ 𝐷 ( 𝑆 ∗ 𝑊 ) ∈ V
59	46	fnmpt	⊢ ( ∀ 𝑘 ∈ 𝐷 ( 𝑆 ∗ 𝑊 ) ∈ V → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) Fn 𝐷 )
60	58 59	mp1i	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) Fn 𝐷 )
61		suppvalfn	⊢ ( ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) supp 0 ) = { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) ≠ 0 } )
62	60 1 15 61	syl3anc	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) supp 0 ) = { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ‘ 𝑑 ) ≠ 0 } )
63	22	fnmpt	⊢ ( ∀ 𝑘 ∈ 𝐷 𝑆 ∈ 𝐵 → ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) Fn 𝐷 )
64	18 63	syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) Fn 𝐷 )
65	8	fvexi	⊢ 𝑍 ∈ V
66	65	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
67		suppvalfn	⊢ ( ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 𝑍 ∈ V ) → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) = { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) ≠ 𝑍 } )
68	64 1 66 67	syl3anc	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) = { 𝑑 ∈ 𝐷 ∣ ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) ‘ 𝑑 ) ≠ 𝑍 } )
69	56 62 68	3sstr4d	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) supp 0 ) ⊆ ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) )
70		suppssfifsupp	⊢ ( ( ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) ∧ 0 ∈ V ) ∧ ( ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) ∈ Fin ∧ ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) supp 0 ) ⊆ ( ( 𝑘 ∈ 𝐷 ↦ 𝑆 ) supp 𝑍 ) ) ) → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) finSupp 0 )
71	11 13 15 16 69 70	syl32anc	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑆 ∗ 𝑊 ) ) finSupp 0 )