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 32346 | . . 3 ⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | sitgfval 32353 | . 2 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)))) |
13 | rnxpss 6090 | . . . . . . 7 ⊢ ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } | |
14 | ssdif0 4303 | . . . . . . 7 ⊢ (ran (∪ dom 𝑀 × { 0 }) ⊆ { 0 } ↔ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅) | |
15 | 13, 14 | mpbi 229 | . . . . . 6 ⊢ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ∅ |
16 | mpteq1 5174 | . . . . . 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 6605 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ | |
19 | 17, 18 | eqtri 2764 | . . . 4 ⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥)) = ∅ |
20 | 19 | oveq2i 7318 | . . 3 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = (𝑊 Σg ∅) |
21 | 4 | gsum0 18413 | . . 3 ⊢ (𝑊 Σg ∅) = 0 |
22 | 20, 21 | eqtri 2764 | . 2 ⊢ (𝑊 Σg (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥}))) · 𝑥))) = 0 |
23 | 12, 22 | eqtrdi 2792 | 1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘(∪ dom 𝑀 × { 0 })) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2104 ∖ cdif 3889 ⊆ wss 3892 ∅c0 4262 {csn 4565 ∪ cuni 4844 ↦ cmpt 5164 × cxp 5598 ◡ccnv 5599 dom cdm 5600 ran crn 5601 “ cima 5603 ‘cfv 6458 (class class class)co 7307 Basecbs 16957 Scalarcsca 17010 ·𝑠 cvsca 17011 TopOpenctopn 17177 0gc0g 17195 Σg cgsu 17196 Mndcmnd 18430 TopSpctps 22126 ℝHomcrrh 31988 sigaGencsigagen 32151 measurescmeas 32208 sitgcsitg 32341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-int 4887 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-om 7745 df-frecs 8128 df-wrecs 8159 df-recs 8233 df-rdg 8272 df-1o 8328 df-map 8648 df-en 8765 df-fin 8768 df-seq 13768 df-0g 17197 df-gsum 17198 df-mgm 18371 df-sgrp 18420 df-mnd 18431 df-top 22088 df-topon 22105 df-topsp 22127 df-esum 32041 df-siga 32122 df-sigagen 32152 df-meas 32209 df-mbfm 32263 df-sitg 32342 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |