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

Theorem mptscmfsupp0 19695
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 6968 . 2 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V)
3 funmpt 6366 . . 3 Fun (𝑘𝐷 ↦ (𝑆 𝑊))
43a1i 11 . 2 (𝜑 → Fun (𝑘𝐷 ↦ (𝑆 𝑊)))
5 mptscmfsupp0.0 . . . 4 0 = (0g𝑄)
65fvexi 6663 . . 3 0 ∈ V
76a1i 11 . 2 (𝜑0 ∈ V)
8 mptscmfsupp0.f . . 3 (𝜑 → (𝑘𝐷𝑆) finSupp 𝑍)
98fsuppimpd 8828 . 2 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) ∈ Fin)
10 simpr 488 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑𝐷)
11 mptscmfsupp0.s . . . . . . . . . . 11 ((𝜑𝑘𝐷) → 𝑆𝐵)
1211ralrimiva 3152 . . . . . . . . . 10 (𝜑 → ∀𝑘𝐷 𝑆𝐵)
1312adantr 484 . . . . . . . . 9 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑆𝐵)
14 rspcsbela 4346 . . . . . . . . 9 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑆𝐵) → 𝑑 / 𝑘𝑆𝐵)
1510, 13, 14syl2anc 587 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑆𝐵)
16 eqid 2801 . . . . . . . . 9 (𝑘𝐷𝑆) = (𝑘𝐷𝑆)
1716fvmpts 6752 . . . . . . . 8 ((𝑑𝐷𝑑 / 𝑘𝑆𝐵) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
1810, 15, 17syl2anc 587 . . . . . . 7 ((𝜑𝑑𝐷) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
1918eqeq1d 2803 . . . . . 6 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍𝑑 / 𝑘𝑆 = 𝑍))
20 oveq1 7146 . . . . . . . . 9 (𝑑 / 𝑘𝑆 = 𝑍 → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = (𝑍 𝑑 / 𝑘𝑊))
21 mptscmfsupp0.z . . . . . . . . . . . 12 𝑍 = (0g𝑅)
22 mptscmfsupp0.r . . . . . . . . . . . . . 14 (𝜑𝑅 = (Scalar‘𝑄))
2322adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑅 = (Scalar‘𝑄))
2423fveq2d 6653 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → (0g𝑅) = (0g‘(Scalar‘𝑄)))
2521, 24syl5eq 2848 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑍 = (0g‘(Scalar‘𝑄)))
2625oveq1d 7154 . . . . . . . . . 10 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊))
27 mptscmfsupp0.q . . . . . . . . . . . 12 (𝜑𝑄 ∈ LMod)
2827adantr 484 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑄 ∈ LMod)
29 mptscmfsupp0.w . . . . . . . . . . . . . 14 ((𝜑𝑘𝐷) → 𝑊𝐾)
3029ralrimiva 3152 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝐷 𝑊𝐾)
3130adantr 484 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑊𝐾)
32 rspcsbela 4346 . . . . . . . . . . . 12 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑊𝐾) → 𝑑 / 𝑘𝑊𝐾)
3310, 31, 32syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑊𝐾)
34 mptscmfsupp0.k . . . . . . . . . . . 12 𝐾 = (Base‘𝑄)
35 eqid 2801 . . . . . . . . . . . 12 (Scalar‘𝑄) = (Scalar‘𝑄)
36 mptscmfsupp0.m . . . . . . . . . . . 12 = ( ·𝑠𝑄)
37 eqid 2801 . . . . . . . . . . . 12 (0g‘(Scalar‘𝑄)) = (0g‘(Scalar‘𝑄))
3834, 35, 36, 37, 5lmod0vs 19663 . . . . . . . . . . 11 ((𝑄 ∈ LMod ∧ 𝑑 / 𝑘𝑊𝐾) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
3928, 33, 38syl2anc 587 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
4026, 39eqtrd 2836 . . . . . . . . 9 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = 0 )
4120, 40sylan9eqr 2858 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 )
42 csbov12g 7183 . . . . . . . . . . . . . 14 (𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
4342adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
44 ovex 7172 . . . . . . . . . . . . 13 (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) ∈ V
4543, 44eqeltrdi 2901 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) ∈ V)
46 eqid 2801 . . . . . . . . . . . . 13 (𝑘𝐷 ↦ (𝑆 𝑊)) = (𝑘𝐷 ↦ (𝑆 𝑊))
4746fvmpts 6752 . . . . . . . . . . . 12 ((𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
4810, 45, 47syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
4948, 43eqtrd 2836 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
5049eqeq1d 2803 . . . . . . . . 9 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5150adantr 484 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5241, 51mpbird 260 . . . . . . 7 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 )
5352ex 416 . . . . . 6 ((𝜑𝑑𝐷) → (𝑑 / 𝑘𝑆 = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5419, 53sylbid 243 . . . . 5 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5554necon3d 3011 . . . 4 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 → ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍))
5655ss2rabdv 4006 . . 3 (𝜑 → {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 } ⊆ {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
57 ovex 7172 . . . . . 6 (𝑆 𝑊) ∈ V
5857rgenw 3121 . . . . 5 𝑘𝐷 (𝑆 𝑊) ∈ V
5946fnmpt 6464 . . . . 5 (∀𝑘𝐷 (𝑆 𝑊) ∈ V → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
6058, 59mp1i 13 . . . 4 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
61 suppvalfn 7824 . . . 4 (((𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷𝐷𝑉0 ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6260, 1, 7, 61syl3anc 1368 . . 3 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6316fnmpt 6464 . . . . 5 (∀𝑘𝐷 𝑆𝐵 → (𝑘𝐷𝑆) Fn 𝐷)
6412, 63syl 17 . . . 4 (𝜑 → (𝑘𝐷𝑆) Fn 𝐷)
6521fvexi 6663 . . . . 5 𝑍 ∈ V
6665a1i 11 . . . 4 (𝜑𝑍 ∈ V)
67 suppvalfn 7824 . . . 4 (((𝑘𝐷𝑆) Fn 𝐷𝐷𝑉𝑍 ∈ V) → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
6864, 1, 66, 67syl3anc 1368 . . 3 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
6956, 62, 683sstr4d 3965 . 2 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) ⊆ ((𝑘𝐷𝑆) supp 𝑍))
70 suppssfifsupp 8836 . 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 209  wa 399   = wceq 1538  wcel 2112  wne 2990  wral 3109  {crab 3113  Vcvv 3444  csb 3831  wss 3884   class class class wbr 5033  cmpt 5113  Fun wfun 6322   Fn wfn 6323  cfv 6328  (class class class)co 7139   supp csupp 7817  Fincfn 8496   finSupp cfsupp 8821  Basecbs 16478  Scalarcsca 16563   ·𝑠 cvsca 16564  0gc0g 16708  LModclmod 19630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-supp 7818  df-er 8276  df-en 8497  df-fin 8500  df-fsupp 8822  df-0g 16710  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-grp 18101  df-ring 19295  df-lmod 19632
This theorem is referenced by:  mptscmfsuppd  19696  gsumsmonply1  20935  pm2mpcl  21405  mply1topmatcllem  21411  mp2pm2mplem5  21418  pm2mpghmlem2  21420  chcoeffeqlem  21493  lbsdiflsp0  31110  fedgmullem2  31114
  Copyright terms: Public domain W3C validator