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

Theorem tsmsmhm 22847
 Description: Apply a continuous group homomorphism to an infinite group sum. (Contributed by Mario Carneiro, 18-Sep-2015.)
Hypotheses
Ref Expression
tsmsmhm.b 𝐵 = (Base‘𝐺)
tsmsmhm.j 𝐽 = (TopOpen‘𝐺)
tsmsmhm.k 𝐾 = (TopOpen‘𝐻)
tsmsmhm.1 (𝜑𝐺 ∈ CMnd)
tsmsmhm.2 (𝜑𝐺 ∈ TopSp)
tsmsmhm.3 (𝜑𝐻 ∈ CMnd)
tsmsmhm.4 (𝜑𝐻 ∈ TopSp)
tsmsmhm.5 (𝜑𝐶 ∈ (𝐺 MndHom 𝐻))
tsmsmhm.6 (𝜑𝐶 ∈ (𝐽 Cn 𝐾))
tsmsmhm.a (𝜑𝐴𝑉)
tsmsmhm.f (𝜑𝐹:𝐴𝐵)
tsmsmhm.x (𝜑𝑋 ∈ (𝐺 tsums 𝐹))
Assertion
Ref Expression
tsmsmhm (𝜑 → (𝐶𝑋) ∈ (𝐻 tsums (𝐶𝐹)))

