Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sitgval Structured version   Visualization version   GIF version

Theorem sitgval 33055
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.
StepHypRef Expression
1 sitgval.1 . . 3 (πœ‘ β†’ π‘Š ∈ 𝑉)
21elexd 3479 . 2 (πœ‘ β†’ π‘Š ∈ V)
3 sitgval.2 . 2 (πœ‘ β†’ 𝑀 ∈ βˆͺ ran measures)
4 2fveq3 6867 . . . . . . 7 (𝑀 = π‘Š β†’ (sigaGenβ€˜(TopOpenβ€˜π‘€)) = (sigaGenβ€˜(TopOpenβ€˜π‘Š)))
5 sitgval.s . . . . . . . 8 𝑆 = (sigaGenβ€˜π½)
6 sitgval.j . . . . . . . . 9 𝐽 = (TopOpenβ€˜π‘Š)
76fveq2i 6865 . . . . . . . 8 (sigaGenβ€˜π½) = (sigaGenβ€˜(TopOpenβ€˜π‘Š))
85, 7eqtri 2759 . . . . . . 7 𝑆 = (sigaGenβ€˜(TopOpenβ€˜π‘Š))
94, 8eqtr4di 2789 . . . . . 6 (𝑀 = π‘Š β†’ (sigaGenβ€˜(TopOpenβ€˜π‘€)) = 𝑆)
109oveq2d 7393 . . . . 5 (𝑀 = π‘Š β†’ (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€))) = (dom π‘šMblFnM𝑆))
11 fveq2 6862 . . . . . . . . . 10 (𝑀 = π‘Š β†’ (0gβ€˜π‘€) = (0gβ€˜π‘Š))
12 sitgval.0 . . . . . . . . . 10 0 = (0gβ€˜π‘Š)
1311, 12eqtr4di 2789 . . . . . . . . 9 (𝑀 = π‘Š β†’ (0gβ€˜π‘€) = 0 )
1413sneqd 4618 . . . . . . . 8 (𝑀 = π‘Š β†’ {(0gβ€˜π‘€)} = { 0 })
1514difeq2d 4102 . . . . . . 7 (𝑀 = π‘Š β†’ (ran 𝑔 βˆ– {(0gβ€˜π‘€)}) = (ran 𝑔 βˆ– { 0 }))
1615raleqdv 3324 . . . . . 6 (𝑀 = π‘Š β†’ (βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞) ↔ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)))
1716anbi2d 629 . . . . 5 (𝑀 = π‘Š β†’ ((ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))))
1810, 17rabeqbidv 3435 . . . 4 (𝑀 = π‘Š β†’ {𝑔 ∈ (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€))) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom π‘šMblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))})
19 id 22 . . . . 5 (𝑀 = π‘Š β†’ 𝑀 = π‘Š)
2014difeq2d 4102 . . . . . 6 (𝑀 = π‘Š β†’ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) = (ran 𝑓 βˆ– { 0 }))
21 fveq2 6862 . . . . . . . 8 (𝑀 = π‘Š β†’ ( ·𝑠 β€˜π‘€) = ( ·𝑠 β€˜π‘Š))
22 sitgval.x . . . . . . . 8 Β· = ( ·𝑠 β€˜π‘Š)
2321, 22eqtr4di 2789 . . . . . . 7 (𝑀 = π‘Š β†’ ( ·𝑠 β€˜π‘€) = Β· )
24 2fveq3 6867 . . . . . . . . 9 (𝑀 = π‘Š β†’ (ℝHomβ€˜(Scalarβ€˜π‘€)) = (ℝHomβ€˜(Scalarβ€˜π‘Š)))
25 sitgval.h . . . . . . . . 9 𝐻 = (ℝHomβ€˜(Scalarβ€˜π‘Š))
2624, 25eqtr4di 2789 . . . . . . . 8 (𝑀 = π‘Š β†’ (ℝHomβ€˜(Scalarβ€˜π‘€)) = 𝐻)
2726fveq1d 6864 . . . . . . 7 (𝑀 = π‘Š β†’ ((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) = (π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))))
28 eqidd 2732 . . . . . . 7 (𝑀 = π‘Š β†’ π‘₯ = π‘₯)
2923, 27, 28oveq123d 7398 . . . . . 6 (𝑀 = π‘Š β†’ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯) = ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯))
3020, 29mpteq12dv 5216 . . . . 5 (𝑀 = π‘Š β†’ (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯)) = (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))
3119, 30oveq12d 7395 . . . 4 (𝑀 = π‘Š β†’ (𝑀 Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯))) = (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯))))
3218, 31mpteq12dv 5216 . . 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 5879 . . . . . 6 (π‘š = 𝑀 β†’ dom π‘š = dom 𝑀)
3433oveq1d 7392 . . . . 5 (π‘š = 𝑀 β†’ (dom π‘šMblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35 fveq1 6861 . . . . . . . 8 (π‘š = 𝑀 β†’ (π‘šβ€˜(◑𝑔 β€œ {π‘₯})) = (π‘€β€˜(◑𝑔 β€œ {π‘₯})))
3635eleq1d 2817 . . . . . . 7 (π‘š = 𝑀 β†’ ((π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞) ↔ (π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)))
3736ralbidv 3176 . . . . . 6 (π‘š = 𝑀 β†’ (βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞) ↔ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)))
3837anbi2d 629 . . . . 5 (π‘š = 𝑀 β†’ ((ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))))
3934, 38rabeqbidv 3435 . . . 4 (π‘š = 𝑀 β†’ {𝑔 ∈ (dom π‘šMblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))})
40 simpl 483 . . . . . . . . 9 ((π‘š = 𝑀 ∧ π‘₯ ∈ (ran 𝑓 βˆ– { 0 })) β†’ π‘š = 𝑀)
4140fveq1d 6864 . . . . . . . 8 ((π‘š = 𝑀 ∧ π‘₯ ∈ (ran 𝑓 βˆ– { 0 })) β†’ (π‘šβ€˜(◑𝑓 β€œ {π‘₯})) = (π‘€β€˜(◑𝑓 β€œ {π‘₯})))
4241fveq2d 6866 . . . . . . 7 ((π‘š = 𝑀 ∧ π‘₯ ∈ (ran 𝑓 βˆ– { 0 })) β†’ (π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) = (π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))))
4342oveq1d 7392 . . . . . 6 ((π‘š = 𝑀 ∧ π‘₯ ∈ (ran 𝑓 βˆ– { 0 })) β†’ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯) = ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯))
4443mpteq2dva 5225 . . . . 5 (π‘š = 𝑀 β†’ (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)) = (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))
4544oveq2d 7393 . . . 4 (π‘š = 𝑀 β†’ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯))) = (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯))))
4639, 45mpteq12dv 5216 . . 3 (π‘š = 𝑀 β†’ (𝑓 ∈ {𝑔 ∈ (dom π‘šMblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))))
47 df-sitg 33053 . . 3 sitg = (𝑀 ∈ V, π‘š ∈ βˆͺ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€))) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (𝑀 Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯)))))
48 ovex 7410 . . . 4 (dom 𝑀MblFnM𝑆) ∈ V
4948mptrabex 7195 . . 3 (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))) ∈ V
5032, 46, 47, 49ovmpo 7535 . 2 ((π‘Š ∈ V ∧ 𝑀 ∈ βˆͺ ran measures) β†’ (π‘Šsitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))))
512, 3, 50syl2anc 584 1 (πœ‘ β†’ (π‘Šsitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– { 0 })(π‘€β€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (π‘Š Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– { 0 }) ↦ ((π»β€˜(π‘€β€˜(◑𝑓 β€œ {π‘₯}))) Β· π‘₯)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3060  {crab 3418  Vcvv 3459   βˆ– cdif 3925  {csn 4606  βˆͺ cuni 4885   ↦ cmpt 5208  β—‘ccnv 5652  dom cdm 5653  ran crn 5654   β€œ cima 5656  β€˜cfv 6516  (class class class)co 7377  Fincfn 8905  0cc0 11075  +∞cpnf 11210  [,)cico 13291  Basecbs 17109  Scalarcsca 17165   ·𝑠 cvsca 17166  TopOpenctopn 17332  0gc0g 17350   Ξ£g cgsu 17351  β„Homcrrh 32697  sigaGencsigagen 32860  measurescmeas 32917  MblFnMcmbfm 32971  sitgcsitg 33052
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 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pr 5404
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7380  df-oprab 7381  df-mpo 7382  df-sitg 33053
This theorem is referenced by:  issibf  33056  sitgfval  33064  sitgf  33070
  Copyright terms: Public domain W3C validator