Theorem sibf0

Description: The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-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 )
	sibf0.1	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
	sibf0.2	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
Assertion	sibf0	⊢ ( 𝜑 → ( ∪ dom 𝑀 × { 0 } ) ∈ dom ( 𝑊 sitg 𝑀 ) )

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		sibf0.1	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
10		sibf0.2	⊢ ( 𝜑 → 𝑊 ∈ Mnd )
11		dmmeas	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra )
12	8 11	syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
13	2	fvexi	⊢ 𝐽 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝐽 ∈ V )
15	14	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
16	3 15	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
17		fconstmpt	⊢ ( ∪ dom 𝑀 × { 0 } ) = ( 𝑥 ∈ ∪ dom 𝑀 ↦ 0 )
18	17	a1i	⊢ ( 𝜑 → ( ∪ dom 𝑀 × { 0 } ) = ( 𝑥 ∈ ∪ dom 𝑀 ↦ 0 ) )
19	1 4	mndidcl	⊢ ( 𝑊 ∈ Mnd → 0 ∈ 𝐵 )
20	10 19	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
21	1 2	tpsuni	⊢ ( 𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽 )
22	9 21	syl	⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
23	3	unieqi	⊢ ∪ 𝑆 = ∪ ( sigaGen ‘ 𝐽 )
24		unisg	⊢ ( 𝐽 ∈ V → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
25	13 24	mp1i	⊢ ( 𝜑 → ∪ ( sigaGen ‘ 𝐽 ) = ∪ 𝐽 )
26	23 25	syl5eq	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐽 )
27	22 26	eqtr4d	⊢ ( 𝜑 → 𝐵 = ∪ 𝑆 )
28	20 27	eleqtrd	⊢ ( 𝜑 → 0 ∈ ∪ 𝑆 )
29	12 16 18 28	mbfmcst	⊢ ( 𝜑 → ( ∪ dom 𝑀 × { 0 } ) ∈ ( dom 𝑀 MblFnM 𝑆 ) )
30		xpeq1	⊢ ( ∪ dom 𝑀 = ∅ → ( ∪ dom 𝑀 × { 0 } ) = ( ∅ × { 0 } ) )
31		0xp	⊢ ( ∅ × { 0 } ) = ∅
32	30 31	eqtrdi	⊢ ( ∪ dom 𝑀 = ∅ → ( ∪ dom 𝑀 × { 0 } ) = ∅ )
33	32	rneqd	⊢ ( ∪ dom 𝑀 = ∅ → ran ( ∪ dom 𝑀 × { 0 } ) = ran ∅ )
34		rn0	⊢ ran ∅ = ∅
35	33 34	eqtrdi	⊢ ( ∪ dom 𝑀 = ∅ → ran ( ∪ dom 𝑀 × { 0 } ) = ∅ )
36		0fin	⊢ ∅ ∈ Fin
37	35 36	eqeltrdi	⊢ ( ∪ dom 𝑀 = ∅ → ran ( ∪ dom 𝑀 × { 0 } ) ∈ Fin )
38		rnxp	⊢ ( ∪ dom 𝑀 ≠ ∅ → ran ( ∪ dom 𝑀 × { 0 } ) = { 0 } )
39		snfi	⊢ { 0 } ∈ Fin
40	38 39	eqeltrdi	⊢ ( ∪ dom 𝑀 ≠ ∅ → ran ( ∪ dom 𝑀 × { 0 } ) ∈ Fin )
41	37 40	pm2.61ine	⊢ ran ( ∪ dom 𝑀 × { 0 } ) ∈ Fin
42	41	a1i	⊢ ( 𝜑 → ran ( ∪ dom 𝑀 × { 0 } ) ∈ Fin )
43		noel	⊢ ¬ 𝑥 ∈ ∅
44	35	difeq1d	⊢ ( ∪ dom 𝑀 = ∅ → ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ( ∅ ∖ { 0 } ) )
45		0dif	⊢ ( ∅ ∖ { 0 } ) = ∅
46	44 45	eqtrdi	⊢ ( ∪ dom 𝑀 = ∅ → ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ )
47	38	difeq1d	⊢ ( ∪ dom 𝑀 ≠ ∅ → ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ( { 0 } ∖ { 0 } ) )
48		difid	⊢ ( { 0 } ∖ { 0 } ) = ∅
49	47 48	eqtrdi	⊢ ( ∪ dom 𝑀 ≠ ∅ → ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ )
50	46 49	pm2.61ine	⊢ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅
51	50	eleq2i	⊢ ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↔ 𝑥 ∈ ∅ )
52	43 51	mtbir	⊢ ¬ 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } )
53	52	pm2.21i	⊢ ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) → ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
54	53	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ) → ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
55	54	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) )
56	1 2 3 4 5 6 7 8	issibf	⊢ ( 𝜑 → ( ( ∪ dom 𝑀 × { 0 } ) ∈ dom ( 𝑊 sitg 𝑀 ) ↔ ( ( ∪ dom 𝑀 × { 0 } ) ∈ ( dom 𝑀 MblFnM 𝑆 ) ∧ ran ( ∪ dom 𝑀 × { 0 } ) ∈ Fin ∧ ∀ 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
57	29 42 55 56	mpbir3and	⊢ ( 𝜑 → ( ∪ dom 𝑀 × { 0 } ) ∈ dom ( 𝑊 sitg 𝑀 ) )