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 34339

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 2737	. 2 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
11		eqid 2737	. 2 ⊢ ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊)))) = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
12		sitgclbn.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ Ban)
13		bncms 25403	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp)
14		cmsms 25407	. . 3 ⊢ (𝑊 ∈ CMetSp → 𝑊 ∈ MetSp)
15		mstps 24490	. . 3 ⊢ (𝑊 ∈ MetSp → 𝑊 ∈ TopSp)
16	12, 13, 14, 15	4syl 19	. 2 ⊢ (𝜑 → 𝑊 ∈ TopSp)
17		bnlmod 25402	. . 3 ⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod)
18		lmodcmn 20934	. . 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 1134	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑊 ∈ LMod)
23		imassrn 6096	. . . . . 6 ⊢ (𝐻 “ (0[,)+∞)) ⊆ ran 𝐻
24	6	rneqi 5955	. . . . . . 7 ⊢ ran 𝐻 = ran (ℝHom‘(Scalar‘𝑊))
25		eqid 2737	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	25	rrhfe 34007	. . . . . . . 8 ⊢ ((Scalar‘𝑊) ∈ ℝExt → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
27		frn 6751	. . . . . . . 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 4047	. . . . . 6 ⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊)))
30	23, 29	sstrid 4010	. . . . 5 ⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆ (Base‘(Scalar‘𝑊)))
31	30	sselda 3998	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞))) → 𝑚 ∈ (Base‘(Scalar‘𝑊)))
32	31	3adant3 1133	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑚 ∈ (Base‘(Scalar‘𝑊)))
33		simp3 1139	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
34	1, 10, 5, 25	lmodvscl 20902	. . 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 34338	1 ⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1539 ∈ wcel 2108 ⊆ wss 3966 ∪ cuni 4915 × cxp 5691 dom cdm 5693 ran crn 5694 ↾ cres 5695 “ cima 5696 ⟶wf 6565 ‘cfv 6569 (class class class)co 7438 ℝcr 11161 0cc0 11162 +∞cpnf 11299 [,)cico 13395 Basecbs 17254 Scalarcsca 17310 ·_𝑠 cvsca 17311 distcds 17316 TopOpenctopn 17477 0_gc0g 17495 CMndccmn 19822 LModclmod 20884 TopSpctps 22963 MetSpcms 24353 CMetSpccms 25391 Bancbn 25392 ℝHomcrrh 33988 ℝExt crrext 33989 sigaGencsigagen 34133 measurescmeas 34190 sitgcsitg 34325

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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5288 ax-sep 5305 ax-nul 5315 ax-pow 5374 ax-pr 5441 ax-un 7761 ax-cnex 11218 ax-resscn 11219 ax-1cn 11220 ax-icn 11221 ax-addcl 11222 ax-addrcl 11223 ax-mulcl 11224 ax-mulrcl 11225 ax-mulcom 11226 ax-addass 11227 ax-mulass 11228 ax-distr 11229 ax-i2m1 11230 ax-1ne0 11231 ax-1rid 11232 ax-rnegex 11233 ax-rrecex 11234 ax-cnre 11235 ax-pre-lttri 11236 ax-pre-lttrn 11237 ax-pre-ltadd 11238 ax-pre-mulgt0 11239 ax-pre-sup 11240 ax-addf 11241 ax-mulf 11242

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3483 df-sbc 3795 df-csb 3912 df-dif 3969 df-un 3971 df-in 3973 df-ss 3983 df-pss 3986 df-nul 4343 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-tp 4639 df-op 4641 df-uni 4916 df-int 4955 df-iun 5001 df-iin 5002 df-br 5152 df-opab 5214 df-mpt 5235 df-tr 5269 df-id 5587 df-eprel 5593 df-po 5601 df-so 5602 df-fr 5645 df-se 5646 df-we 5647 df-xp 5699 df-rel 5700 df-cnv 5701 df-co 5702 df-dm 5703 df-rn 5704 df-res 5705 df-ima 5706 df-pred 6329 df-ord 6395 df-on 6396 df-lim 6397 df-suc 6398 df-iota 6522 df-fun 6571 df-fn 6572 df-f 6573 df-f1 6574 df-fo 6575 df-f1o 6576 df-fv 6577 df-isom 6578 df-riota 7395 df-ov 7441 df-oprab 7442 df-mpo 7443 df-of 7704 df-om 7895 df-1st 8022 df-2nd 8023 df-supp 8194 df-tpos 8259 df-frecs 8314 df-wrecs 8345 df-recs 8419 df-rdg 8458 df-1o 8514 df-2o 8515 df-er 8753 df-map 8876 df-pm 8877 df-ixp 8946 df-en 8994 df-dom 8995 df-sdom 8996 df-fin 8997 df-fsupp 9409 df-fi 9458 df-sup 9489 df-inf 9490 df-oi 9557 df-card 9986 df-pnf 11304 df-mnf 11305 df-xr 11306 df-ltxr 11307 df-le 11308 df-sub 11501 df-neg 11502 df-div 11928 df-nn 12274 df-2 12336 df-3 12337 df-4 12338 df-5 12339 df-6 12340 df-7 12341 df-8 12342 df-9 12343 df-n0 12534 df-z 12621 df-dec 12741 df-uz 12886 df-q 12998 df-rp 13042 df-xneg 13161 df-xadd 13162 df-xmul 13163 df-ioo 13397 df-ico 13399 df-icc 13400 df-fz 13554 df-fzo 13701 df-fl 13838 df-mod 13916 df-seq 14049 df-exp 14109 df-hash 14376 df-cj 15144 df-re 15145 df-im 15146 df-sqrt 15280 df-abs 15281 df-dvds 16297 df-gcd 16538 df-numer 16778 df-denom 16779 df-gz 16973 df-struct 17190 df-sets 17207 df-slot 17225 df-ndx 17237 df-base 17255 df-ress 17284 df-plusg 17320 df-mulr 17321 df-starv 17322 df-sca 17323 df-vsca 17324 df-ip 17325 df-tset 17326 df-ple 17327 df-ds 17329 df-unif 17330 df-hom 17331 df-cco 17332 df-rest 17478 df-topn 17479 df-0g 17497 df-gsum 17498 df-topgen 17499 df-pt 17500 df-prds 17503 df-xrs 17558 df-qtop 17563 df-imas 17564 df-xps 17566 df-mre 17640 df-mrc 17641 df-acs 17643 df-mgm 18675 df-sgrp 18754 df-mnd 18770 df-mhm 18818 df-submnd 18819 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-ghm 19253 df-cntz 19357 df-od 19570 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-ring 20262 df-cring 20263 df-oppr 20360 df-dvdsr 20383 df-unit 20384 df-invr 20414 df-dvr 20427 df-rhm 20498 df-nzr 20539 df-subrng 20572 df-subrg 20596 df-drng 20757 df-abv 20836 df-lmod 20886 df-psmet 21383 df-xmet 21384 df-met 21385 df-bl 21386 df-mopn 21387 df-fbas 21388 df-fg 21389 df-metu 21390 df-cnfld 21392 df-zring 21485 df-zrh 21541 df-zlm 21542 df-chr 21543 df-refld 21650 df-top 22925 df-topon 22942 df-topsp 22964 df-bases 22978 df-cld 23052 df-ntr 23053 df-cls 23054 df-nei 23131 df-cn 23260 df-cnp 23261 df-haus 23348 df-reg 23349 df-cmp 23420 df-tx 23595 df-hmeo 23788 df-fil 23879 df-fm 23971 df-flim 23972 df-flf 23973 df-fcls 23974 df-cnext 24093 df-ust 24234 df-utop 24265 df-uss 24290 df-usp 24291 df-ucn 24310 df-cfilu 24321 df-cusp 24332 df-xms 24355 df-ms 24356 df-tms 24357 df-nm 24620 df-ngp 24621 df-nrg 24623 df-nlm 24624 df-nvc 24625 df-cncf 24929 df-cfil 25314 df-cmet 25316 df-cms 25394 df-bn 25395 df-qqh 33966 df-rrh 33990 df-rrext 33994 df-esum 34023 df-siga 34104 df-sigagen 34134 df-meas 34191 df-mbfm 34245 df-sitg 34326

This theorem is referenced by: sitgclcn 34340 sitgclre 34341

W3C validator