Metamath Proof Explorer


Theorem sitg0

Description: The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Hypotheses sitgval.b B=BaseW
sitgval.j J=TopOpenW
sitgval.s S=𝛔J
sitgval.0 0˙=0W
sitgval.x ·˙=W
sitgval.h H=ℝHomScalarW
sitgval.1 φWV
sitgval.2 φMranmeasures
sitg0.1 φWTopSp
sitg0.2 φWMnd
Assertion sitg0 φWdomM×0˙dM=0˙

Proof

Step Hyp Ref Expression
1 sitgval.b B=BaseW
2 sitgval.j J=TopOpenW
3 sitgval.s S=𝛔J
4 sitgval.0 0˙=0W
5 sitgval.x ·˙=W
6 sitgval.h H=ℝHomScalarW
7 sitgval.1 φWV
8 sitgval.2 φMranmeasures
9 sitg0.1 φWTopSp
10 sitg0.2 φWMnd
11 1 2 3 4 5 6 7 8 9 10 sibf0 φdomM×0˙MW
12 1 2 3 4 5 6 7 8 11 sitgfval φWdomM×0˙dM=WxrandomM×0˙0˙HMdomM×0˙-1x·˙x
13 rnxpss randomM×0˙0˙
14 ssdif0 randomM×0˙0˙randomM×0˙0˙=
15 13 14 mpbi randomM×0˙0˙=
16 mpteq1 randomM×0˙0˙=xrandomM×0˙0˙HMdomM×0˙-1x·˙x=xHMdomM×0˙-1x·˙x
17 15 16 ax-mp xrandomM×0˙0˙HMdomM×0˙-1x·˙x=xHMdomM×0˙-1x·˙x
18 mpt0 xHMdomM×0˙-1x·˙x=
19 17 18 eqtri xrandomM×0˙0˙HMdomM×0˙-1x·˙x=
20 19 oveq2i WxrandomM×0˙0˙HMdomM×0˙-1x·˙x=W
21 4 gsum0 W=0˙
22 20 21 eqtri WxrandomM×0˙0˙HMdomM×0˙-1x·˙x=0˙
23 12 22 eqtrdi φWdomM×0˙dM=0˙