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 )