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

Theorem tsmsval2 23270
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 23267 . . 3 tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
21a1i 11 . 2 (𝜑 → tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))))
3 vex 3435 . . . . . . 7 𝑓 ∈ V
43dmex 7750 . . . . . 6 dom 𝑓 ∈ V
54pwex 5303 . . . . 5 𝒫 dom 𝑓 ∈ V
65inex1 5241 . . . 4 (𝒫 dom 𝑓 ∩ Fin) ∈ V
76a1i 11 . . 3 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) ∈ V)
8 simplrl 774 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑤 = 𝐺)
98fveq2d 6772 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = (TopOpen‘𝐺))
10 tsmsval.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
119, 10eqtr4di 2796 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = 𝐽)
12 id 22 . . . . . . 7 (𝑠 = (𝒫 dom 𝑓 ∩ Fin) → 𝑠 = (𝒫 dom 𝑓 ∩ Fin))
13 simprr 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → 𝑓 = 𝐹)
1413dmeqd 5809 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝑓 = dom 𝐹)
15 tsmsval2.a . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐴)
1615adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝐹 = 𝐴)
1714, 16eqtrd 2778 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → dom 𝑓 = 𝐴)
1817pweqd 4554 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → 𝒫 dom 𝑓 = 𝒫 𝐴)
1918ineq1d 4147 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = (𝒫 𝐴 ∩ Fin))
20 tsmsval.s . . . . . . . 8 𝑆 = (𝒫 𝐴 ∩ Fin)
2119, 20eqtr4di 2796 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = 𝑆)
2212, 21sylan9eqr 2800 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑠 = 𝑆)
2322rabeqdv 3418 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → {𝑦𝑠𝑧𝑦} = {𝑦𝑆𝑧𝑦})
2422, 23mpteq12dv 5166 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}))
2524rneqd 5842 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = ran (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}))
26 tsmsval.l . . . . . . 7 𝐿 = ran (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦})
2725, 26eqtr4di 2796 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}) = 𝐿)
2822, 27oveq12d 7287 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})) = (𝑆filGen𝐿))
2911, 28oveq12d 7287 . . . 4 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}))) = (𝐽 fLimf (𝑆filGen𝐿)))
30 simplrr 775 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑓 = 𝐹)
3130reseq1d 5885 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑓𝑦) = (𝐹𝑦))
328, 31oveq12d 7287 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑤 Σg (𝑓𝑦)) = (𝐺 Σg (𝐹𝑦)))
3322, 32mpteq12dv 5166 . . . 4 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))) = (𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦))))
3429, 33fveq12d 6775 . . 3 (((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
357, 34csbied 3871 . 2 ((𝜑 ∧ (𝑤 = 𝐺𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
36 tsmsval.g . . 3 (𝜑𝐺𝑉)
3736elexd 3451 . 2 (𝜑𝐺 ∈ V)
38 tsmsval2.f . . 3 (𝜑𝐹𝑊)
3938elexd 3451 . 2 (𝜑𝐹 ∈ V)
40 fvexd 6783 . 2 (𝜑 → ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))) ∈ V)
412, 35, 37, 39, 40ovmpod 7417 1 (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦𝑆 ↦ (𝐺 Σg (𝐹𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wcel 2106  {crab 3068  Vcvv 3431  csb 3833  cin 3887  wss 3888  𝒫 cpw 4535  cmpt 5158  dom cdm 5586  ran crn 5587  cres 5588  cfv 6428  (class class class)co 7269  cmpo 7271  Fincfn 8722  Basecbs 16901  TopOpenctopn 17121   Σg cgsu 17140  filGencfg 20575   fLimf cflf 23075   tsums ctsu 23266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7580
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-iota 6386  df-fun 6430  df-fv 6436  df-ov 7272  df-oprab 7273  df-mpo 7274  df-tsms 23267
This theorem is referenced by:  tsmsval  23271  tsmspropd  23272
  Copyright terms: Public domain W3C validator