Theorem sitgval 32295

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 3451	. 2 ⊢ (𝜑 → 𝑊 ∈ V)
3		sitgval.2	. 2 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4		2fveq3 6776	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = (sigaGen‘(TopOpen‘𝑊)))
5		sitgval.s	. . . . . . . 8 ⊢ 𝑆 = (sigaGen‘𝐽)
6		sitgval.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝑊)
7	6	fveq2i 6774	. . . . . . . 8 ⊢ (sigaGen‘𝐽) = (sigaGen‘(TopOpen‘𝑊))
8	5, 7	eqtri 2768	. . . . . . 7 ⊢ 𝑆 = (sigaGen‘(TopOpen‘𝑊))
9	4, 8	eqtr4di 2798	. . . . . 6 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆)
10	9	oveq2d 7287	. . . . 5 ⊢ (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆))
11		fveq2 6771	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊))
12		sitgval.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝑊)
13	11, 12	eqtr4di 2798	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 )
14	13	sneqd 4579	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 })
15	14	difeq2d 4062	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g‘𝑤)}) = (ran 𝑔 ∖ { 0 }))
16	15	raleqdv 3347	. . . . . 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 3419	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
19		id 22	. . . . 5 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
20	14	difeq2d 4062	. . . . . 6 ⊢ (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g‘𝑤)}) = (ran 𝑓 ∖ { 0 }))
21		fveq2 6771	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
22		sitgval.x	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
23	21, 22	eqtr4di 2798	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
24		2fveq3 6776	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊)))
25		sitgval.h	. . . . . . . . 9 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
26	24, 25	eqtr4di 2798	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = 𝐻)
27	26	fveq1d 6773	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))))
28		eqidd 2741	. . . . . . 7 ⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥)
29	23, 27, 28	oveq123d 7292	. . . . . 6 ⊢ (𝑤 = 𝑊 → (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥) = ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))
30	20, 29	mpteq12dv 5170	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))
31	19, 30	oveq12d 7289	. . . 4 ⊢ (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))))
32	18, 31	mpteq12dv 5170	. . 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 5811	. . . . . 6 ⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀)
34	33	oveq1d 7286	. . . . 5 ⊢ (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35		fveq1 6770	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (𝑚‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝑔 “ {𝑥})))
36	35	eleq1d 2825	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
37	36	ralbidv 3123	. . . . . 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 3419	. . . 4 ⊢ (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
40		simpl 483	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀)
41	40	fveq1d 6773	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝑓 “ {𝑥})))
42	41	fveq2d 6775	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))))
43	42	oveq1d 7286	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))
44	43	mpteq2dva 5179	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))
45	44	oveq2d 7287	. . . 4 ⊢ (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))
46	39, 45	mpteq12dv 5170	. . 3 ⊢ (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
47		df-sitg 32293	. . 3 ⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
48		ovex 7304	. . . 4 ⊢ (dom 𝑀MblFnM𝑆) ∈ V
49	48	mptrabex 7098	. . 3 ⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) ∈ V
50	32, 46, 47, 49	ovmpo 7427	. 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 1542   ∈ wcel 2110  ∀wral 3066  {crab 3070  Vcvv 3431   ∖ cdif 3889  {csn 4567  ∪ cuni 4845   ↦ cmpt 5162  ^◡ccnv 5589  dom cdm 5590  ran crn 5591   “ cima 5593  ‘cfv 6432  (class class class)co 7271  Fincfn 8716  0cc0 10872  +∞cpnf 11007  [,)cico 13080  Basecbs 16910  Scalarcsca 16963   ·_𝑠 cvsca 16964  TopOpenctopn 17130  0_gc0g 17148   Σ_g cgsu 17149  ℝHomcrrh 31939  sigaGencsigagen 32102  measurescmeas 32159  MblFnMcmbfm 32213  sitgcsitg 32292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-sitg 32293

This theorem is referenced by:  issibf  32296  sitgfval  32304  sitgf  32310