MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptscmfsupp0 Structured version   Visualization version   GIF version
Theorem mptscmfsupp0 20814
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.)
Hypotheses
Ref Expression
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
Ref Expression
mptscmfsupp0 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) finSupp 0 )
Distinct variable groups:   𝐡,π‘˜   𝐷,π‘˜   π‘˜,𝐾   πœ‘,π‘˜   βˆ— ,π‘˜
Allowed substitution hints:   𝑄(π‘˜)   𝑅(π‘˜)   𝑆(π‘˜)   𝑉(π‘˜)   π‘Š(π‘˜)   0 (π‘˜)   𝑍(π‘˜)
Proof of Theorem mptscmfsupp0
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 mptscmfsupp0.d . . 3 (πœ‘ β†’ 𝐷 ∈ 𝑉)
21mptexd 7234 . 2 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) ∈ V)
3 funmpt 6590 . . 3 Fun (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))
43a1i 11 . 2 (πœ‘ β†’ Fun (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)))
5 mptscmfsupp0.0 . . . 4 0 = (0gβ€˜π‘„)
65fvexi 6908 . . 3 0 ∈ V
76a1i 11 . 2 (πœ‘ β†’ 0 ∈ V)
8 mptscmfsupp0.f . . 3 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ 𝑆) finSupp 𝑍)
98fsuppimpd 9393 . 2 (πœ‘ β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin)
10 simpr 483 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ 𝐷)
11 mptscmfsupp0.s . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ 𝐷) β†’ 𝑆 ∈ 𝐡)
1211ralrimiva 3136 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐷 𝑆 ∈ 𝐡)
1312adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ βˆ€π‘˜ ∈ 𝐷 𝑆 ∈ 𝐡)
14 rspcsbela 4436 . . . . . . . . 9 ((𝑑 ∈ 𝐷 ∧ βˆ€π‘˜ ∈ 𝐷 𝑆 ∈ 𝐡) β†’ ⦋𝑑 / π‘˜β¦Œπ‘† ∈ 𝐡)
1510, 13, 14syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ⦋𝑑 / π‘˜β¦Œπ‘† ∈ 𝐡)
16 eqid 2725 . . . . . . . . 9 (π‘˜ ∈ 𝐷 ↦ 𝑆) = (π‘˜ ∈ 𝐷 ↦ 𝑆)
1716fvmpts 7005 . . . . . . . 8 ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / π‘˜β¦Œπ‘† ∈ 𝐡) β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) = ⦋𝑑 / π‘˜β¦Œπ‘†)
1810, 15, 17syl2anc 582 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) = ⦋𝑑 / π‘˜β¦Œπ‘†)
1918eqeq1d 2727 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) = 𝑍 ↔ ⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍))
20 oveq1 7424 . . . . . . . . 9 (⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍 β†’ (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = (𝑍 βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š))
21 mptscmfsupp0.z . . . . . . . . . . . 12 𝑍 = (0gβ€˜π‘…)
22 mptscmfsupp0.r . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 = (Scalarβ€˜π‘„))
2322adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑅 = (Scalarβ€˜π‘„))
2423fveq2d 6898 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘„)))
2521, 24eqtrid 2777 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑍 = (0gβ€˜(Scalarβ€˜π‘„)))
2625oveq1d 7432 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (𝑍 βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = ((0gβ€˜(Scalarβ€˜π‘„)) βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š))
27 mptscmfsupp0.q . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ LMod)
2827adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑄 ∈ LMod)
29 mptscmfsupp0.w . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐷) β†’ π‘Š ∈ 𝐾)
3029ralrimiva 3136 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐷 π‘Š ∈ 𝐾)
3130adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ βˆ€π‘˜ ∈ 𝐷 π‘Š ∈ 𝐾)
32 rspcsbela 4436 . . . . . . . . . . . 12 ((𝑑 ∈ 𝐷 ∧ βˆ€π‘˜ ∈ 𝐷 π‘Š ∈ 𝐾) β†’ ⦋𝑑 / π‘˜β¦Œπ‘Š ∈ 𝐾)
3310, 31, 32syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ⦋𝑑 / π‘˜β¦Œπ‘Š ∈ 𝐾)
34 mptscmfsupp0.k . . . . . . . . . . . 12 𝐾 = (Baseβ€˜π‘„)
35 eqid 2725 . . . . . . . . . . . 12 (Scalarβ€˜π‘„) = (Scalarβ€˜π‘„)
36 mptscmfsupp0.m . . . . . . . . . . . 12 βˆ— = ( ·𝑠 β€˜π‘„)
37 eqid 2725 . . . . . . . . . . . 12 (0gβ€˜(Scalarβ€˜π‘„)) = (0gβ€˜(Scalarβ€˜π‘„))
3834, 35, 36, 37, 5lmod0vs 20782 . . . . . . . . . . 11 ((𝑄 ∈ LMod ∧ ⦋𝑑 / π‘˜β¦Œπ‘Š ∈ 𝐾) β†’ ((0gβ€˜(Scalarβ€˜π‘„)) βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 )
3928, 33, 38syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ((0gβ€˜(Scalarβ€˜π‘„)) βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 )
4026, 39eqtrd 2765 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (𝑍 βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 )
4120, 40sylan9eqr 2787 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍) β†’ (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 )
42 csbov12g 7462 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝐷 β†’ ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š) = (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š))
4342adantl 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š) = (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š))
44 ovex 7450 . . . . . . . . . . . . 13 (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) ∈ V
4543, 44eqeltrdi 2833 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š) ∈ V)
46 eqid 2725 . . . . . . . . . . . . 13 (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) = (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))
4746fvmpts 7005 . . . . . . . . . . . 12 ((𝑑 ∈ 𝐷 ∧ ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š) ∈ V) β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š))
4810, 45, 47syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = ⦋𝑑 / π‘˜β¦Œ(𝑆 βˆ— π‘Š))
4948, 43eqtrd 2765 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š))
5049eqeq1d 2727 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = 0 ↔ (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 ))
5150adantr 479 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍) β†’ (((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = 0 ↔ (⦋𝑑 / π‘˜β¦Œπ‘† βˆ— ⦋𝑑 / π‘˜β¦Œπ‘Š) = 0 ))
5241, 51mpbird 256 . . . . . . 7 (((πœ‘ ∧ 𝑑 ∈ 𝐷) ∧ ⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍) β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = 0 )
5352ex 411 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (⦋𝑑 / π‘˜β¦Œπ‘† = 𝑍 β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = 0 ))
5419, 53sylbid 239 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) = 𝑍 β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) = 0 ))
5554necon3d 2951 . . . 4 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) β‰  0 β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) β‰  𝑍))
5655ss2rabdv 4070 . . 3 (πœ‘ β†’ {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) β‰  0 } βŠ† {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) β‰  𝑍})
57 ovex 7450 . . . . . 6 (𝑆 βˆ— π‘Š) ∈ V
5857rgenw 3055 . . . . 5 βˆ€π‘˜ ∈ 𝐷 (𝑆 βˆ— π‘Š) ∈ V
5946fnmpt 6694 . . . . 5 (βˆ€π‘˜ ∈ 𝐷 (𝑆 βˆ— π‘Š) ∈ V β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) Fn 𝐷)
6058, 59mp1i 13 . . . 4 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) Fn 𝐷)
61 suppvalfn 8171 . . . 4 (((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 0 ∈ V) β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) β‰  0 })
6260, 1, 7, 61syl3anc 1368 . . 3 (πœ‘ β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) supp 0 ) = {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š))β€˜π‘‘) β‰  0 })
6316fnmpt 6694 . . . . 5 (βˆ€π‘˜ ∈ 𝐷 𝑆 ∈ 𝐡 β†’ (π‘˜ ∈ 𝐷 ↦ 𝑆) Fn 𝐷)
6412, 63syl 17 . . . 4 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ 𝑆) Fn 𝐷)
6521fvexi 6908 . . . . 5 𝑍 ∈ V
6665a1i 11 . . . 4 (πœ‘ β†’ 𝑍 ∈ V)
67 suppvalfn 8171 . . . 4 (((π‘˜ ∈ 𝐷 ↦ 𝑆) Fn 𝐷 ∧ 𝐷 ∈ 𝑉 ∧ 𝑍 ∈ V) β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) β‰  𝑍})
6864, 1, 66, 67syl3anc 1368 . . 3 (πœ‘ β†’ ((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍) = {𝑑 ∈ 𝐷 ∣ ((π‘˜ ∈ 𝐷 ↦ 𝑆)β€˜π‘‘) β‰  𝑍})
6956, 62, 683sstr4d 4025 . 2 (πœ‘ β†’ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) supp 0 ) βŠ† ((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍))
70 suppssfifsupp 9403 . 2 ((((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) ∈ V ∧ Fun (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) ∧ 0 ∈ V) ∧ (((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍) ∈ Fin ∧ ((π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) supp 0 ) βŠ† ((π‘˜ ∈ 𝐷 ↦ 𝑆) supp 𝑍))) β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) finSupp 0 )
712, 4, 7, 9, 69, 70syl32anc 1375 1 (πœ‘ β†’ (π‘˜ ∈ 𝐷 ↦ (𝑆 βˆ— π‘Š)) finSupp 0 )
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  {crab 3419  Vcvv 3463  β¦‹csb 3890   βŠ† wss 3945   class class class wbr 5148   ↦ cmpt 5231  Fun wfun 6541   Fn wfn 6542  β€˜cfv 6547  (class class class)co 7417   supp csupp 8163  Fincfn 8962   finSupp cfsupp 9385  Basecbs 17179  Scalarcsca 17235   ·𝑠 cvsca 17236  0gc0g 17420  LModclmod 20747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-supp 8164  df-1o 8485  df-en 8963  df-fin 8966  df-fsupp 9386  df-0g 17422  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18897  df-ring 20179  df-lmod 20749
This theorem is referenced by:  mptscmfsuppd  20815  gsumsmonply1  22235  pm2mpcl  22729  mply1topmatcllem  22735  mp2pm2mplem5  22742  pm2mpghmlem2  22744  chcoeffeqlem  22817  lbsdiflsp0  33394  fedgmullem2  33398
  Copyright terms: Public domain W3C validator