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

Theorem tsmsval2 22441
Description: Definition of the topological group sum(s) of a collection 𝐹(𝑥) of values in the group with index set 𝐴. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
tsmsval.b 𝐵 = (Base‘𝐺)
tsmsval.j 𝐽 = (TopOpen‘𝐺)
tsmsval.s 𝑆 = (𝒫 𝐴 ∩ Fin)
tsmsval.l 𝐿 = ran (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦})
tsmsval.g (𝜑𝐺𝑉)
tsmsval2.f (𝜑𝐹𝑊)
tsmsval2.a (𝜑 → dom 𝐹 = 𝐴)
Assertion
Ref Expression
tsmsval2 (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
Distinct variable groups:   𝑦,𝑧,𝐹   𝑦,𝐺,𝑧   𝜑,𝑦,𝑧   𝑦,𝑆
Allowed substitution hints:   𝐴(𝑦,𝑧)   𝐵(𝑦,𝑧)   𝑆(𝑧)   𝐽(𝑦,𝑧)   𝐿(𝑦,𝑧)   𝑉(𝑦,𝑧)   𝑊(𝑦,𝑧)

Proof of Theorem tsmsval2
Dummy variables 𝑓 𝑠 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-tsms 22438 . . 3 tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
21a1i 11 . 2 (𝜑 → tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))))
3 vex 3419 . . . . . . 7 𝑓 ∈ V
43dmex 7431 . . . . . 6 dom 𝑓 ∈ V
54pwex 5134 . . . . 5 𝒫 dom 𝑓 ∈ V
65inex1 5078 . . . 4 (𝒫 dom 𝑓 ∩ Fin) ∈ V
76a1i 11 . . 3 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) ∈ V)
8 simplrl 764 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑤 = 𝐺)
98fveq2d 6503 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = (TopOpen‘𝐺))
10 tsmsval.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
119, 10syl6eqr 2833 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = 𝐽)
12 id 22 . . . . . . 7 (𝑠 = (𝒫 dom 𝑓 ∩ Fin) → 𝑠 = (𝒫 dom 𝑓 ∩ Fin))
13 simprr 760 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → 𝑓 = 𝐹)
1413dmeqd 5624 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝑓 = dom 𝐹)
15 tsmsval2.a . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐴)
1615adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝐹 = 𝐴)
1714, 16eqtrd 2815 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝑓 = 𝐴)
1817pweqd 4427 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → 𝒫 dom 𝑓 = 𝒫 𝐴)
1918ineq1d 4076 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = (𝒫 𝐴 ∩ Fin))
20 tsmsval.s . . . . . . . 8 𝑆 = (𝒫 𝐴 ∩ Fin)
2119, 20syl6eqr 2833 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = 𝑆)
2212, 21sylan9eqr 2837 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑠 = 𝑆)
2322rabeqdv 3408 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → {𝑦𝑠𝑧𝑦} = {𝑦𝑆𝑧𝑦})
2422, 23mpteq12dv 5012 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}))
2524rneqd 5651 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = ran (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}))
26 tsmsval.l . . . . . . 7 𝐿 = ran (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦})
2725, 26syl6eqr 2833 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = 𝐿)
2822, 27oveq12d 6994 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})) = (𝑆filGen𝐿))
2911, 28oveq12d 6994 . . . 4 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}))) = (𝐽 fLimf (𝑆filGen𝐿)))
30 simplrr 765 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑓 = 𝐹)
3130reseq1d 5694 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑓𝑦) = (𝐹𝑦))
328, 31oveq12d 6994 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑤 Σg (𝑓𝑦)) = (𝐺 Σg (𝐹𝑦)))
3322, 32mpteq12dv 5012 . . . 4 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))) = (𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦))))
3429, 33fveq12d 6506 . . 3 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
357, 34csbied 3816 . 2 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
36 tsmsval.g . . 3 (𝜑𝐺𝑉)
3736elexd 3436 . 2 (𝜑𝐺 ∈ V)
38 tsmsval2.f . . 3 (𝜑𝐹𝑊)
3938elexd 3436 . 2 (𝜑𝐹 ∈ V)
40 fvexd 6514 . 2 (𝜑 → ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))) ∈ V)
412, 35, 37, 39, 40ovmpod 7118 1 (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wcel 2050  {crab 3093  Vcvv 3416  csb 3787  cin 3829  wss 3830  𝒫 cpw 4422  cmpt 5008  dom cdm 5407  ran crn 5408  cres 5409  cfv 6188  (class class class)co 6976  cmpo 6978  Fincfn 8306  Basecbs 16339  TopOpenctopn 16551   Σg cgsu 16570  filGencfg 20236   fLimf cflf 22247   tsums ctsu 22437
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 2751  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-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-iota 6152  df-fun 6190  df-fv 6196  df-ov 6979  df-oprab 6980  df-mpo 6981  df-tsms 22438
This theorem is referenced by:  tsmsval  22442  tsmspropd  22443
  Copyright terms: Public domain W3C validator