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 34320

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 25315	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp)
14		cmsms 25319	. . 3 ⊢ (𝑊 ∈ CMetSp → 𝑊 ∈ MetSp)
15		mstps 24411	. . 3 ⊢ (𝑊 ∈ MetSp → 𝑊 ∈ TopSp)
16	12, 13, 14, 15	4syl 19	. 2 ⊢ (𝜑 → 𝑊 ∈ TopSp)
17		bnlmod 25314	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod)
18		lmodcmn 20877	. . 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 33988	. . . . . . . 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 20845	. . 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 34319	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 17230 Scalarcsca 17277 ·_𝑠 cvsca 17278 distcds 17283 TopOpenctopn 17438 0_gc0g 17456 CMndccmn 19767 LModclmod 20827 TopSpctps 22887 MetSpcms 24274 CMetSpccms 25303 Bancbn 25304 ℝHomcrrh 33969 ℝExt crrext 33970 sigaGencsigagen 34114 measurescmeas 34171 sitgcsitg 34306

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 14353 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-dvds 16274 df-gcd 16515 df-numer 16755 df-denom 16756 df-gz 16951 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17254 df-plusg 17287 df-mulr 17288 df-starv 17289 df-sca 17290 df-vsca 17291 df-ip 17292 df-tset 17293 df-ple 17294 df-ds 17296 df-unif 17297 df-hom 17298 df-cco 17299 df-rest 17439 df-topn 17440 df-0g 17458 df-gsum 17459 df-topgen 17460 df-pt 17461 df-prds 17464 df-xrs 17519 df-qtop 17524 df-imas 17525 df-xps 17527 df-mre 17601 df-mrc 17602 df-acs 17604 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-subg 19111 df-ghm 19201 df-cntz 19305 df-od 19515 df-cmn 19769 df-abl 19770 df-mgp 20107 df-rng 20119 df-ur 20148 df-ring 20201 df-cring 20202 df-oppr 20303 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-rhm 20441 df-nzr 20482 df-subrng 20515 df-subrg 20539 df-drng 20700 df-abv 20779 df-lmod 20829 df-psmet 21319 df-xmet 21320 df-met 21321 df-bl 21322 df-mopn 21323 df-fbas 21324 df-fg 21325 df-metu 21326 df-cnfld 21328 df-zring 21421 df-zrh 21477 df-zlm 21478 df-chr 21479 df-refld 21578 df-top 22849 df-topon 22866 df-topsp 22888 df-bases 22901 df-cld 22974 df-ntr 22975 df-cls 22976 df-nei 23053 df-cn 23182 df-cnp 23183 df-haus 23270 df-reg 23271 df-cmp 23342 df-tx 23517 df-hmeo 23710 df-fil 23801 df-fm 23893 df-flim 23894 df-flf 23895 df-fcls 23896 df-cnext 24015 df-ust 24156 df-utop 24187 df-uss 24212 df-usp 24213 df-ucn 24231 df-cfilu 24242 df-cusp 24253 df-xms 24276 df-ms 24277 df-tms 24278 df-nm 24540 df-ngp 24541 df-nrg 24543 df-nlm 24544 df-nvc 24545 df-cncf 24841 df-cfil 25226 df-cmet 25228 df-cms 25306 df-bn 25307 df-qqh 33947 df-rrh 33971 df-rrext 33975 df-esum 34004 df-siga 34085 df-sigagen 34115 df-meas 34172 df-mbfm 34226 df-sitg 34307

This theorem is referenced by: sitgclcn 34321 sitgclre 34322

W3C validator