Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumpfinvalf Structured version   Visualization version   GIF version

Theorem esumpfinvalf 31343
 Description: Same as esumpfinval 31342, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.)
Hypotheses
Ref Expression
esumpfinvalf.1 𝑘𝐴
esumpfinvalf.2 𝑘𝜑
esumpfinvalf.a (𝜑𝐴 ∈ Fin)
esumpfinvalf.b ((𝜑𝑘𝐴) → 𝐵 ∈ (0[,)+∞))
Assertion
Ref Expression
esumpfinvalf (𝜑 → Σ*𝑘𝐴𝐵 = Σ𝑘𝐴 𝐵)

Proof of Theorem esumpfinvalf
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 df-esum 31295 . . . 4 Σ*𝑘𝐴𝐵 = ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
2 xrge0base 30680 . . . . . 6 (0[,]+∞) = (Base‘(ℝ*𝑠s (0[,]+∞)))
3 xrge00 30681 . . . . . 6 0 = (0g‘(ℝ*𝑠s (0[,]+∞)))
4 xrge0cmn 20563 . . . . . . 7 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
54a1i 11 . . . . . 6 (𝜑 → (ℝ*𝑠s (0[,]+∞)) ∈ CMnd)
6 xrge0tps 31193 . . . . . . 7 (ℝ*𝑠s (0[,]+∞)) ∈ TopSp
76a1i 11 . . . . . 6 (𝜑 → (ℝ*𝑠s (0[,]+∞)) ∈ TopSp)
8 esumpfinvalf.a . . . . . 6 (𝜑𝐴 ∈ Fin)
9 esumpfinvalf.2 . . . . . . 7 𝑘𝜑
10 esumpfinvalf.1 . . . . . . 7 𝑘𝐴
11 nfcv 2973 . . . . . . 7 𝑘(0[,]+∞)
12 icossicc 12805 . . . . . . . 8 (0[,)+∞) ⊆ (0[,]+∞)
13 esumpfinvalf.b . . . . . . . 8 ((𝜑𝑘𝐴) → 𝐵 ∈ (0[,)+∞))
1412, 13sseldi 3944 . . . . . . 7 ((𝜑𝑘𝐴) → 𝐵 ∈ (0[,]+∞))
15 eqid 2820 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
169, 10, 11, 14, 15fmptdF 30388 . . . . . 6 (𝜑 → (𝑘𝐴𝐵):𝐴⟶(0[,]+∞))
17 c0ex 10613 . . . . . . . 8 0 ∈ V
1817a1i 11 . . . . . . 7 (𝜑 → 0 ∈ V)
1916, 8, 18fdmfifsupp 8821 . . . . . 6 (𝜑 → (𝑘𝐴𝐵) finSupp 0)
20 xrge0topn 31194 . . . . . . 7 (TopOpen‘(ℝ*𝑠s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
2120eqcomi 2829 . . . . . 6 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘(ℝ*𝑠s (0[,]+∞)))
22 xrhaus 21969 . . . . . . . 8 (ordTop‘ ≤ ) ∈ Haus
23 ovex 7166 . . . . . . . 8 (0[,]+∞) ∈ V
24 resthaus 21952 . . . . . . . 8 (((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
2522, 23, 24mp2an 690 . . . . . . 7 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus
2625a1i 11 . . . . . 6 (𝜑 → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
272, 3, 5, 7, 8, 16, 19, 21, 26haustsmsid 22725 . . . . 5 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵)) = {((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))})
2827unieqd 4828 . . . 4 (𝜑 ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵)) = {((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))})
291, 28syl5eq 2867 . . 3 (𝜑 → Σ*𝑘𝐴𝐵 = {((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))})
30 ovex 7166 . . . 4 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ V
3130unisn 4834 . . 3 {((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))} = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))
3229, 31syl6eq 2871 . 2 (𝜑 → Σ*𝑘𝐴𝐵 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
33 nfcv 2973 . . . 4 𝑘(0[,)+∞)
349, 10, 33, 13, 15fmptdF 30388 . . 3 (𝜑 → (𝑘𝐴𝐵):𝐴⟶(0[,)+∞))
35 esumpfinvallem 31341 . . 3 ((𝐴 ∈ Fin ∧ (𝑘𝐴𝐵):𝐴⟶(0[,)+∞)) → (ℂfld Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
368, 34, 35syl2anc 586 . 2 (𝜑 → (ℂfld Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
37 rge0ssre 12825 . . . . . . . 8 (0[,)+∞) ⊆ ℝ
38 ax-resscn 10572 . . . . . . . 8 ℝ ⊆ ℂ
3937, 38sstri 3955 . . . . . . 7 (0[,)+∞) ⊆ ℂ
4039, 13sseldi 3944 . . . . . 6 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
4140sbt 2071 . . . . 5 [𝑙 / 𝑘]((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
42 sbim 2311 . . . . . 6 ([𝑙 / 𝑘]((𝜑𝑘𝐴) → 𝐵 ∈ ℂ) ↔ ([𝑙 / 𝑘](𝜑𝑘𝐴) → [𝑙 / 𝑘]𝐵 ∈ ℂ))
43 sban 2086 . . . . . . . 8 ([𝑙 / 𝑘](𝜑𝑘𝐴) ↔ ([𝑙 / 𝑘]𝜑 ∧ [𝑙 / 𝑘]𝑘𝐴))
449sbf 2271 . . . . . . . . 9 ([𝑙 / 𝑘]𝜑𝜑)
4510clelsb3fw 2977 . . . . . . . . 9 ([𝑙 / 𝑘]𝑘𝐴𝑙𝐴)
4644, 45anbi12i 628 . . . . . . . 8 (([𝑙 / 𝑘]𝜑 ∧ [𝑙 / 𝑘]𝑘𝐴) ↔ (𝜑𝑙𝐴))
4743, 46bitri 277 . . . . . . 7 ([𝑙 / 𝑘](𝜑𝑘𝐴) ↔ (𝜑𝑙𝐴))
48 sbsbc 3756 . . . . . . . 8 ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ [𝑙 / 𝑘]𝐵 ∈ ℂ)
49 sbcel1g 4341 . . . . . . . . 9 (𝑙 ∈ V → ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ 𝑙 / 𝑘𝐵 ∈ ℂ))
5049elv 3478 . . . . . . . 8 ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ 𝑙 / 𝑘𝐵 ∈ ℂ)
5148, 50bitri 277 . . . . . . 7 ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ 𝑙 / 𝑘𝐵 ∈ ℂ)
5247, 51imbi12i 353 . . . . . 6 (([𝑙 / 𝑘](𝜑𝑘𝐴) → [𝑙 / 𝑘]𝐵 ∈ ℂ) ↔ ((𝜑𝑙𝐴) → 𝑙 / 𝑘𝐵 ∈ ℂ))
5342, 52bitri 277 . . . . 5 ([𝑙 / 𝑘]((𝜑𝑘𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑𝑙𝐴) → 𝑙 / 𝑘𝐵 ∈ ℂ))
5441, 53mpbi 232 . . . 4 ((𝜑𝑙𝐴) → 𝑙 / 𝑘𝐵 ∈ ℂ)
558, 54gsumfsum 20588 . . 3 (𝜑 → (ℂfld Σg (𝑙𝐴𝑙 / 𝑘𝐵)) = Σ𝑙𝐴 𝑙 / 𝑘𝐵)
56 nfcv 2973 . . . . 5 𝑙𝐴
57 nfcv 2973 . . . . 5 𝑙𝐵
58 nfcsb1v 3884 . . . . 5 𝑘𝑙 / 𝑘𝐵
59 csbeq1a 3874 . . . . 5 (𝑘 = 𝑙𝐵 = 𝑙 / 𝑘𝐵)
6010, 56, 57, 58, 59cbvmptf 5141 . . . 4 (𝑘𝐴𝐵) = (𝑙𝐴𝑙 / 𝑘𝐵)
6160oveq2i 7144 . . 3 (ℂfld Σg (𝑘𝐴𝐵)) = (ℂfld Σg (𝑙𝐴𝑙 / 𝑘𝐵))
6259, 56, 10, 57, 58cbvsum 15032 . . 3 Σ𝑘𝐴 𝐵 = Σ𝑙𝐴 𝑙 / 𝑘𝐵
6355, 61, 623eqtr4g 2880 . 2 (𝜑 → (ℂfld Σg (𝑘𝐴𝐵)) = Σ𝑘𝐴 𝐵)
6432, 36, 633eqtr2d 2861 1 (𝜑 → Σ*𝑘𝐴𝐵 = Σ𝑘𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  Ⅎwnf 1784  [wsb 2069   ∈ wcel 2114  Ⅎwnfc 2957  Vcvv 3473  [wsbc 3752  ⦋csb 3860  {csn 4543  ∪ cuni 4814   ↦ cmpt 5122  ⟶wf 6327  ‘cfv 6331  (class class class)co 7133  Fincfn 8487  ℂcc 10513  ℝcr 10514  0cc0 10515  +∞cpnf 10650   ≤ cle 10654  [,)cico 12719  [,]cicc 12720  Σcsu 15022   ↾s cress 16463   ↾t crest 16673  TopOpenctopn 16674   Σg cgsu 16693  ordTopcordt 16751  ℝ*𝑠cxrs 16752  CMndccmn 18885  ℂfldccnfld 20521  TopSpctps 21516  Hauscha 21892   tsums ctsu 22710  Σ*cesum 31294 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593  ax-addf 10594  ax-mulf 10595 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-iin 4898  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-supp 7809  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-fsupp 8812  df-fi 8853  df-sup 8884  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-4 11681  df-5 11682  df-6 11683  df-7 11684  df-8 11685  df-9 11686  df-n0 11877  df-z 11961  df-dec 12078  df-uz 12223  df-rp 12369  df-xadd 12487  df-ico 12723  df-icc 12724  df-fz 12877  df-fzo 13018  df-seq 13354  df-exp 13415  df-hash 13676  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-clim 14825  df-sum 15023  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-mulr 16558  df-starv 16559  df-tset 16563  df-ple 16564  df-ds 16566  df-unif 16567  df-rest 16675  df-topn 16676  df-0g 16694  df-gsum 16695  df-topgen 16696  df-ordt 16753  df-xrs 16754  df-ps 17789  df-tsr 17790  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-grp 18085  df-minusg 18086  df-cntz 18426  df-cmn 18887  df-abl 18888  df-mgp 19219  df-ur 19231  df-ring 19278  df-cring 19279  df-fbas 20518  df-fg 20519  df-cnfld 20522  df-top 21478  df-topon 21495  df-topsp 21517  df-bases 21530  df-cld 21603  df-ntr 21604  df-cls 21605  df-nei 21682  df-cn 21811  df-haus 21899  df-fil 22430  df-fm 22522  df-flim 22523  df-flf 22524  df-tsms 22711  df-esum 31295 This theorem is referenced by:  volfiniune  31497
 Copyright terms: Public domain W3C validator