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

Theorem sibf0 29516
Description: The constant zero function is a simple function. (Contributed by Thierry Arnoux, 4-Mar-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)
sibf0.1 (𝜑𝑊 ∈ TopSp)
sibf0.2 (𝜑𝑊 ∈ Mnd)
Assertion
Ref Expression
sibf0 (𝜑 → ( dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀))

Proof of Theorem sibf0
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sitgval.2 . . . 4 (𝜑𝑀 ran measures)
2 dmmeas 29384 . . . 4 (𝑀 ran measures → dom 𝑀 ran sigAlgebra)
31, 2syl 17 . . 3 (𝜑 → dom 𝑀 ran sigAlgebra)
4 sitgval.s . . . 4 𝑆 = (sigaGen‘𝐽)
5 sitgval.j . . . . . . 7 𝐽 = (TopOpen‘𝑊)
6 fvex 6097 . . . . . . 7 (TopOpen‘𝑊) ∈ V
75, 6eqeltri 2683 . . . . . 6 𝐽 ∈ V
87a1i 11 . . . . 5 (𝜑𝐽 ∈ V)
98sgsiga 29325 . . . 4 (𝜑 → (sigaGen‘𝐽) ∈ ran sigAlgebra)
104, 9syl5eqel 2691 . . 3 (𝜑𝑆 ran sigAlgebra)
11 fconstmpt 5074 . . . 4 ( dom 𝑀 × { 0 }) = (𝑥 dom 𝑀0 )
1211a1i 11 . . 3 (𝜑 → ( dom 𝑀 × { 0 }) = (𝑥 dom 𝑀0 ))
13 sibf0.2 . . . . 5 (𝜑𝑊 ∈ Mnd)
14 sitgval.b . . . . . 6 𝐵 = (Base‘𝑊)
15 sitgval.0 . . . . . 6 0 = (0g𝑊)
1614, 15mndidcl 17079 . . . . 5 (𝑊 ∈ Mnd → 0𝐵)
1713, 16syl 17 . . . 4 (𝜑0𝐵)
18 sibf0.1 . . . . . 6 (𝜑𝑊 ∈ TopSp)
1914, 5tpsuni 20500 . . . . . 6 (𝑊 ∈ TopSp → 𝐵 = 𝐽)
2018, 19syl 17 . . . . 5 (𝜑𝐵 = 𝐽)
214unieqi 4375 . . . . . 6 𝑆 = (sigaGen‘𝐽)
22 unisg 29326 . . . . . . 7 (𝐽 ∈ V → (sigaGen‘𝐽) = 𝐽)
237, 22mp1i 13 . . . . . 6 (𝜑 (sigaGen‘𝐽) = 𝐽)
2421, 23syl5eq 2655 . . . . 5 (𝜑 𝑆 = 𝐽)
2520, 24eqtr4d 2646 . . . 4 (𝜑𝐵 = 𝑆)
2617, 25eleqtrd 2689 . . 3 (𝜑0 𝑆)
273, 10, 12, 26mbfmcst 29441 . 2 (𝜑 → ( dom 𝑀 × { 0 }) ∈ (dom 𝑀MblFnM𝑆))
28 xpeq1 5041 . . . . . . . 8 ( dom 𝑀 = ∅ → ( dom 𝑀 × { 0 }) = (∅ × { 0 }))
29 0xp 5111 . . . . . . . 8 (∅ × { 0 }) = ∅
3028, 29syl6eq 2659 . . . . . . 7 ( dom 𝑀 = ∅ → ( dom 𝑀 × { 0 }) = ∅)
3130rneqd 5260 . . . . . 6 ( dom 𝑀 = ∅ → ran ( dom 𝑀 × { 0 }) = ran ∅)
32 rn0 5284 . . . . . 6 ran ∅ = ∅
3331, 32syl6eq 2659 . . . . 5 ( dom 𝑀 = ∅ → ran ( dom 𝑀 × { 0 }) = ∅)
34 0fin 8050 . . . . 5 ∅ ∈ Fin
3533, 34syl6eqel 2695 . . . 4 ( dom 𝑀 = ∅ → ran ( dom 𝑀 × { 0 }) ∈ Fin)
36 rnxp 5468 . . . . 5 ( dom 𝑀 ≠ ∅ → ran ( dom 𝑀 × { 0 }) = { 0 })
37 snfi 7900 . . . . 5 { 0 } ∈ Fin
3836, 37syl6eqel 2695 . . . 4 ( dom 𝑀 ≠ ∅ → ran ( dom 𝑀 × { 0 }) ∈ Fin)
3935, 38pm2.61ine 2864 . . 3 ran ( dom 𝑀 × { 0 }) ∈ Fin
4039a1i 11 . 2 (𝜑 → ran ( dom 𝑀 × { 0 }) ∈ Fin)
41 noel 3877 . . . . . 6 ¬ 𝑥 ∈ ∅
4233difeq1d 3688 . . . . . . . . 9 ( dom 𝑀 = ∅ → (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) = (∅ ∖ { 0 }))
43 0dif 3928 . . . . . . . . 9 (∅ ∖ { 0 }) = ∅
4442, 43syl6eq 2659 . . . . . . . 8 ( dom 𝑀 = ∅ → (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) = ∅)
4536difeq1d 3688 . . . . . . . . 9 ( dom 𝑀 ≠ ∅ → (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) = ({ 0 } ∖ { 0 }))
46 difid 3901 . . . . . . . . 9 ({ 0 } ∖ { 0 }) = ∅
4745, 46syl6eq 2659 . . . . . . . 8 ( dom 𝑀 ≠ ∅ → (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) = ∅)
4844, 47pm2.61ine 2864 . . . . . . 7 (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) = ∅
4948eleq2i 2679 . . . . . 6 (𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) ↔ 𝑥 ∈ ∅)
5041, 49mtbir 311 . . . . 5 ¬ 𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 })
5150pm2.21i 114 . . . 4 (𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 }) → (𝑀‘(( dom 𝑀 × { 0 }) “ {𝑥})) ∈ (0[,)+∞))
5251adantl 480 . . 3 ((𝜑𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 })) → (𝑀‘(( dom 𝑀 × { 0 }) “ {𝑥})) ∈ (0[,)+∞))
5352ralrimiva 2948 . 2 (𝜑 → ∀𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 })(𝑀‘(( dom 𝑀 × { 0 }) “ {𝑥})) ∈ (0[,)+∞))
54 sitgval.x . . 3 · = ( ·𝑠𝑊)
55 sitgval.h . . 3 𝐻 = (ℝHom‘(Scalar‘𝑊))
56 sitgval.1 . . 3 (𝜑𝑊𝑉)
5714, 5, 4, 15, 54, 55, 56, 1issibf 29515 . 2 (𝜑 → (( dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀) ↔ (( dom 𝑀 × { 0 }) ∈ (dom 𝑀MblFnM𝑆) ∧ ran ( dom 𝑀 × { 0 }) ∈ Fin ∧ ∀𝑥 ∈ (ran ( dom 𝑀 × { 0 }) ∖ { 0 })(𝑀‘(( dom 𝑀 × { 0 }) “ {𝑥})) ∈ (0[,)+∞))))
5827, 40, 53, 57mpbir3and 1237 1 (𝜑 → ( dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cdif 3536  c0 3873  {csn 4124   cuni 4366  cmpt 4637   × cxp 5025  ccnv 5026  dom cdm 5027  ran crn 5028  cima 5030  cfv 5789  (class class class)co 6526  Fincfn 7818  0cc0 9792  +∞cpnf 9927  [,)cico 12006  Basecbs 15643  Scalarcsca 15719   ·𝑠 cvsca 15720  TopOpenctopn 15853  0gc0g 15871  Mndcmnd 17065  TopSpctps 20466  ℝHomcrrh 29158  sigAlgebracsiga 29290  sigaGencsigagen 29321  measurescmeas 29378  MblFnMcmbfm 29432  sitgcsitg 29511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1o 7424  df-map 7723  df-en 7819  df-fin 7822  df-0g 15873  df-mgm 17013  df-sgrp 17055  df-mnd 17066  df-top 20468  df-topon 20470  df-topsp 20471  df-esum 29210  df-siga 29291  df-sigagen 29322  df-meas 29379  df-mbfm 29433  df-sitg 29512
This theorem is referenced by:  sitg0  29528
  Copyright terms: Public domain W3C validator