Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑍 = ( 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 )