![]() |
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 31269 | . . 3 ⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | sitgfval 31276 | . 2 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)))) |
13 | rnxpss 5866 | . . . . . . 7 ⊢ ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } | |
14 | ssdif0 4203 | . . . . . . 7 ⊢ (ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } ↔ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅) | |
15 | 13, 14 | mpbi 222 | . . . . . 6 ⊢ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅ |
16 | mpteq1 5011 | . . . . . 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 6317 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ | |
19 | 17, 18 | eqtri 2795 | . . . 4 ⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ |
20 | 19 | oveq2i 6985 | . . 3 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = (𝑊 Σg ∅) |
21 | 4 | gsum0 17758 | . . 3 ⊢ (𝑊 Σg ∅) = 0 |
22 | 20, 21 | eqtri 2795 | . 2 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = 0 |
23 | 12, 22 | syl6eq 2823 | 1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∈ wcel 2051 ∖ cdif 3819 ⊆ wss 3822 ∅c0 4172 {csn 4435 ∪ cuni 4708 ↦ cmpt 5004 × cxp 5401 ◡ccnv 5402 dom cdm 5403 ran crn 5404 “ cima 5406 ‘cfv 6185 (class class class)co 6974 Basecbs 16337 Scalarcsca 16422 ·𝑠 cvsca 16423 TopOpenctopn 16549 0gc0g 16567 Σg cgsu 16568 Mndcmnd 17774 TopSpctps 21259 ℝHomcrrh 30910 sigaGencsigagen 31074 measurescmeas 31131 sitgcsitg 31264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-fal 1521 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-int 4746 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-map 8206 df-en 8305 df-fin 8308 df-seq 13183 df-0g 16569 df-gsum 16570 df-mgm 17722 df-sgrp 17764 df-mnd 17775 df-top 21221 df-topon 21238 df-topsp 21260 df-esum 30963 df-siga 31044 df-sigagen 31075 df-meas 31132 df-mbfm 31186 df-sitg 31265 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |