Theorem sitgval 34369

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 3488	. 2 ⊢ (𝜑 → 𝑊 ∈ V)
3		sitgval.2	. 2 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4		2fveq3 6886	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = (sigaGen‘(TopOpen‘𝑊)))
5		sitgval.s	. . . . . . . 8 ⊢ 𝑆 = (sigaGen‘𝐽)
6		sitgval.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝑊)
7	6	fveq2i 6884	. . . . . . . 8 ⊢ (sigaGen‘𝐽) = (sigaGen‘(TopOpen‘𝑊))
8	5, 7	eqtri 2759	. . . . . . 7 ⊢ 𝑆 = (sigaGen‘(TopOpen‘𝑊))
9	4, 8	eqtr4di 2789	. . . . . 6 ⊢ (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆)
10	9	oveq2d 7426	. . . . 5 ⊢ (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆))
11		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊))
12		sitgval.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝑊)
13	11, 12	eqtr4di 2789	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 )
14	13	sneqd 4618	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 })
15	14	difeq2d 4106	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g‘𝑤)}) = (ran 𝑔 ∖ { 0 }))
16	15	raleqdv 3309	. . . . . 6 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
17	16	anbi2d 630	. . . . 5 ⊢ (𝑤 = 𝑊 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
18	10, 17	rabeqbidv 3439	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
19		id 22	. . . . 5 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
20	14	difeq2d 4106	. . . . . 6 ⊢ (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g‘𝑤)}) = (ran 𝑓 ∖ { 0 }))
21		fveq2 6881	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
22		sitgval.x	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
23	21, 22	eqtr4di 2789	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
24		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊)))
25		sitgval.h	. . . . . . . . 9 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
26	24, 25	eqtr4di 2789	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = 𝐻)
27	26	fveq1d 6883	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))))
28		eqidd 2737	. . . . . . 7 ⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥)
29	23, 27, 28	oveq123d 7431	. . . . . 6 ⊢ (𝑤 = 𝑊 → (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥) = ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))
30	20, 29	mpteq12dv 5212	. . . . 5 ⊢ (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))
31	19, 30	oveq12d 7428	. . . 4 ⊢ (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))))
32	18, 31	mpteq12dv 5212	. . 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 5888	. . . . . 6 ⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀)
34	33	oveq1d 7425	. . . . 5 ⊢ (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35		fveq1 6880	. . . . . . . 8 ⊢ (𝑚 = 𝑀 → (𝑚‘(◡𝑔 “ {𝑥})) = (𝑀‘(◡𝑔 “ {𝑥})))
36	35	eleq1d 2820	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
37	36	ralbidv 3164	. . . . . 6 ⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)))
38	37	anbi2d 630	. . . . 5 ⊢ (𝑚 = 𝑀 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))))
39	34, 38	rabeqbidv 3439	. . . 4 ⊢ (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))})
40		simpl 482	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀)
41	40	fveq1d 6883	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(◡𝑓 “ {𝑥})) = (𝑀‘(◡𝑓 “ {𝑥})))
42	41	fveq2d 6885	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))))
43	42	oveq1d 7425	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))
44	43	mpteq2dva 5219	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))
45	44	oveq2d 7426	. . . 4 ⊢ (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥))))
46	39, 45	mpteq12dv 5212	. . 3 ⊢ (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(◡𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))))
47		df-sitg 34367	. . 3 ⊢ sitg = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠 ‘𝑤)𝑥)))))
48		ovex 7443	. . . 4 ⊢ (dom 𝑀MblFnM𝑆) ∈ V
49	48	mptrabex 7222	. . 3 ⊢ (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝑓 “ {𝑥}))) · 𝑥)))) ∈ V
50	32, 46, 47, 49	ovmpo 7572	. 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 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052  {crab 3420  Vcvv 3464   ∖ cdif 3928  {csn 4606  ∪ cuni 4888   ↦ cmpt 5206  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662  ‘cfv 6536  (class class class)co 7410  Fincfn 8964  0cc0 11134  +∞cpnf 11271  [,)cico 13369  Basecbs 17233  Scalarcsca 17279   ·_𝑠 cvsca 17280  TopOpenctopn 17440  0_gc0g 17458   Σ_g cgsu 17459  ℝHomcrrh 34029  sigaGencsigagen 34174  measurescmeas 34231  MblFnMcmbfm 34285  sitgcsitg 34366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-sitg 34367

This theorem is referenced by:  issibf  34370  sitgfval  34378  sitgf  34384