sitgval

Description: Value of the simple function integral builder for a given space W and measure M . (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
Assertion	sitgval	⊢ ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9	7	elexd	⊢ ( 𝜑 → 𝑊 ∈ V )
10		2fveq3	⊢ ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) )
11	2	fveq2i	⊢ ( sigaGen ‘ 𝐽 ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) )
12	3 11	eqtri	⊢ 𝑆 = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) )
13	10 12	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = 𝑆 )
14	13	oveq2d	⊢ ( 𝑤 = 𝑊 → ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) = ( dom 𝑚 MblFnM 𝑆 ) )
15		fveq2	⊢ ( 𝑤 = 𝑊 → ( 0_g ‘ 𝑤 ) = ( 0_g ‘ 𝑊 ) )
16	15 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 0_g ‘ 𝑤 ) = 0 )
17	16	sneqd	⊢ ( 𝑤 = 𝑊 → { ( 0_g ‘ 𝑤 ) } = { 0 } )
18	17	difeq2d	⊢ ( 𝑤 = 𝑊 → ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) = ( ran 𝑔 ∖ { 0 } ) )
19	18	raleqdv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
20	19	anbi2d	⊢ ( 𝑤 = 𝑊 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
21	14 20	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } )
22		id	⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
23	17	difeq2d	⊢ ( 𝑤 = 𝑊 → ( ran 𝑓 ∖ { ( 0_g ‘ 𝑤 ) } ) = ( ran 𝑓 ∖ { 0 } ) )
24		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·_𝑠 ‘ 𝑤 ) = ( ·_𝑠 ‘ 𝑊 ) )
25	24 5	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·_𝑠 ‘ 𝑤 ) = · )
26		2fveq3	⊢ ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) )
27	26 6	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = 𝐻 )
28	27	fveq1d	⊢ ( 𝑤 = 𝑊 → ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) )
29		eqidd	⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
30	25 28 29	oveq123d	⊢ ( 𝑤 = 𝑊 → ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) ( ·_𝑠 ‘ 𝑤 ) 𝑥 ) = ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) )
31	23 30	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0_g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) ( ·_𝑠 ‘ 𝑤 ) 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
32	22 31	oveq12d	⊢ ( 𝑤 = 𝑊 → ( 𝑤 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0_g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) ( ·_𝑠 ‘ 𝑤 ) 𝑥 ) ) ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
33	21 32	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0_g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) ( ·_𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
34		dmeq	⊢ ( 𝑚 = 𝑀 → dom 𝑚 = dom 𝑀 )
35	34	oveq1d	⊢ ( 𝑚 = 𝑀 → ( dom 𝑚 MblFnM 𝑆 ) = ( dom 𝑀 MblFnM 𝑆 ) )
36		fveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) )
37	36	eleq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
38	37	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) )
39	38	anbi2d	⊢ ( 𝑚 = 𝑀 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
40	35 39	rabeqbidv	⊢ ( 𝑚 = 𝑀 → { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } )
41		simpl	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → 𝑚 = 𝑀 )
42	41	fveq1d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) )
43	42	fveq2d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) )
44	43	oveq1d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) )
45	44	mpteq2dva	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) )
46	45	oveq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) )
47	40 46	mpteq12dv	⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
48		df-sitg	⊢ sitg = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0_g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0_g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) ( ·_𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) )
49		ovex	⊢ ( dom 𝑀 MblFnM 𝑆 ) ∈ V
50	49	mptrabex	⊢ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ∈ V
51	33 47 48 50	ovmpo	⊢ ( ( 𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )
52	9 8 51	syl2anc	⊢ ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ^◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ^◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem sitgval

Proof