Theorem sitgval 34495

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 3454	. 2 ⊢ (𝜑 → 𝑊 ∈ V)
3		sitgval.2	. 2 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4		2fveq3 6840	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = (sigaGen‘(TopOpen‘𝑊)))
5		sitgval.s	. . . . . . . 8 ⊢ 𝑆 = (sigaGen‘𝐽)
6		sitgval.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝑊)
7	6	fveq2i 6838	. . . . . . . 8 ⊢ (sigaGen‘𝐽) = (sigaGen‘(TopOpen‘𝑊))
8	5, 7	eqtri 2760	. . . . . . 7 ⊢ 𝑆 = (sigaGen‘(TopOpen‘𝑊))
9	4, 8	eqtr4di 2790	. . . . . 6 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆)
10	9	oveq2d 7377	. . . . 5 ⊢ (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆))
11		fveq2 6835	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊))
12		sitgval.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝑊)
13	11, 12	eqtr4di 2790	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 )
14	13	sneqd 4580	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 })
15	14	difeq2d 4067	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g‘𝑤)}) = (ran 𝑔 ∖ { 0 }))
16	15	raleqdv 3296	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
17	16	anbi2d 631	. . . . 5 ⊢ (𝑤 = 𝑊 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
18	10, 17	rabeqbidv 3408	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
19		id 22	. . . . 5 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
20	14	difeq2d 4067	. . . . . 6 ⊢ (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g‘𝑤)}) = (ran 𝑓 ∖ { 0 }))
21		fveq2 6835	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
22		sitgval.x	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
23	21, 22	eqtr4di 2790	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
24		2fveq3 6840	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊)))
25		sitgval.h	. . . . . . . . 9 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
26	24, 25	eqtr4di 2790	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = 𝐻)
27	26	fveq1d 6837	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))))
28		eqidd 2738	. . . . . . 7 ⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥)
29	23, 27, 28	oveq123d 7382	. . . . . 6 ⊢ (𝑤 = 𝑊 → (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥) = ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))
30	20, 29	mpteq12dv 5173	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))
31	19, 30	oveq12d 7379	. . . 4 ⊢ (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))))
32	18, 31	mpteq12dv 5173	. . 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 5853	. . . . . 6 ⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀)
34	33	oveq1d 7376	. . . . 5 ⊢ (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35		fveq1 6834	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (𝑚‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝑔 “ {𝑥})))
36	35	eleq1d 2822	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
37	36	ralbidv 3161	. . . . . 6 ⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
38	37	anbi2d 631	. . . . 5 ⊢ (𝑚 = 𝑀 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
39	34, 38	rabeqbidv 3408	. . . 4 ⊢ (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
40		simpl 482	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀)
41	40	fveq1d 6837	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝑓 “ {𝑥})))
42	41	fveq2d 6839	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))))
43	42	oveq1d 7376	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))
44	43	mpteq2dva 5179	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))
45	44	oveq2d 7377	. . . 4 ⊢ (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))
46	39, 45	mpteq12dv 5173	. . 3 ⊢ (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
47		df-sitg 34493	. . 3 ⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
48		ovex 7394	. . . 4 ⊢ (dom 𝑀MblFnM𝑆) ∈ V
49	48	mptrabex 7174	. . 3 ⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) ∈ V
50	32, 46, 47, 49	ovmpo 7521	. 2 ⊢ ((𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
51	2, 3, 50	syl2anc 585	1 ⊢ (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3390  Vcvv 3430   ∖ cdif 3887  {csn 4568  ∪ cuni 4851   ↦ cmpt 5167  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   “ cima 5628  ‘cfv 6493  (class class class)co 7361  Fincfn 8887  0cc0 11032  +∞cpnf 11170  [,)cico 13294  Basecbs 17173  Scalarcsca 17217   ·_𝑠 cvsca 17218  TopOpenctopn 17378  0_gc0g 17396   Σ_g cgsu 17397  ℝHomcrrh 34156  sigaGencsigagen 34301  measurescmeas 34358  MblFnMcmbfm 34412  sitgcsitg 34492

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-sitg 34493

This theorem is referenced by:  issibf  34496  sitgfval  34504  sitgf  34510