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

Theorem mptscmfsupp0 18694
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 (𝜑𝐷𝑉)
2 mptexg 6364 . . 3 (𝐷𝑉 → (𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V)
31, 2syl 17 . 2 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V)
4 funmpt 5823 . . 3 Fun (𝑘𝐷 ↦ (𝑆 𝑊))
54a1i 11 . 2 (𝜑 → Fun (𝑘𝐷 ↦ (𝑆 𝑊)))
6 mptscmfsupp0.0 . . . 4 0 = (0g𝑄)
7 fvex 6095 . . . 4 (0g𝑄) ∈ V
86, 7eqeltri 2680 . . 3 0 ∈ V
98a1i 11 . 2 (𝜑0 ∈ V)
10 mptscmfsupp0.f . . 3 (𝜑 → (𝑘𝐷𝑆) finSupp 𝑍)
1110fsuppimpd 8139 . 2 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) ∈ Fin)
12 simpr 475 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑𝐷)
13 mptscmfsupp0.s . . . . . . . . . . 11 ((𝜑𝑘𝐷) → 𝑆𝐵)
1413ralrimiva 2945 . . . . . . . . . 10 (𝜑 → ∀𝑘𝐷 𝑆𝐵)
1514adantr 479 . . . . . . . . 9 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑆𝐵)
16 rspcsbela 3954 . . . . . . . . 9 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑆𝐵) → 𝑑 / 𝑘𝑆𝐵)
1712, 15, 16syl2anc 690 . . . . . . . 8 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑆𝐵)
18 eqid 2606 . . . . . . . . 9 (𝑘𝐷𝑆) = (𝑘𝐷𝑆)
1918fvmpts 6176 . . . . . . . 8 ((𝑑𝐷𝑑 / 𝑘𝑆𝐵) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
2012, 17, 19syl2anc 690 . . . . . . 7 ((𝜑𝑑𝐷) → ((𝑘𝐷𝑆)‘𝑑) = 𝑑 / 𝑘𝑆)
2120eqeq1d 2608 . . . . . 6 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍𝑑 / 𝑘𝑆 = 𝑍))
22 oveq1 6531 . . . . . . . . 9 (𝑑 / 𝑘𝑆 = 𝑍 → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = (𝑍 𝑑 / 𝑘𝑊))
23 mptscmfsupp0.z . . . . . . . . . . . 12 𝑍 = (0g𝑅)
24 mptscmfsupp0.r . . . . . . . . . . . . . 14 (𝜑𝑅 = (Scalar‘𝑄))
2524adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑅 = (Scalar‘𝑄))
2625fveq2d 6089 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → (0g𝑅) = (0g‘(Scalar‘𝑄)))
2723, 26syl5eq 2652 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑍 = (0g‘(Scalar‘𝑄)))
2827oveq1d 6539 . . . . . . . . . 10 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊))
29 mptscmfsupp0.q . . . . . . . . . . . 12 (𝜑𝑄 ∈ LMod)
3029adantr 479 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑄 ∈ LMod)
31 mptscmfsupp0.w . . . . . . . . . . . . . 14 ((𝜑𝑘𝐷) → 𝑊𝐾)
3231ralrimiva 2945 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝐷 𝑊𝐾)
3332adantr 479 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → ∀𝑘𝐷 𝑊𝐾)
34 rspcsbela 3954 . . . . . . . . . . . 12 ((𝑑𝐷 ∧ ∀𝑘𝐷 𝑊𝐾) → 𝑑 / 𝑘𝑊𝐾)
3512, 33, 34syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → 𝑑 / 𝑘𝑊𝐾)
36 mptscmfsupp0.k . . . . . . . . . . . 12 𝐾 = (Base‘𝑄)
37 eqid 2606 . . . . . . . . . . . 12 (Scalar‘𝑄) = (Scalar‘𝑄)
38 mptscmfsupp0.m . . . . . . . . . . . 12 = ( ·𝑠𝑄)
39 eqid 2606 . . . . . . . . . . . 12 (0g‘(Scalar‘𝑄)) = (0g‘(Scalar‘𝑄))
4036, 37, 38, 39, 6lmod0vs 18662 . . . . . . . . . . 11 ((𝑄 ∈ LMod ∧ 𝑑 / 𝑘𝑊𝐾) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
4130, 35, 40syl2anc 690 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((0g‘(Scalar‘𝑄)) 𝑑 / 𝑘𝑊) = 0 )
4228, 41eqtrd 2640 . . . . . . . . 9 ((𝜑𝑑𝐷) → (𝑍 𝑑 / 𝑘𝑊) = 0 )
4322, 42sylan9eqr 2662 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 )
44 csbov12g 6562 . . . . . . . . . . . . . 14 (𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
4544adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
46 ovex 6552 . . . . . . . . . . . . 13 (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) ∈ V
4745, 46syl6eqel 2692 . . . . . . . . . . . 12 ((𝜑𝑑𝐷) → 𝑑 / 𝑘(𝑆 𝑊) ∈ V)
48 eqid 2606 . . . . . . . . . . . . 13 (𝑘𝐷 ↦ (𝑆 𝑊)) = (𝑘𝐷 ↦ (𝑆 𝑊))
4948fvmpts 6176 . . . . . . . . . . . 12 ((𝑑𝐷𝑑 / 𝑘(𝑆 𝑊) ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
5012, 47, 49syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 𝑑 / 𝑘(𝑆 𝑊))
5150, 45eqtrd 2640 . . . . . . . . . 10 ((𝜑𝑑𝐷) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊))
5251eqeq1d 2608 . . . . . . . . 9 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5352adantr 479 . . . . . . . 8 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ↔ (𝑑 / 𝑘𝑆 𝑑 / 𝑘𝑊) = 0 ))
5443, 53mpbird 245 . . . . . . 7 (((𝜑𝑑𝐷) ∧ 𝑑 / 𝑘𝑆 = 𝑍) → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 )
5554ex 448 . . . . . 6 ((𝜑𝑑𝐷) → (𝑑 / 𝑘𝑆 = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5621, 55sylbid 228 . . . . 5 ((𝜑𝑑𝐷) → (((𝑘𝐷𝑆)‘𝑑) = 𝑍 → ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) = 0 ))
5756necon3d 2799 . . . 4 ((𝜑𝑑𝐷) → (((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 → ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍))
5857ss2rabdv 3642 . . 3 (𝜑 → {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 } ⊆ {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
59 ovex 6552 . . . . . 6 (𝑆 𝑊) ∈ V
6059rgenw 2904 . . . . 5 𝑘𝐷 (𝑆 𝑊) ∈ V
6148fnmpt 5916 . . . . 5 (∀𝑘𝐷 (𝑆 𝑊) ∈ V → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
6260, 61mp1i 13 . . . 4 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷)
63 suppvalfn 7163 . . . 4 (((𝑘𝐷 ↦ (𝑆 𝑊)) Fn 𝐷𝐷𝑉0 ∈ V) → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6462, 1, 9, 63syl3anc 1317 . . 3 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) = {𝑑𝐷 ∣ ((𝑘𝐷 ↦ (𝑆 𝑊))‘𝑑) ≠ 0 })
6518fnmpt 5916 . . . . 5 (∀𝑘𝐷 𝑆𝐵 → (𝑘𝐷𝑆) Fn 𝐷)
6614, 65syl 17 . . . 4 (𝜑 → (𝑘𝐷𝑆) Fn 𝐷)
67 fvex 6095 . . . . . 6 (0g𝑅) ∈ V
6823, 67eqeltri 2680 . . . . 5 𝑍 ∈ V
6968a1i 11 . . . 4 (𝜑𝑍 ∈ V)
70 suppvalfn 7163 . . . 4 (((𝑘𝐷𝑆) Fn 𝐷𝐷𝑉𝑍 ∈ V) → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
7166, 1, 69, 70syl3anc 1317 . . 3 (𝜑 → ((𝑘𝐷𝑆) supp 𝑍) = {𝑑𝐷 ∣ ((𝑘𝐷𝑆)‘𝑑) ≠ 𝑍})
7258, 64, 713sstr4d 3607 . 2 (𝜑 → ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) ⊆ ((𝑘𝐷𝑆) supp 𝑍))
73 suppssfifsupp 8147 . 2 ((((𝑘𝐷 ↦ (𝑆 𝑊)) ∈ V ∧ Fun (𝑘𝐷 ↦ (𝑆 𝑊)) ∧ 0 ∈ V) ∧ (((𝑘𝐷𝑆) supp 𝑍) ∈ Fin ∧ ((𝑘𝐷 ↦ (𝑆 𝑊)) supp 0 ) ⊆ ((𝑘𝐷𝑆) supp 𝑍))) → (𝑘𝐷 ↦ (𝑆 𝑊)) finSupp 0 )
743, 5, 9, 11, 72, 73syl32anc 1325 1 (𝜑 → (𝑘𝐷 ↦ (𝑆 𝑊)) finSupp 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2776  wral 2892  {crab 2896  Vcvv 3169  csb 3495  wss 3536   class class class wbr 4574  cmpt 4634  Fun wfun 5781   Fn wfn 5782  cfv 5787  (class class class)co 6524   supp csupp 7156  Fincfn 7815   finSupp cfsupp 8132  Basecbs 15638  Scalarcsca 15714   ·𝑠 cvsca 15715  0gc0g 15866  LModclmod 18629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-supp 7157  df-er 7603  df-en 7816  df-fin 7819  df-fsupp 8133  df-0g 15868  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-grp 17191  df-ring 18315  df-lmod 18631
This theorem is referenced by:  mptscmfsuppd  18695  gsumsmonply1  19437  pm2mpcl  20360  mply1topmatcllem  20366  mp2pm2mplem5  20373  pm2mpghmlem2  20375  chcoeffeqlem  20448
  Copyright terms: Public domain W3C validator