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 = Base W
sitgval.j J = TopOpen W
sitgval.s S = 𝛔 J
sitgval.0 0 ˙ = 0 W
sitgval.x · ˙ = W
sitgval.h H = ℝHom Scalar W
sitgval.1 φ W V
sitgval.2 φ M ran measures
sitg0.1 φ W TopSp
sitg0.2 φ W Mnd
Assertion sitg0 φ W dom M × 0 ˙ dM = 0 ˙

Proof

Step Hyp Ref Expression
1 sitgval.b B = Base W
2 sitgval.j J = TopOpen W
3 sitgval.s S = 𝛔 J
4 sitgval.0 0 ˙ = 0 W
5 sitgval.x · ˙ = W
6 sitgval.h H = ℝHom Scalar W
7 sitgval.1 φ W V
8 sitgval.2 φ M ran measures
9 sitg0.1 φ W TopSp
10 sitg0.2 φ W Mnd
11 1 2 3 4 5 6 7 8 9 10 sibf0 φ dom M × 0 ˙ M W
12 1 2 3 4 5 6 7 8 11 sitgfval φ W dom M × 0 ˙ dM = W x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x
13 rnxpss ran dom M × 0 ˙ 0 ˙
14 ssdif0 ran dom M × 0 ˙ 0 ˙ ran dom M × 0 ˙ 0 ˙ =
15 13 14 mpbi ran dom M × 0 ˙ 0 ˙ =
16 mpteq1 ran dom M × 0 ˙ 0 ˙ = x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x = x H M dom M × 0 ˙ -1 x · ˙ x
17 15 16 ax-mp x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x = x H M dom M × 0 ˙ -1 x · ˙ x
18 mpt0 x H M dom M × 0 ˙ -1 x · ˙ x =
19 17 18 eqtri x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x =
20 19 oveq2i W x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x = W
21 4 gsum0 W = 0 ˙
22 20 21 eqtri W x ran dom M × 0 ˙ 0 ˙ H M dom M × 0 ˙ -1 x · ˙ x = 0 ˙
23 12 22 eqtrdi φ W dom M × 0 ˙ dM = 0 ˙