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 30719
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 3408 . 2 (𝜑𝑊 ∈ V)
3 sitgval.2 . 2 (𝜑𝑀 ran measures)
4 2fveq3 6413 . . . . . . 7 (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = (sigaGen‘(TopOpen‘𝑊)))
5 sitgval.s . . . . . . . 8 𝑆 = (sigaGen‘𝐽)
6 sitgval.j . . . . . . . . 9 𝐽 = (TopOpen‘𝑊)
76fveq2i 6411 . . . . . . . 8 (sigaGen‘𝐽) = (sigaGen‘(TopOpen‘𝑊))
85, 7eqtri 2828 . . . . . . 7 𝑆 = (sigaGen‘(TopOpen‘𝑊))
94, 8syl6eqr 2858 . . . . . 6 (𝑤 = 𝑊 → (sigaGen‘(TopOpen‘𝑤)) = 𝑆)
109oveq2d 6890 . . . . 5 (𝑤 = 𝑊 → (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) = (dom 𝑚MblFnM𝑆))
11 fveq2 6408 . . . . . . . . . 10 (𝑤 = 𝑊 → (0g𝑤) = (0g𝑊))
12 sitgval.0 . . . . . . . . . 10 0 = (0g𝑊)
1311, 12syl6eqr 2858 . . . . . . . . 9 (𝑤 = 𝑊 → (0g𝑤) = 0 )
1413sneqd 4382 . . . . . . . 8 (𝑤 = 𝑊 → {(0g𝑤)} = { 0 })
1514difeq2d 3927 . . . . . . 7 (𝑤 = 𝑊 → (ran 𝑔 ∖ {(0g𝑤)}) = (ran 𝑔 ∖ { 0 }))
1615raleqdv 3333 . . . . . 6 (𝑤 = 𝑊 → (∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)))
1716anbi2d 616 . . . . 5 (𝑤 = 𝑊 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))))
1810, 17rabeqbidv 3385 . . . 4 (𝑤 = 𝑊 → {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))})
19 id 22 . . . . 5 (𝑤 = 𝑊𝑤 = 𝑊)
2014difeq2d 3927 . . . . . 6 (𝑤 = 𝑊 → (ran 𝑓 ∖ {(0g𝑤)}) = (ran 𝑓 ∖ { 0 }))
21 fveq2 6408 . . . . . . . 8 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
22 sitgval.x . . . . . . . 8 · = ( ·𝑠𝑊)
2321, 22syl6eqr 2858 . . . . . . 7 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
24 2fveq3 6413 . . . . . . . . 9 (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = (ℝHom‘(Scalar‘𝑊)))
25 sitgval.h . . . . . . . . 9 𝐻 = (ℝHom‘(Scalar‘𝑊))
2624, 25syl6eqr 2858 . . . . . . . 8 (𝑤 = 𝑊 → (ℝHom‘(Scalar‘𝑤)) = 𝐻)
2726fveq1d 6410 . . . . . . 7 (𝑤 = 𝑊 → ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥}))) = (𝐻‘(𝑚‘(𝑓 “ {𝑥}))))
28 eqidd 2807 . . . . . . 7 (𝑤 = 𝑊𝑥 = 𝑥)
2923, 27, 28oveq123d 6895 . . . . . 6 (𝑤 = 𝑊 → (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥) = ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥))
3020, 29mpteq12dv 4927 . . . . 5 (𝑤 = 𝑊 → (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥)))
3119, 30oveq12d 6892 . . . 4 (𝑤 = 𝑊 → (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥))))
3218, 31mpteq12dv 4927 . . 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 5525 . . . . . 6 (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀)
3433oveq1d 6889 . . . . 5 (𝑚 = 𝑀 → (dom 𝑚MblFnM𝑆) = (dom 𝑀MblFnM𝑆))
35 fveq1 6407 . . . . . . . 8 (𝑚 = 𝑀 → (𝑚‘(𝑔 “ {𝑥})) = (𝑀‘(𝑔 “ {𝑥})))
3635eleq1d 2870 . . . . . . 7 (𝑚 = 𝑀 → ((𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ (𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)))
3736ralbidv 3174 . . . . . 6 (𝑚 = 𝑀 → (∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)))
3837anbi2d 616 . . . . 5 (𝑚 = 𝑀 → ((ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)) ↔ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))))
3934, 38rabeqbidv 3385 . . . 4 (𝑚 = 𝑀 → {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} = {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))})
40 simpl 470 . . . . . . . . 9 ((𝑚 = 𝑀𝑥 ∈ (ran 𝑓 ∖ { 0 })) → 𝑚 = 𝑀)
4140fveq1d 6410 . . . . . . . 8 ((𝑚 = 𝑀𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝑚‘(𝑓 “ {𝑥})) = (𝑀‘(𝑓 “ {𝑥})))
4241fveq2d 6412 . . . . . . 7 ((𝑚 = 𝑀𝑥 ∈ (ran 𝑓 ∖ { 0 })) → (𝐻‘(𝑚‘(𝑓 “ {𝑥}))) = (𝐻‘(𝑀‘(𝑓 “ {𝑥}))))
4342oveq1d 6889 . . . . . 6 ((𝑚 = 𝑀𝑥 ∈ (ran 𝑓 ∖ { 0 })) → ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥) = ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥))
4443mpteq2dva 4938 . . . . 5 (𝑚 = 𝑀 → (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥)))
4544oveq2d 6890 . . . 4 (𝑚 = 𝑀 → (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥))) = (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥))))
4639, 45mpteq12dv 4927 . . 3 (𝑚 = 𝑀 → (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑚‘(𝑓 “ {𝑥}))) · 𝑥)))) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥)))))
47 df-sitg 30717 . . 3 sitg = (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
48 ovex 6906 . . . 4 (dom 𝑀MblFnM𝑆) ∈ V
4948mptrabex 6713 . . 3 (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥)))) ∈ V
5032, 46, 47, 49ovmpt2 7026 . 2 ((𝑊 ∈ V ∧ 𝑀 ran measures) → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥)))))
512, 3, 50syl2anc 575 1 (𝜑 → (𝑊sitg𝑀) = (𝑓 ∈ {𝑔 ∈ (dom 𝑀MblFnM𝑆) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ { 0 })(𝑀‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑊 Σg (𝑥 ∈ (ran 𝑓 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝑓 “ {𝑥}))) · 𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  wral 3096  {crab 3100  Vcvv 3391  cdif 3766  {csn 4370   cuni 4630  cmpt 4923  ccnv 5310  dom cdm 5311  ran crn 5312  cima 5314  cfv 6101  (class class class)co 6874  Fincfn 8192  0cc0 10221  +∞cpnf 10356  [,)cico 12395  Basecbs 16068  Scalarcsca 16156   ·𝑠 cvsca 16157  TopOpenctopn 16287  0gc0g 16305   Σg cgsu 16306  ℝHomcrrh 30362  sigaGencsigagen 30526  measurescmeas 30583  MblFnMcmbfm 30637  sitgcsitg 30716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-sitg 30717
This theorem is referenced by:  issibf  30720  sitgfval  30728  sitgf  30734
  Copyright terms: Public domain W3C validator