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 = ( sigaGen ` J )
	sitgval.0	|- .0. = ( 0g ` W )
	sitgval.x	|- .x. = ( .s ` W )
	sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
	sitgval.1	|- ( ph -> W e. V )
	sitgval.2	|- ( ph -> M e. U. ran measures )
	sitg0.1	|- ( ph -> W e. TopSp )
	sitg0.2	|- ( ph -> W e. Mnd )
Assertion	sitg0	|- ( ph -> ( ( W sitg M ) ` ( U. dom M X. { .0. } ) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	|- B = ( Base ` W )
2		sitgval.j	|- J = ( TopOpen ` W )
3		sitgval.s	|- S = ( sigaGen ` J )
4		sitgval.0	|- .0. = ( 0g ` W )
5		sitgval.x	|- .x. = ( .s ` W )
6		sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
7		sitgval.1	|- ( ph -> W e. V )
8		sitgval.2	|- ( ph -> M e. U. ran measures )
9		sitg0.1	|- ( ph -> W e. TopSp )
10		sitg0.2	|- ( ph -> W e. Mnd )
11	1 2 3 4 5 6 7 8 9 10	sibf0	|- ( ph -> ( U. dom M X. { .0. } ) e. dom ( W sitg M ) )
12	1 2 3 4 5 6 7 8 11	sitgfval	|- ( ph -> ( ( W sitg M ) ` ( U. dom M X. { .0. } ) ) = ( W gsum ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) ) )
13		rnxpss	|- ran ( U. dom M X. { .0. } ) C_ { .0. }
14		ssdif0	|- ( ran ( U. dom M X. { .0. } ) C_ { .0. } <-> ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/) )
15	13 14	mpbi	|- ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/)
16		mpteq1	|- ( ( ran ( U. dom M X. { .0. } ) \ { .0. } ) = (/) -> ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) = ( x e. (/) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) )
17	15 16	ax-mp	|- ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) = ( x e. (/) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) )
18		mpt0	|- ( x e. (/) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) = (/)
19	17 18	eqtri	|- ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) = (/)
20	19	oveq2i	|- ( W gsum ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) ) = ( W gsum (/) )
21	4	gsum0	|- ( W gsum (/) ) = .0.
22	20 21	eqtri	|- ( W gsum ( x e. ( ran ( U. dom M X. { .0. } ) \ { .0. } ) |-> ( ( H ` ( M ` ( `' ( U. dom M X. { .0. } ) " { x } ) ) ) .x. x ) ) ) = .0.
23	12 22	eqtrdi	|- ( ph -> ( ( W sitg M ) ` ( U. dom M X. { .0. } ) ) = .0. )