| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > esumpfinvalf | Structured version Visualization version GIF version | ||
| Description: Same as esumpfinval 34640, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.) |
| Ref | Expression |
|---|---|
| esumpfinvalf.1 | ⊢ Ⅎ𝑘𝐴 |
| esumpfinvalf.2 | ⊢ Ⅎ𝑘𝜑 |
| esumpfinvalf.a | ⊢ (𝜑 → 𝐴 ∈ Fin) |
| esumpfinvalf.b | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
| Ref | Expression |
|---|---|
| esumpfinvalf | ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-esum 34593 | . . . 4 ⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) | |
| 2 | xrge0base 17740 | . . . . . 6 ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | |
| 3 | xrge00 33508 | . . . . . 6 ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | |
| 4 | xrge0cmn 21711 | . . . . . . 7 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | |
| 5 | 4 | a1i 11 | . . . . . 6 ⊢ (𝜑 → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd) |
| 6 | xrge0tps 34507 | . . . . . . 7 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | |
| 7 | 6 | a1i 11 | . . . . . 6 ⊢ (𝜑 → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp) |
| 8 | esumpfinvalf.a | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ Fin) | |
| 9 | esumpfinvalf.2 | . . . . . . 7 ⊢ Ⅎ𝑘𝜑 | |
| 10 | esumpfinvalf.1 | . . . . . . 7 ⊢ Ⅎ𝑘𝐴 | |
| 11 | nfcv 2922 | . . . . . . 7 ⊢ Ⅎ𝑘(0[,]+∞) | |
| 12 | icossicc 13536 | . . . . . . . 8 ⊢ (0[,)+∞) ⊆ (0[,]+∞) | |
| 13 | esumpfinvalf.b | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) | |
| 14 | 12, 13 | sselid 3928 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
| 15 | eqid 2760 | . . . . . . 7 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) | |
| 16 | 9, 10, 11, 14, 15 | fmptdf2 33183 | . . . . . 6 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
| 17 | c0ex 11271 | . . . . . . . 8 ⊢ 0 ∈ V | |
| 18 | 17 | a1i 11 | . . . . . . 7 ⊢ (𝜑 → 0 ∈ V) |
| 19 | 16, 8, 18 | fdmfifsupp 9345 | . . . . . 6 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) finSupp 0) |
| 20 | xrge0topn 34508 | . . . . . . 7 ⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | |
| 21 | 20 | eqcomi 2769 | . . . . . 6 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) |
| 22 | xrhaus 23664 | . . . . . . . 8 ⊢ (ordTop‘ ≤ ) ∈ Haus | |
| 23 | ovex 7441 | . . . . . . . 8 ⊢ (0[,]+∞) ∈ V | |
| 24 | resthaus 23647 | . . . . . . . 8 ⊢ (((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus) | |
| 25 | 22, 23, 24 | mp2an 705 | . . . . . . 7 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus |
| 26 | 25 | a1i 11 | . . . . . 6 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus) |
| 27 | 2, 3, 5, 7, 8, 16, 19, 21, 26 | haustsmsid 24421 | . . . . 5 ⊢ (𝜑 → ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) = {((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))}) |
| 28 | 27 | unieqd 4879 | . . . 4 ⊢ (𝜑 → ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) = ∪ {((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))}) |
| 29 | 1, 28 | eqtrid 2807 | . . 3 ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = ∪ {((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))}) |
| 30 | ovex 7441 | . . . 4 ⊢ ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ V | |
| 31 | 30 | unisn 4885 | . . 3 ⊢ ∪ {((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))} = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) |
| 32 | 29, 31 | eqtrdi 2811 | . 2 ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) |
| 33 | nfcv 2922 | . . . 4 ⊢ Ⅎ𝑘(0[,)+∞) | |
| 34 | 9, 10, 33, 13, 15 | fmptdf2 33183 | . . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,)+∞)) |
| 35 | esumpfinvallem 34639 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,)+∞)) → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | |
| 36 | 8, 34, 35 | syl2anc 596 | . 2 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) |
| 37 | rge0ssre 13556 | . . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ | |
| 38 | ax-resscn 11228 | . . . . . . . 8 ⊢ ℝ ⊆ ℂ | |
| 39 | 37, 38 | sstri 3939 | . . . . . . 7 ⊢ (0[,)+∞) ⊆ ℂ |
| 40 | 39, 13 | sselid 3928 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 41 | 40 | sbt 2103 | . . . . 5 ⊢ [𝑙 / 𝑘]((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 42 | sbim 2336 | . . . . . 6 ⊢ ([𝑙 / 𝑘]((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ([𝑙 / 𝑘](𝜑 ∧ 𝑘 ∈ 𝐴) → [𝑙 / 𝑘]𝐵 ∈ ℂ)) | |
| 43 | sban 2117 | . . . . . . . 8 ⊢ ([𝑙 / 𝑘](𝜑 ∧ 𝑘 ∈ 𝐴) ↔ ([𝑙 / 𝑘]𝜑 ∧ [𝑙 / 𝑘]𝑘 ∈ 𝐴)) | |
| 44 | 9 | sbf 2304 | . . . . . . . . 9 ⊢ ([𝑙 / 𝑘]𝜑 ↔ 𝜑) |
| 45 | 10 | clelsb1fw 2926 | . . . . . . . . 9 ⊢ ([𝑙 / 𝑘]𝑘 ∈ 𝐴 ↔ 𝑙 ∈ 𝐴) |
| 46 | 44, 45 | anbi12i 640 | . . . . . . . 8 ⊢ (([𝑙 / 𝑘]𝜑 ∧ [𝑙 / 𝑘]𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑙 ∈ 𝐴)) |
| 47 | 43, 46 | bitri 278 | . . . . . . 7 ⊢ ([𝑙 / 𝑘](𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑙 ∈ 𝐴)) |
| 48 | sbsbc 3742 | . . . . . . . 8 ⊢ ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ [𝑙 / 𝑘]𝐵 ∈ ℂ) | |
| 49 | sbcel1g 4373 | . . . . . . . . 9 ⊢ (𝑙 ∈ V → ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ)) | |
| 50 | 49 | elv 3455 | . . . . . . . 8 ⊢ ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ) |
| 51 | 48, 50 | bitri 278 | . . . . . . 7 ⊢ ([𝑙 / 𝑘]𝐵 ∈ ℂ ↔ ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ) |
| 52 | 47, 51 | imbi12i 353 | . . . . . 6 ⊢ (([𝑙 / 𝑘](𝜑 ∧ 𝑘 ∈ 𝐴) → [𝑙 / 𝑘]𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑙 ∈ 𝐴) → ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ)) |
| 53 | 42, 52 | bitri 278 | . . . . 5 ⊢ ([𝑙 / 𝑘]((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑙 ∈ 𝐴) → ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ)) |
| 54 | 41, 53 | mpbi 233 | . . . 4 ⊢ ((𝜑 ∧ 𝑙 ∈ 𝐴) → ⦋𝑙 / 𝑘⦌𝐵 ∈ ℂ) |
| 55 | 8, 54 | gsumfsum 21701 | . . 3 ⊢ (𝜑 → (ℂfld Σg (𝑙 ∈ 𝐴 ↦ ⦋𝑙 / 𝑘⦌𝐵)) = Σ𝑙 ∈ 𝐴 ⦋𝑙 / 𝑘⦌𝐵) |
| 56 | nfcv 2922 | . . . . 5 ⊢ Ⅎ𝑙𝐴 | |
| 57 | nfcv 2922 | . . . . 5 ⊢ Ⅎ𝑙𝐵 | |
| 58 | nfcsb1v 3870 | . . . . 5 ⊢ Ⅎ𝑘⦋𝑙 / 𝑘⦌𝐵 | |
| 59 | csbeq1a 3860 | . . . . 5 ⊢ (𝑘 = 𝑙 → 𝐵 = ⦋𝑙 / 𝑘⦌𝐵) | |
| 60 | 10, 56, 57, 58, 59 | cbvmptf 5204 | . . . 4 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑙 ∈ 𝐴 ↦ ⦋𝑙 / 𝑘⦌𝐵) |
| 61 | 60 | oveq2i 7419 | . . 3 ⊢ (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (ℂfld Σg (𝑙 ∈ 𝐴 ↦ ⦋𝑙 / 𝑘⦌𝐵)) |
| 62 | 59, 57, 58 | cbvsum 15829 | . . 3 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑙 ∈ 𝐴 ⦋𝑙 / 𝑘⦌𝐵 |
| 63 | 55, 61, 62 | 3eqtr4g 2820 | . 2 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
| 64 | 32, 36, 63 | 3eqtr2d 2801 | 1 ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 Ⅎwnf 1816 [wsb 2099 ∈ wcel 2145 Ⅎwnfc 2907 Vcvv 3450 [wsbc 3738 ⦋csb 3846 {csn 4583 ∪ cuni 4866 ↦ cmpt 5185 ⟶wf 6523 ‘cfv 6527 (class class class)co 7408 Fincfn 8951 ℂcc 11169 ℝcr 11170 0cc0 11171 +∞cpnf 11311 ≤ cle 11315 [,)cico 13447 [,]cicc 13448 Σcsu 15820 ↾s cress 17369 ↾t crest 17552 TopOpenctopn 17553 Σg cgsu 17572 ordTopcordt 17632 ℝ*𝑠cxrs 17633 CMndccmn 19955 ℂfldccnfld 21639 TopSpctps 23211 Hauscha 23587 tsums ctsu 24406 Σ*cesum 34592 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-inf2 9620 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248 ax-pre-sup 11249 ax-addf 11250 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-fsupp 9332 df-fi 9381 df-sup 9412 df-oi 9482 df-card 9991 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-div 11943 df-nn 12305 df-2 12374 df-3 12375 df-4 12376 df-5 12377 df-6 12378 df-7 12379 df-8 12380 df-9 12381 df-n0 12576 df-z 12663 df-dec 12784 df-uz 12935 df-rp 13090 df-xadd 13211 df-ico 13451 df-icc 13452 df-fz 13609 df-fzo 13757 df-seq 14113 df-exp 14173 df-hash 14442 df-cj 15233 df-re 15234 df-im 15235 df-sqrt 15369 df-abs 15370 df-clim 15622 df-sum 15821 df-struct 17286 df-sets 17303 df-slot 17321 df-ndx 17333 df-base 17349 df-ress 17370 df-plusg 17402 df-mulr 17403 df-starv 17404 df-tset 17408 df-ple 17409 df-ds 17411 df-unif 17412 df-rest 17554 df-topn 17555 df-0g 17573 df-gsum 17574 df-topgen 17575 df-ordt 17634 df-xrs 17635 df-ps 18701 df-tsr 18702 df-mgm 18777 df-sgrp 18869 df-mnd 18885 df-submnd 18940 df-grp 19108 df-minusg 19109 df-cntz 19492 df-cmn 19957 df-abl 19958 df-mgp 20322 df-ur 20369 df-ring 20422 df-cring 20423 df-fbas 21636 df-fg 21637 df-cnfld 21640 df-top 23173 df-topon 23190 df-topsp 23212 df-bases 23225 df-cld 23298 df-ntr 23299 df-cls 23300 df-nei 23377 df-cn 23506 df-haus 23594 df-fil 24126 df-fm 24218 df-flim 24219 df-flf 24220 df-tsms 24407 df-esum 34593 |
| This theorem is used by: volfiniune 34796 |
| Copyright terms: Public domain | W3C validator |