MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg11 Structured version   Visualization version   GIF version

Theorem itg11 23985
Description: The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypothesis
Ref Expression
i1f1.1 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 1, 0))
Assertion
Ref Expression
itg11 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (∫1𝐹) = (vol‘𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem itg11
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovol0 23787 . . . . 5 (vol*‘∅) = 0
2 0mbl 23833 . . . . . 6 ∅ ∈ dom vol
3 mblvol 23824 . . . . . 6 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
42, 3ax-mp 5 . . . . 5 (vol‘∅) = (vol*‘∅)
5 itg10 23982 . . . . 5 (∫1‘(ℝ × {0})) = 0
61, 4, 53eqtr4ri 2807 . . . 4 (∫1‘(ℝ × {0})) = (vol‘∅)
7 noel 4178 . . . . . . . . 9 ¬ 𝑥 ∈ ∅
8 eleq2 2848 . . . . . . . . 9 (𝐴 = ∅ → (𝑥𝐴𝑥 ∈ ∅))
97, 8mtbiri 319 . . . . . . . 8 (𝐴 = ∅ → ¬ 𝑥𝐴)
109iffalsed 4355 . . . . . . 7 (𝐴 = ∅ → if(𝑥𝐴, 1, 0) = 0)
1110mpteq2dv 5017 . . . . . 6 (𝐴 = ∅ → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 1, 0)) = (𝑥 ∈ ℝ ↦ 0))
12 i1f1.1 . . . . . 6 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, 1, 0))
13 fconstmpt 5457 . . . . . 6 (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)
1411, 12, 133eqtr4g 2833 . . . . 5 (𝐴 = ∅ → 𝐹 = (ℝ × {0}))
1514fveq2d 6497 . . . 4 (𝐴 = ∅ → (∫1𝐹) = (∫1‘(ℝ × {0})))
16 fveq2 6493 . . . 4 (𝐴 = ∅ → (vol‘𝐴) = (vol‘∅))
176, 15, 163eqtr4a 2834 . . 3 (𝐴 = ∅ → (∫1𝐹) = (vol‘𝐴))
1817a1i 11 . 2 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (𝐴 = ∅ → (∫1𝐹) = (vol‘𝐴)))
19 n0 4191 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦𝐴)
2012i1f1 23984 . . . . . . . 8 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → 𝐹 ∈ dom ∫1)
2120adantr 473 . . . . . . 7 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → 𝐹 ∈ dom ∫1)
22 itg1val 23977 . . . . . . 7 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(𝐹 “ {𝑧}))))
2321, 22syl 17 . . . . . 6 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (∫1𝐹) = Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(𝐹 “ {𝑧}))))
2412i1f1lem 23983 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (𝐹 “ {1}) = 𝐴))
2524simpli 476 . . . . . . . . . . . . 13 𝐹:ℝ⟶{0, 1}
26 frn 6344 . . . . . . . . . . . . 13 (𝐹:ℝ⟶{0, 1} → ran 𝐹 ⊆ {0, 1})
2725, 26ax-mp 5 . . . . . . . . . . . 12 ran 𝐹 ⊆ {0, 1}
28 ssdif 4002 . . . . . . . . . . . 12 (ran 𝐹 ⊆ {0, 1} → (ran 𝐹 ∖ {0}) ⊆ ({0, 1} ∖ {0}))
2927, 28ax-mp 5 . . . . . . . . . . 11 (ran 𝐹 ∖ {0}) ⊆ ({0, 1} ∖ {0})
30 difprsnss 4600 . . . . . . . . . . 11 ({0, 1} ∖ {0}) ⊆ {1}
3129, 30sstri 3863 . . . . . . . . . 10 (ran 𝐹 ∖ {0}) ⊆ {1}
3231a1i 11 . . . . . . . . 9 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (ran 𝐹 ∖ {0}) ⊆ {1})
33 mblss 23825 . . . . . . . . . . . . . . . 16 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3433adantr 473 . . . . . . . . . . . . . . 15 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → 𝐴 ⊆ ℝ)
3534sselda 3854 . . . . . . . . . . . . . 14 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → 𝑦 ∈ ℝ)
36 eleq1w 2842 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3736ifbid 4366 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → if(𝑥𝐴, 1, 0) = if(𝑦𝐴, 1, 0))
38 1ex 10427 . . . . . . . . . . . . . . . 16 1 ∈ V
39 c0ex 10425 . . . . . . . . . . . . . . . 16 0 ∈ V
4038, 39ifex 4392 . . . . . . . . . . . . . . 15 if(𝑦𝐴, 1, 0) ∈ V
4137, 12, 40fvmpt 6589 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ → (𝐹𝑦) = if(𝑦𝐴, 1, 0))
4235, 41syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (𝐹𝑦) = if(𝑦𝐴, 1, 0))
43 iftrue 4350 . . . . . . . . . . . . . 14 (𝑦𝐴 → if(𝑦𝐴, 1, 0) = 1)
4443adantl 474 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → if(𝑦𝐴, 1, 0) = 1)
4542, 44eqtrd 2808 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (𝐹𝑦) = 1)
46 ffn 6338 . . . . . . . . . . . . . 14 (𝐹:ℝ⟶{0, 1} → 𝐹 Fn ℝ)
4725, 46ax-mp 5 . . . . . . . . . . . . 13 𝐹 Fn ℝ
48 fnfvelrn 6667 . . . . . . . . . . . . 13 ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ran 𝐹)
4947, 35, 48sylancr 578 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (𝐹𝑦) ∈ ran 𝐹)
5045, 49eqeltrrd 2861 . . . . . . . . . . 11 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → 1 ∈ ran 𝐹)
51 ax-1ne0 10396 . . . . . . . . . . 11 1 ≠ 0
52 eldifsn 4587 . . . . . . . . . . 11 (1 ∈ (ran 𝐹 ∖ {0}) ↔ (1 ∈ ran 𝐹 ∧ 1 ≠ 0))
5350, 51, 52sylanblrc 581 . . . . . . . . . 10 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → 1 ∈ (ran 𝐹 ∖ {0}))
5453snssd 4610 . . . . . . . . 9 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → {1} ⊆ (ran 𝐹 ∖ {0}))
5532, 54eqssd 3871 . . . . . . . 8 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (ran 𝐹 ∖ {0}) = {1})
5655sumeq1d 14908 . . . . . . 7 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(𝐹 “ {𝑧}))) = Σ𝑧 ∈ {1} (𝑧 · (vol‘(𝐹 “ {𝑧}))))
57 1re 10431 . . . . . . . . 9 1 ∈ ℝ
5824simpri 478 . . . . . . . . . . . . . 14 (𝐴 ∈ dom vol → (𝐹 “ {1}) = 𝐴)
5958ad2antrr 713 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (𝐹 “ {1}) = 𝐴)
6059fveq2d 6497 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (vol‘(𝐹 “ {1})) = (vol‘𝐴))
6160oveq2d 6986 . . . . . . . . . . 11 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (1 · (vol‘(𝐹 “ {1}))) = (1 · (vol‘𝐴)))
62 simplr 756 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (vol‘𝐴) ∈ ℝ)
6362recnd 10460 . . . . . . . . . . . 12 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (vol‘𝐴) ∈ ℂ)
6463mulid2d 10450 . . . . . . . . . . 11 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (1 · (vol‘𝐴)) = (vol‘𝐴))
6561, 64eqtrd 2808 . . . . . . . . . 10 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (1 · (vol‘(𝐹 “ {1}))) = (vol‘𝐴))
6665, 63eqeltrd 2860 . . . . . . . . 9 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (1 · (vol‘(𝐹 “ {1}))) ∈ ℂ)
67 id 22 . . . . . . . . . . 11 (𝑧 = 1 → 𝑧 = 1)
68 sneq 4445 . . . . . . . . . . . . 13 (𝑧 = 1 → {𝑧} = {1})
6968imaeq2d 5764 . . . . . . . . . . . 12 (𝑧 = 1 → (𝐹 “ {𝑧}) = (𝐹 “ {1}))
7069fveq2d 6497 . . . . . . . . . . 11 (𝑧 = 1 → (vol‘(𝐹 “ {𝑧})) = (vol‘(𝐹 “ {1})))
7167, 70oveq12d 6988 . . . . . . . . . 10 (𝑧 = 1 → (𝑧 · (vol‘(𝐹 “ {𝑧}))) = (1 · (vol‘(𝐹 “ {1}))))
7271sumsn 14951 . . . . . . . . 9 ((1 ∈ ℝ ∧ (1 · (vol‘(𝐹 “ {1}))) ∈ ℂ) → Σ𝑧 ∈ {1} (𝑧 · (vol‘(𝐹 “ {𝑧}))) = (1 · (vol‘(𝐹 “ {1}))))
7357, 66, 72sylancr 578 . . . . . . . 8 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → Σ𝑧 ∈ {1} (𝑧 · (vol‘(𝐹 “ {𝑧}))) = (1 · (vol‘(𝐹 “ {1}))))
7473, 65eqtrd 2808 . . . . . . 7 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → Σ𝑧 ∈ {1} (𝑧 · (vol‘(𝐹 “ {𝑧}))) = (vol‘𝐴))
7556, 74eqtrd 2808 . . . . . 6 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(𝐹 “ {𝑧}))) = (vol‘𝐴))
7623, 75eqtrd 2808 . . . . 5 (((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ 𝑦𝐴) → (∫1𝐹) = (vol‘𝐴))
7776ex 405 . . . 4 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (𝑦𝐴 → (∫1𝐹) = (vol‘𝐴)))
7877exlimdv 1892 . . 3 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (∃𝑦 𝑦𝐴 → (∫1𝐹) = (vol‘𝐴)))
7919, 78syl5bi 234 . 2 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (𝐴 ≠ ∅ → (∫1𝐹) = (vol‘𝐴)))
8018, 79pm2.61dne 3048 1 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (∫1𝐹) = (vol‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wex 1742  wcel 2048  wne 2961  cdif 3822  wss 3825  c0 4173  ifcif 4344  {csn 4435  {cpr 4437  cmpt 5002   × cxp 5398  ccnv 5399  dom cdm 5400  ran crn 5401  cima 5403   Fn wfn 6177  wf 6178  cfv 6182  (class class class)co 6970  cc 10325  cr 10326  0cc0 10327  1c1 10328   · cmul 10332  Σcsu 14893  vol*covol 23756  volcvol 23757  1citg1 23909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8890  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404  ax-pre-sup 10405
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-2o 7898  df-oadd 7901  df-er 8081  df-map 8200  df-pm 8201  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-sup 8693  df-inf 8694  df-oi 8761  df-dju 9116  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-div 11091  df-nn 11432  df-2 11496  df-3 11497  df-n0 11701  df-z 11787  df-uz 12052  df-q 12156  df-rp 12198  df-xadd 12318  df-ioo 12551  df-ico 12553  df-icc 12554  df-fz 12702  df-fzo 12843  df-fl 12970  df-seq 13178  df-exp 13238  df-hash 13499  df-cj 14309  df-re 14310  df-im 14311  df-sqrt 14445  df-abs 14446  df-clim 14696  df-sum 14894  df-xmet 20230  df-met 20231  df-ovol 23758  df-vol 23759  df-mbf 23913  df-itg1 23914
This theorem is referenced by:  itg2const  24034  itg2addnclem  34332
  Copyright terms: Public domain W3C validator