Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > sitg0 | Structured version Visualization version GIF version |
Description: The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
Ref | Expression |
---|---|
sitgval.b | ⊢ 𝐵 = (Base‘𝑊) |
sitgval.j | ⊢ 𝐽 = (TopOpen‘𝑊) |
sitgval.s | ⊢ 𝑆 = (sigaGen‘𝐽) |
sitgval.0 | ⊢ 0 = (0g‘𝑊) |
sitgval.x | ⊢ · = ( ·𝑠 ‘𝑊) |
sitgval.h | ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) |
sitgval.1 | ⊢ (𝜑 → 𝑊 ∈ 𝑉) |
sitgval.2 | ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) |
sitg0.1 | ⊢ (𝜑 → 𝑊 ∈ TopSp) |
sitg0.2 | ⊢ (𝜑 → 𝑊 ∈ Mnd) |
Ref | Expression |
---|---|
sitg0 | ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sitgval.b | . . 3 ⊢ 𝐵 = (Base‘𝑊) | |
2 | sitgval.j | . . 3 ⊢ 𝐽 = (TopOpen‘𝑊) | |
3 | sitgval.s | . . 3 ⊢ 𝑆 = (sigaGen‘𝐽) | |
4 | sitgval.0 | . . 3 ⊢ 0 = (0g‘𝑊) | |
5 | sitgval.x | . . 3 ⊢ · = ( ·𝑠 ‘𝑊) | |
6 | sitgval.h | . . 3 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊)) | |
7 | sitgval.1 | . . 3 ⊢ (𝜑 → 𝑊 ∈ 𝑉) | |
8 | sitgval.2 | . . 3 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures) | |
9 | sitg0.1 | . . . 4 ⊢ (𝜑 → 𝑊 ∈ TopSp) | |
10 | sitg0.2 | . . . 4 ⊢ (𝜑 → 𝑊 ∈ Mnd) | |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | sibf0 31824 | . . 3 ⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | sitgfval 31831 | . 2 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)))) |
13 | rnxpss 6005 | . . . . . . 7 ⊢ ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } | |
14 | ssdif0 4264 | . . . . . . 7 ⊢ (ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } ↔ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅) | |
15 | 13, 14 | mpbi 233 | . . . . . 6 ⊢ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅ |
16 | mpteq1 5123 | . . . . . 6 ⊢ ((ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅ → (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = (𝑥 ∈ ∅ ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) | |
17 | 15, 16 | ax-mp 5 | . . . . 5 ⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = (𝑥 ∈ ∅ ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) |
18 | mpt0 6477 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ | |
19 | 17, 18 | eqtri 2781 | . . . 4 ⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ |
20 | 19 | oveq2i 7166 | . . 3 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = (𝑊 Σg ∅) |
21 | 4 | gsum0 17965 | . . 3 ⊢ (𝑊 Σg ∅) = 0 |
22 | 20, 21 | eqtri 2781 | . 2 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = 0 |
23 | 12, 22 | eqtrdi 2809 | 1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 ∖ cdif 3857 ⊆ wss 3860 ∅c0 4227 {csn 4525 ∪ cuni 4801 ↦ cmpt 5115 × cxp 5525 ◡ccnv 5526 dom cdm 5527 ran crn 5528 “ cima 5530 ‘cfv 6339 (class class class)co 7155 Basecbs 16546 Scalarcsca 16631 ·𝑠 cvsca 16632 TopOpenctopn 16758 0gc0g 16776 Σg cgsu 16777 Mndcmnd 17982 TopSpctps 21637 ℝHomcrrh 31466 sigaGencsigagen 31629 measurescmeas 31686 sitgcsitg 31819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7585 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-1o 8117 df-map 8423 df-en 8533 df-fin 8536 df-seq 13424 df-0g 16778 df-gsum 16779 df-mgm 17923 df-sgrp 17972 df-mnd 17983 df-top 21599 df-topon 21616 df-topsp 21638 df-esum 31519 df-siga 31600 df-sigagen 31630 df-meas 31687 df-mbfm 31741 df-sitg 31820 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |