sitgclbn - Mathbox for Thierry Arnoux

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

Theorem sitgclbn 34304

Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.)

**Hypotheses**
Ref	Expression
sitgval.b	⊢ 𝐵 = (Base‘𝑊)
sitgval.j	⊢ 𝐽 = (TopOpen‘𝑊)
sitgval.s	⊢ 𝑆 = (sigaGen‘𝐽)
sitgval.0	⊢ 0 = (0_g‘𝑊)
sitgval.x	⊢ · = ( ·_𝑠 ‘𝑊)
sitgval.h	⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
sitgval.1	⊢ (𝜑 → 𝑊 ∈ 𝑉)
sitgval.2	⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
sibfmbl.1	⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
sitgclbn.1	⊢ (𝜑 → 𝑊 ∈ Ban)
sitgclbn.2	⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )

**Assertion**
Ref	Expression
sitgclbn	⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)

Proof of Theorem sitgclbn Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sitgval.b	. 2 ⊢ 𝐵 = (Base‘𝑊)
2		sitgval.j	. 2 ⊢ 𝐽 = (TopOpen‘𝑊)
3		sitgval.s	. 2 ⊢ 𝑆 = (sigaGen‘𝐽)
4		sitgval.0	. 2 ⊢ 0 = (0_g‘𝑊)
5		sitgval.x	. 2 ⊢ · = ( ·_𝑠 ‘𝑊)
6		sitgval.h	. 2 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
7		sitgval.1	. 2 ⊢ (𝜑 → 𝑊 ∈ 𝑉)
8		sitgval.2	. 2 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
9		sibfmbl.1	. 2 ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
10		eqid 2734	. 2 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
11		eqid 2734	. 2 ⊢ ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊)))) = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
12		sitgclbn.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ Ban)
13		bncms 25314	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp)
14		cmsms 25318	. . 3 ⊢ (𝑊 ∈ CMetSp → 𝑊 ∈ MetSp)
15		mstps 24410	. . 3 ⊢ (𝑊 ∈ MetSp → 𝑊 ∈ TopSp)
16	12, 13, 14, 15	4syl 19	. 2 ⊢ (𝜑 → 𝑊 ∈ TopSp)
17		bnlmod 25313	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod)
18		lmodcmn 20876	. . 3 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
19	12, 17, 18	3syl 18	. 2 ⊢ (𝜑 → 𝑊 ∈ CMnd)
20		sitgclbn.2	. 2 ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
21	12, 17	syl 17	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LMod)
22	21	3ad2ant1 1133	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑊 ∈ LMod)
23		imassrn 6069	. . . . . 6 ⊢ (𝐻 “ (0[,)+∞)) ⊆ ran 𝐻
24	6	rneqi 5928	. . . . . . 7 ⊢ ran 𝐻 = ran (ℝHom‘(Scalar‘𝑊))
25		eqid 2734	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	25	rrhfe 33972	. . . . . . . 8 ⊢ ((Scalar‘𝑊) ∈ ℝExt → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
27		frn 6723	. . . . . . . 8 ⊢ ((ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)) → ran (ℝHom‘(Scalar‘𝑊)) ⊆ (Base‘(Scalar‘𝑊)))
28	20, 26, 27	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran (ℝHom‘(Scalar‘𝑊)) ⊆ (Base‘(Scalar‘𝑊)))
29	24, 28	eqsstrid 4002	. . . . . 6 ⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊)))
30	23, 29	sstrid 3975	. . . . 5 ⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆ (Base‘(Scalar‘𝑊)))
31	30	sselda 3963	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞))) → 𝑚 ∈ (Base‘(Scalar‘𝑊)))
32	31	3adant3 1132	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑚 ∈ (Base‘(Scalar‘𝑊)))
33		simp3 1138	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
34	1, 10, 5, 25	lmodvscl 20844	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑚 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵)
35	22, 32, 33, 34	syl3anc 1372	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵)
36	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 16, 19, 20, 35	sitgclg 34303	1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ⊆ wss 3931 ∪ cuni 4887 × cxp 5663 dom cdm 5665 ran crn 5666 ↾ cres 5667 “ cima 5668 ⟶wf 6537 ‘cfv 6541 (class class class)co 7413 ℝcr 11136 0cc0 11137 +∞cpnf 11274 [,)cico 13371 Basecbs 17229 Scalarcsca 17276 ·_𝑠 cvsca 17277 distcds 17282 TopOpenctopn 17437 0_gc0g 17455 CMndccmn 19766 LModclmod 20826 TopSpctps 22886 MetSpcms 24273 CMetSpccms 25302 Bancbn 25303 ℝHomcrrh 33953 ℝExt crrext 33954 sigaGencsigagen 34098 measurescmeas 34155 sitgcsitg 34290

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216 ax-mulf 11217

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-tpos 8233 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-er 8727 df-map 8850 df-pm 8851 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9532 df-card 9961 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13373 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-hash 14352 df-cj 15120 df-re 15121 df-im 15122 df-sqrt 15256 df-abs 15257 df-dvds 16273 df-gcd 16514 df-numer 16754 df-denom 16755 df-gz 16950 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-starv 17288 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-unif 17296 df-hom 17297 df-cco 17298 df-rest 17438 df-topn 17439 df-0g 17457 df-gsum 17458 df-topgen 17459 df-pt 17460 df-prds 17463 df-xrs 17518 df-qtop 17523 df-imas 17524 df-xps 17526 df-mre 17600 df-mrc 17601 df-acs 17603 df-mgm 18622 df-sgrp 18701 df-mnd 18717 df-mhm 18765 df-submnd 18766 df-grp 18923 df-minusg 18924 df-sbg 18925 df-mulg 19055 df-subg 19110 df-ghm 19200 df-cntz 19304 df-od 19514 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-cring 20201 df-oppr 20302 df-dvdsr 20325 df-unit 20326 df-invr 20356 df-dvr 20369 df-rhm 20440 df-nzr 20481 df-subrng 20514 df-subrg 20538 df-drng 20699 df-abv 20778 df-lmod 20828 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-fbas 21323 df-fg 21324 df-metu 21325 df-cnfld 21327 df-zring 21420 df-zrh 21476 df-zlm 21477 df-chr 21478 df-refld 21577 df-top 22848 df-topon 22865 df-topsp 22887 df-bases 22900 df-cld 22973 df-ntr 22974 df-cls 22975 df-nei 23052 df-cn 23181 df-cnp 23182 df-haus 23269 df-reg 23270 df-cmp 23341 df-tx 23516 df-hmeo 23709 df-fil 23800 df-fm 23892 df-flim 23893 df-flf 23894 df-fcls 23895 df-cnext 24014 df-ust 24155 df-utop 24186 df-uss 24211 df-usp 24212 df-ucn 24230 df-cfilu 24241 df-cusp 24252 df-xms 24275 df-ms 24276 df-tms 24277 df-nm 24539 df-ngp 24540 df-nrg 24542 df-nlm 24543 df-nvc 24544 df-cncf 24840 df-cfil 25225 df-cmet 25227 df-cms 25305 df-bn 25306 df-qqh 33931 df-rrh 33955 df-rrext 33959 df-esum 33988 df-siga 34069 df-sigagen 34099 df-meas 34156 df-mbfm 34210 df-sitg 34291

This theorem is referenced by: sitgclcn 34305 sitgclre 34306

W3C validator