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 𝐵 = ( 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 )
Assertion sitg0 ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ ( dom 𝑀 × { 0 } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 sitgval.b 𝐵 = ( Base ‘ 𝑊 )
2 sitgval.j 𝐽 = ( TopOpen ‘ 𝑊 )
3 sitgval.s 𝑆 = ( sigaGen ‘ 𝐽 )
4 sitgval.0 0 = ( 0g𝑊 )
5 sitgval.x · = ( ·𝑠𝑊 )
6 sitgval.h 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7 sitgval.1 ( 𝜑𝑊𝑉 )
8 sitgval.2 ( 𝜑𝑀 ran measures )
9 sitg0.1 ( 𝜑𝑊 ∈ TopSp )
10 sitg0.2 ( 𝜑𝑊 ∈ Mnd )
11 1 2 3 4 5 6 7 8 9 10 sibf0 ( 𝜑 → ( dom 𝑀 × { 0 } ) ∈ dom ( 𝑊 sitg 𝑀 ) )
12 1 2 3 4 5 6 7 8 11 sitgfval ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ ( dom 𝑀 × { 0 } ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
13 rnxpss ran ( dom 𝑀 × { 0 } ) ⊆ { 0 }
14 ssdif0 ( ran ( dom 𝑀 × { 0 } ) ⊆ { 0 } ↔ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ )
15 13 14 mpbi ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅
16 mpteq1 ( ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ → ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) )
17 15 16 ax-mp ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) )
18 mpt0 ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ∅
19 17 18 eqtri ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ∅
20 19 oveq2i ( 𝑊 Σg ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σg ∅ )
21 4 gsum0 ( 𝑊 Σg ∅ ) = 0
22 20 21 eqtri ( 𝑊 Σg ( 𝑥 ∈ ( ran ( dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = 0
23 12 22 eqtrdi ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ ( dom 𝑀 × { 0 } ) ) = 0 )