Proof of Theorem tsmsmhm
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsmhm.2 . . . 4 (𝜑𝐺 ∈ TopSp)
2 tsmsmhm.b . . . . 5 𝐵 = (Base‘𝐺)
3 tsmsmhm.j . . . . 5 𝐽 = (TopOpen‘𝐺)
42, 3istps 21635 . . . 4 (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵))
51, 4sylib 221 . . 3 (𝜑𝐽 ∈ (TopOn‘𝐵))
6 eqid 2759 . . . . 5 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
7 eqid 2759 . . . . 5 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) = (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})
8 eqid 2759 . . . . 5 ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) = ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})
9 tsmsmhm.a . . . . 5 (𝜑𝐴𝑉)
106, 7, 8, 9tsmsfbas 22829 . . . 4 (𝜑 → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)))
11 fgcl 22579 . . . 4 (ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)) → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)))
1210, 11syl 17 . . 3 (𝜑 → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)))
13 tsmsmhm.1 . . . . 5 (𝜑𝐺 ∈ CMnd)
14 tsmsmhm.f . . . . 5 (𝜑𝐹:𝐴𝐵)
152, 6, 13, 9, 14tsmslem1 22830 . . . 4 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑧)) ∈ 𝐵)
1615fmpttd 6871 . . 3 (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))):(𝒫 𝐴 ∩ Fin)⟶𝐵)
17 tsmsmhm.x . . . 4 (𝜑𝑋 ∈ (𝐺 tsums 𝐹))
182, 3, 6, 8, 1, 9, 14tsmsval 22832 . . . 4 (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))))
1917, 18eleqtrd 2855 . . 3 (𝜑𝑋 ∈ ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))))
20 tsmsmhm.6 . . . 4 (𝜑𝐶 ∈ (𝐽 Cn 𝐾))
212, 13, 1, 9, 14tsmscl 22836 . . . . . 6 (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵)
2221, 17sseldd 3894 . . . . 5 (𝜑𝑋𝐵)
23 toponuni 21615 . . . . . 6 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
245, 23syl 17 . . . . 5 (𝜑𝐵 = 𝐽)
2522, 24eleqtrd 2855 . . . 4 (𝜑𝑋 𝐽)
26 eqid 2759 . . . . 5 𝐽 = 𝐽
2726cncnpi 21979 . . . 4 ((𝐶 ∈ (𝐽 Cn 𝐾) ∧ 𝑋 𝐽) → 𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋))
2820, 25, 27syl2anc 588 . . 3 (𝜑𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋))
29 flfcnp 22705 . . 3 (((𝐽 ∈ (TopOn‘𝐵) ∧ ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))):(𝒫 𝐴 ∩ Fin)⟶𝐵) ∧ (𝑋 ∈ ((𝐽 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))) ∧ 𝐶 ∈ ((𝐽 CnP 𝐾)‘𝑋))) → (𝐶𝑋) ∈ ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))))))
305, 12, 16, 19, 28, 29syl32anc 1376 . 2 (𝜑 → (𝐶𝑋) ∈ ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))))))
31 eqid 2759 . . . 4 (Base‘𝐻) = (Base‘𝐻)
32 tsmsmhm.k . . . 4 𝐾 = (TopOpen‘𝐻)
33 tsmsmhm.3 . . . 4 (𝜑𝐻 ∈ CMnd)
34 tsmsmhm.4 . . . . . . 7 (𝜑𝐻 ∈ TopSp)
3531, 32istps 21635 . . . . . . 7 (𝐻 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐻)))
3634, 35sylib 221 . . . . . 6 (𝜑𝐾 ∈ (TopOn‘(Base‘𝐻)))
37 cnf2 21950 . . . . . 6 ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐶 ∈ (𝐽 Cn 𝐾)) → 𝐶:𝐵⟶(Base‘𝐻))
385, 36, 20, 37syl3anc 1369 . . . . 5 (𝜑𝐶:𝐵⟶(Base‘𝐻))
39 fco 6517 . . . . 5 ((𝐶:𝐵⟶(Base‘𝐻) ∧ 𝐹:𝐴𝐵) → (𝐶𝐹):𝐴⟶(Base‘𝐻))
4038, 14, 39syl2anc 588 . . . 4 (𝜑 → (𝐶𝐹):𝐴⟶(Base‘𝐻))
4131, 32, 6, 8, 33, 9, 40tsmsval 22832 . . 3 (𝜑 → (𝐻 tsums (𝐶𝐹)) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶𝐹) ↾ 𝑧)))))
4238, 15cofmpt 6886 . . . . 5 (𝜑 → (𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐶‘(𝐺 Σg (𝐹𝑧)))))
43 resco 6081 . . . . . . . 8 ((𝐶𝐹) ↾ 𝑧) = (𝐶 ∘ (𝐹𝑧))
4443oveq2i 7162 . . . . . . 7 (𝐻 Σg ((𝐶𝐹) ↾ 𝑧)) = (𝐻 Σg (𝐶 ∘ (𝐹𝑧)))
45 eqid 2759 . . . . . . . 8 (0g𝐺) = (0g𝐺)
4613adantr 485 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
4733adantr 485 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ CMnd)
48 cmnmnd 18990 . . . . . . . . 9 (𝐻 ∈ CMnd → 𝐻 ∈ Mnd)
4947, 48syl 17 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ Mnd)
50 elinel2 4102 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin)
5150adantl 486 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin)
52 tsmsmhm.5 . . . . . . . . 9 (𝜑𝐶 ∈ (𝐺 MndHom 𝐻))
5352adantr 485 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐶 ∈ (𝐺 MndHom 𝐻))
54 elfpw 8860 . . . . . . . . . 10 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧𝐴𝑧 ∈ Fin))
5554simplbi 502 . . . . . . . . 9 (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧𝐴)
56 fssres 6530 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧):𝑧𝐵)
5714, 55, 56syl2an 599 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑧):𝑧𝐵)
58 fvexd 6674 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (0g𝐺) ∈ V)
5957, 51, 58fdmfifsupp 8877 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑧) finSupp (0g𝐺))
602, 45, 46, 49, 51, 53, 57, 59gsummhm 19127 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐶 ∘ (𝐹𝑧))) = (𝐶‘(𝐺 Σg (𝐹𝑧))))
6144, 60syl5eq 2806 . . . . . 6 ((𝜑𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg ((𝐶𝐹) ↾ 𝑧)) = (𝐶‘(𝐺 Σg (𝐹𝑧))))
6261mpteq2dva 5128 . . . . 5 (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶𝐹) ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐶‘(𝐺 Σg (𝐹𝑧)))))
6342, 62eqtr4d 2797 . . . 4 (𝜑 → (𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶𝐹) ↾ 𝑧))))
6463fveq2d 6663 . . 3 (𝜑 → ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))))) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐻 Σg ((𝐶𝐹) ↾ 𝑧)))))
6541, 64eqtr4d 2797 . 2 (𝜑 → (𝐻 tsums (𝐶𝐹)) = ((𝐾 fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦𝑧})))‘(𝐶 ∘ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧))))))
6630, 65eleqtrrd 2856 1 (𝜑 → (𝐶𝑋) ∈ (𝐻 tsums (𝐶𝐹)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  {crab 3075  Vcvv 3410   ∩ cin 3858   ⊆ wss 3859  𝒫 cpw 4495  ∪ cuni 4799   ↦ cmpt 5113  ran crn 5526   ↾ cres 5527   ∘ ccom 5529  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151  Fincfn 8528  Basecbs 16542  TopOpenctopn 16754  0gc0g 16772   Σg cgsu 16773  Mndcmnd 17978   MndHom cmhm 18021  CMndccmn 18974  fBascfbas 20155  filGencfg 20156  TopOnctopon 21611  TopSpctps 21633   Cn ccn 21925   CnP ccnp 21926  Filcfil 22546   fLimf cflf 22636   tsums ctsu 22827 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-er 8300  df-map 8419  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8868  df-oi 9008  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-n0 11936  df-z 12022  df-uz 12284  df-fz 12941  df-fzo 13084  df-seq 13420  df-hash 13742  df-0g 16774  df-gsum 16775  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-mhm 18023  df-cntz 18515  df-cmn 18976  df-fbas 20164  df-fg 20165  df-top 21595  df-topon 21612  df-topsp 21634  df-ntr 21721  df-nei 21799  df-cn 21928  df-cnp 21929  df-fil 22547  df-fm 22639  df-flim 22640  df-flf 22641  df-tsms 22828 This theorem is referenced by:  tsmsinv  22849  esumcocn  31568
 Copyright terms: Public domain W3C validator