Theorem sitgval 32932

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

Hypotheses

Ref	Expression
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)

Assertion

Ref	Expression
sitgval	⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))

Distinct variable groups:   𝐵,𝑓   𝑓,𝑔,𝑥   𝑓,𝐻   𝑓,𝑀,𝑔,𝑥   𝑆,𝑓,𝑔   𝑓,𝑊,𝑔,𝑥   0 ,𝑓,𝑔,𝑥   · ,𝑓

Allowed substitution hints:   𝜑(𝑥,𝑓,𝑔)   𝐵(𝑥,𝑔)   𝑆(𝑥)   · (𝑥,𝑔)   𝐻(𝑥,𝑔)   𝐽(𝑥,𝑓,𝑔)   𝑉(𝑥,𝑓,𝑔)

Proof of Theorem sitgval

Dummy variables 𝑚 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sitgval.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ 𝑉)
2	1	elexd 3465	. 2 ⊢ (𝜑 → 𝑊 ∈ V)
3		sitgval.2	. 2 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4		2fveq3 6847	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = (sigaGen‘(TopOpen‘𝑊)))
5		sitgval.s	. . . . . . . 8 ⊢ 𝑆 = (sigaGen‘𝐽)
6		sitgval.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝑊)
7	6	fveq2i 6845	. . . . . . . 8 ⊢ (sigaGen‘𝐽) = (sigaGen‘(TopOpen‘𝑊))
8	5, 7	eqtri 2764	. . . . . . 7 ⊢ 𝑆 = (sigaGen‘(TopOpen‘𝑊))
9	4, 8	eqtr4di 2794	. . . . . 6 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆)
10	9	oveq2d 7373	. . . . 5 ⊢ (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆))
11		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊))
12		sitgval.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝑊)
13	11, 12	eqtr4di 2794	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 )
14	13	sneqd 4598	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 })
15	14	difeq2d 4082	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g‘𝑤)}) = (ran 𝑔 ∖ { 0 }))
16	15	raleqdv 3313	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
17	16	anbi2d 629	. . . . 5 ⊢ (𝑤 = 𝑊 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
18	10, 17	rabeqbidv 3424	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
19		id 22	. . . . 5 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
20	14	difeq2d 4082	. . . . . 6 ⊢ (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g‘𝑤)}) = (ran 𝑓 ∖ { 0 }))
21		fveq2 6842	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
22		sitgval.x	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
23	21, 22	eqtr4di 2794	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
24		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊)))
25		sitgval.h	. . . . . . . . 9 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
26	24, 25	eqtr4di 2794	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = 𝐻)
27	26	fveq1d 6844	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))))
28		eqidd 2737	. . . . . . 7 ⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥)
29	23, 27, 28	oveq123d 7378	. . . . . 6 ⊢ (𝑤 = 𝑊 → (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥) = ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))
30	20, 29	mpteq12dv 5196	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))
31	19, 30	oveq12d 7375	. . . 4 ⊢ (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))))
32	18, 31	mpteq12dv 5196	. . 3 ⊢ (𝑤 = 𝑊 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
33		dmeq 5859	. . . . . 6 ⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀)
34	33	oveq1d 7372	. . . . 5 ⊢ (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35		fveq1 6841	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (𝑚‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝑔 “ {𝑥})))
36	35	eleq1d 2822	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
37	36	ralbidv 3174	. . . . . 6 ⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
38	37	anbi2d 629	. . . . 5 ⊢ (𝑚 = 𝑀 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
39	34, 38	rabeqbidv 3424	. . . 4 ⊢ (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
40		simpl 483	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀)
41	40	fveq1d 6844	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝑓 “ {𝑥})))
42	41	fveq2d 6846	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))))
43	42	oveq1d 7372	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))
44	43	mpteq2dva 5205	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))
45	44	oveq2d 7373	. . . 4 ⊢ (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))
46	39, 45	mpteq12dv 5196	. . 3 ⊢ (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
47		df-sitg 32930	. . 3 ⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
48		ovex 7390	. . . 4 ⊢ (dom 𝑀MblFnM𝑆) ∈ V
49	48	mptrabex 7175	. . 3 ⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) ∈ V
50	32, 46, 47, 49	ovmpo 7515	. 2 ⊢ ((𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
51	2, 3, 50	syl2anc 584	1 ⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3064  {crab 3407  Vcvv 3445   ∖ cdif 3907  {csn 4586  ∪ cuni 4865   ↦ cmpt 5188  ^◡ccnv 5632  dom cdm 5633  ran crn 5634   “ cima 5636  ‘cfv 6496  (class class class)co 7357  Fincfn 8883  0cc0 11051  +∞cpnf 11186  [,)cico 13266  Basecbs 17083  Scalarcsca 17136   ·_𝑠 cvsca 17137  TopOpenctopn 17303  0_gc0g 17321   Σ_g cgsu 17322  ℝHomcrrh 32574  sigaGencsigagen 32737  measurescmeas 32794  MblFnMcmbfm 32848  sitgcsitg 32929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-sitg 32930

This theorem is referenced by:  issibf  32933  sitgfval  32941  sitgf  32947