MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptscmfsupp0 Structured version   Visualization version   GIF version

Theorem mptscmfsupp0 19421
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 6813 . 2 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V)
3 funmpt 6226 . . 3 Fun (𝑘𝐷 ↦ (𝑆 𝑊))
43a1i 11 . 2 (𝜑 → Fun (𝑘𝐷 ↦ (𝑆 𝑊)))
5 mptscmfsupp0.0 . . . 4 0 = (0g𝑄)
65fvexi 6513 . . 3 0 ∈ V
76a1i 11 . 2 (𝜑0 ∈ V)
8 mptscmfsupp0.f . . 3 (𝜑 → (𝑘𝐷𝑆) finSupp 𝑍)
98fsuppimpd 8635 . 2 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) ∈ Fin)
10 simpr 477 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑𝐷)
11 mptscmfsupp0.s . . . . . . . . . . 11 ((𝜑𝑘𝐷) → 𝑆𝐵)
1211ralrimiva 3132 . . . . . . . . . 10 (𝜑 → ∀𝑘𝐷 𝑆𝐵)
1312adantr 473 . . . . . . . . 9 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑆𝐵)
14 rspcsbela 4271 . . . . . . . . 9 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑆𝐵) → 𝑑 / 𝑘𝑆𝐵)
1510, 13, 14syl2anc 576 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑆𝐵)
16 eqid 2778 . . . . . . . . 9 (𝑘𝐷𝑆) = (𝑘𝐷𝑆)
1716fvmpts 6598 . . . . . . . 8 ((𝑑𝐷𝑑 / 𝑘𝑆𝐵) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
1810, 15, 17syl2anc 576 . . . . . . 7 ((𝜑𝑑𝐷) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
1918eqeq1d 2780 . . . . . 6 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍𝑑 / 𝑘𝑆 = 𝑍))
20 oveq1 6983 . . . . . . . . 9 (𝑑 / 𝑘𝑆 = 𝑍 → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = (𝑍 𝑑 / 𝑘𝑊))
21 mptscmfsupp0.z . . . . . . . . . . . 12 𝑍 = (0g𝑅)
22 mptscmfsupp0.r . . . . . . . . . . . . . 14 (𝜑𝑅 = (Scalar‘𝑄))
2322adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑅 = (Scalar‘𝑄))
2423fveq2d 6503 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → (0g𝑅) = (0g‘(Scalar‘𝑄)))
2521, 24syl5eq 2826 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑍 = (0g‘(Scalar‘𝑄)))
2625oveq1d 6991 . . . . . . . . . 10 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊))
27 mptscmfsupp0.q . . . . . . . . . . . 12 (𝜑𝑄 ∈ LMod)
2827adantr 473 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑄 ∈ LMod)
29 mptscmfsupp0.w . . . . . . . . . . . . . 14 ((𝜑𝑘𝐷) → 𝑊𝐾)
3029ralrimiva 3132 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝐷 𝑊𝐾)
3130adantr 473 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑊𝐾)
32 rspcsbela 4271 . . . . . . . . . . . 12 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑊𝐾) → 𝑑 / 𝑘𝑊𝐾)
3310, 31, 32syl2anc 576 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑊𝐾)
34 mptscmfsupp0.k . . . . . . . . . . . 12 𝐾 = (Base‘𝑄)
35 eqid 2778 . . . . . . . . . . . 12 (Scalar‘𝑄) = (Scalar‘𝑄)
36 mptscmfsupp0.m . . . . . . . . . . . 12 = ( ·𝑠𝑄)
37 eqid 2778 . . . . . . . . . . . 12 (0g‘(Scalar‘𝑄)) = (0g‘(Scalar‘𝑄))
3834, 35, 36, 37, 5lmod0vs 19389 . . . . . . . . . . 11 ((𝑄 ∈ LMod ∧ 𝑑 / 𝑘𝑊𝐾) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
3928, 33, 38syl2anc 576 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
4026, 39eqtrd 2814 . . . . . . . . 9 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = 0 )
4120, 40sylan9eqr 2836 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 )
42 csbov12g 7019 . . . . . . . . . . . . . 14 (𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
4342adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
44 ovex 7008 . . . . . . . . . . . . 13 (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) ∈ V
4543, 44syl6eqel 2874 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) ∈ V)
46 eqid 2778 . . . . . . . . . . . . 13 (𝑘𝐷 ↦ (𝑆 𝑊)) = (𝑘𝐷 ↦ (𝑆 𝑊))
4746fvmpts 6598 . . . . . . . . . . . 12 ((𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
4810, 45, 47syl2anc 576 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
4948, 43eqtrd 2814 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
5049eqeq1d 2780 . . . . . . . . 9 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5150adantr 473 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5241, 51mpbird 249 . . . . . . 7 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 )
5352ex 405 . . . . . 6 ((𝜑𝑑𝐷) → (𝑑 / 𝑘𝑆 = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5419, 53sylbid 232 . . . . 5 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5554necon3d 2988 . . . 4 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 → ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍))
5655ss2rabdv 3942 . . 3 (𝜑 → {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 } ⊆ {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
57 ovex 7008 . . . . . 6 (𝑆 𝑊) ∈ V
5857rgenw 3100 . . . . 5 𝑘𝐷 (𝑆 𝑊) ∈ V
5946fnmpt 6318 . . . . 5 (∀𝑘𝐷 (𝑆 𝑊) ∈ V → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
6058, 59mp1i 13 . . . 4 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
61 suppvalfn 7640 . . . 4 (((𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷𝐷𝑉0 ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6260, 1, 7, 61syl3anc 1351 . . 3 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6316fnmpt 6318 . . . . 5 (∀𝑘𝐷 𝑆𝐵 → (𝑘𝐷𝑆) Fn 𝐷)
6412, 63syl 17 . . . 4 (𝜑 → (𝑘𝐷𝑆) Fn 𝐷)
6521fvexi 6513 . . . . 5 𝑍 ∈ V
6665a1i 11 . . . 4 (𝜑𝑍 ∈ V)
67 suppvalfn 7640 . . . 4 (((𝑘𝐷𝑆) Fn 𝐷𝐷𝑉𝑍 ∈ V) → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
6864, 1, 66, 67syl3anc 1351 . . 3 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
6956, 62, 683sstr4d 3904 . 2 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) ⊆ ((𝑘𝐷𝑆) supp 𝑍))
70 suppssfifsupp 8643 . 2 ((((𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V ∧ Fun (𝑘𝐷 ↦ (𝑆 𝑊)) ∧ 0 ∈ V) ∧ (((𝑘𝐷𝑆) supp 𝑍) ∈ Fin ∧ ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) ⊆ ((𝑘𝐷𝑆) supp 𝑍))) → (𝑘𝐷 ↦ (𝑆 𝑊)) finSupp 0 )
712, 4, 7, 9, 69, 70syl32anc 1358 1 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) finSupp 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wne 2967  wral 3088  {crab 3092  Vcvv 3415  csb 3786  wss 3829   class class class wbr 4929  cmpt 5008  Fun wfun 6182   Fn wfn 6183  cfv 6188  (class class class)co 6976   supp csupp 7633  Fincfn 8306   finSupp cfsupp 8628  Basecbs 16339  Scalarcsca 16424   ·𝑠 cvsca 16425  0gc0g 16569  LModclmod 19356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-supp 7634  df-er 8089  df-en 8307  df-fin 8310  df-fsupp 8629  df-0g 16571  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-grp 17894  df-ring 19022  df-lmod 19358
This theorem is referenced by:  mptscmfsuppd  19422  gsumsmonply1  20174  pm2mpcl  21109  mply1topmatcllem  21115  mp2pm2mplem5  21122  pm2mpghmlem2  21124  chcoeffeqlem  21197  lbsdiflsp0  30657  fedgmullem2  30661
  Copyright terms: Public domain W3C validator