Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > sitgclre | Structured version Visualization version GIF version |
Description: Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
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) |
sibfmbl.1 | β’ (π β πΉ β dom (πsitgπ)) |
sitgclre.1 | β’ (π β π β Ban) |
sitgclre.3 | β’ (π β (Scalarβπ) = βfld) |
Ref | Expression |
---|---|
sitgclre | β’ (π β ((πsitgπ)βπΉ) β π΅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sitgval.b | . 2 β’ π΅ = (Baseβπ) | |
2 | sitgval.j | . 2 β’ π½ = (TopOpenβπ) | |
3 | sitgval.s | . 2 β’ π = (sigaGenβπ½) | |
4 | sitgval.0 | . 2 β’ 0 = (0gβπ) | |
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 | sitgclre.1 | . 2 β’ (π β π β Ban) | |
11 | sitgclre.3 | . . 3 β’ (π β (Scalarβπ) = βfld) | |
12 | rerrext 32004 | . . 3 β’ βfld β βExt | |
13 | 11, 12 | eqeltrdi 2845 | . 2 β’ (π β (Scalarβπ) β βExt ) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13 | sitgclbn 32355 | 1 β’ (π β ((πsitgπ)βπΉ) β π΅) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1539 β wcel 2104 βͺ cuni 4844 dom cdm 5600 ran crn 5601 βcfv 6458 (class class class)co 7307 Basecbs 16957 Scalarcsca 17010 Β·π cvsca 17011 TopOpenctopn 17177 0gc0g 17195 βfldcrefld 20854 Bancbn 24542 βHomcrrh 31988 βExt crrext 31989 sigaGencsigagen 32151 measurescmeas 32208 sitgcsitg 32341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-resscn 10974 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-addrcl 10978 ax-mulcl 10979 ax-mulrcl 10980 ax-mulcom 10981 ax-addass 10982 ax-mulass 10983 ax-distr 10984 ax-i2m1 10985 ax-1ne0 10986 ax-1rid 10987 ax-rnegex 10988 ax-rrecex 10989 ax-cnre 10990 ax-pre-lttri 10991 ax-pre-lttrn 10992 ax-pre-ltadd 10993 ax-pre-mulgt0 10994 ax-pre-sup 10995 ax-addf 10996 ax-mulf 10997 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-tp 4570 df-op 4572 df-uni 4845 df-int 4887 df-iun 4933 df-iin 4934 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-se 5556 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-isom 6467 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-of 7565 df-om 7745 df-1st 7863 df-2nd 7864 df-supp 8009 df-tpos 8073 df-frecs 8128 df-wrecs 8159 df-recs 8233 df-rdg 8272 df-1o 8328 df-2o 8329 df-er 8529 df-map 8648 df-pm 8649 df-ixp 8717 df-en 8765 df-dom 8766 df-sdom 8767 df-fin 8768 df-fsupp 9173 df-fi 9214 df-sup 9245 df-inf 9246 df-oi 9313 df-card 9741 df-pnf 11057 df-mnf 11058 df-xr 11059 df-ltxr 11060 df-le 11061 df-sub 11253 df-neg 11254 df-div 11679 df-nn 12020 df-2 12082 df-3 12083 df-4 12084 df-5 12085 df-6 12086 df-7 12087 df-8 12088 df-9 12089 df-n0 12280 df-z 12366 df-dec 12484 df-uz 12629 df-q 12735 df-rp 12777 df-xneg 12894 df-xadd 12895 df-xmul 12896 df-ioo 13129 df-ico 13131 df-icc 13132 df-fz 13286 df-fzo 13429 df-fl 13558 df-mod 13636 df-seq 13768 df-exp 13829 df-hash 14091 df-cj 14855 df-re 14856 df-im 14857 df-sqrt 14991 df-abs 14992 df-dvds 16009 df-gcd 16247 df-numer 16484 df-denom 16485 df-gz 16676 df-struct 16893 df-sets 16910 df-slot 16928 df-ndx 16940 df-base 16958 df-ress 16987 df-plusg 17020 df-mulr 17021 df-starv 17022 df-sca 17023 df-vsca 17024 df-ip 17025 df-tset 17026 df-ple 17027 df-ds 17029 df-unif 17030 df-hom 17031 df-cco 17032 df-rest 17178 df-topn 17179 df-0g 17197 df-gsum 17198 df-topgen 17199 df-pt 17200 df-prds 17203 df-xrs 17258 df-qtop 17263 df-imas 17264 df-xps 17266 df-mre 17340 df-mrc 17341 df-acs 17343 df-proset 18058 df-poset 18076 df-plt 18093 df-toset 18180 df-ps 18329 df-tsr 18330 df-mgm 18371 df-sgrp 18420 df-mnd 18431 df-mhm 18475 df-submnd 18476 df-grp 18625 df-minusg 18626 df-sbg 18627 df-mulg 18746 df-subg 18797 df-ghm 18877 df-cntz 18968 df-od 19181 df-cmn 19433 df-abl 19434 df-mgp 19766 df-ur 19783 df-ring 19830 df-cring 19831 df-oppr 19907 df-dvdsr 19928 df-unit 19929 df-invr 19959 df-dvr 19970 df-rnghom 20004 df-drng 20038 df-field 20039 df-subrg 20067 df-abv 20122 df-lmod 20170 df-nzr 20574 df-psmet 20634 df-xmet 20635 df-met 20636 df-bl 20637 df-mopn 20638 df-fbas 20639 df-fg 20640 df-metu 20641 df-cnfld 20643 df-zring 20716 df-zrh 20750 df-zlm 20751 df-chr 20752 df-refld 20855 df-top 22088 df-topon 22105 df-topsp 22127 df-bases 22141 df-cld 22215 df-ntr 22216 df-cls 22217 df-nei 22294 df-cn 22423 df-cnp 22424 df-haus 22511 df-reg 22512 df-cmp 22583 df-tx 22758 df-hmeo 22951 df-fil 23042 df-fm 23134 df-flim 23135 df-flf 23136 df-fcls 23137 df-cnext 23256 df-ust 23397 df-utop 23428 df-uss 23453 df-usp 23454 df-ucn 23473 df-cfilu 23484 df-cusp 23495 df-xms 23518 df-ms 23519 df-tms 23520 df-nm 23783 df-ngp 23784 df-nrg 23786 df-nlm 23787 df-nvc 23788 df-cncf 24086 df-cfil 24464 df-cmet 24466 df-cms 24544 df-bn 24545 df-omnd 31370 df-ogrp 31371 df-orng 31541 df-ofld 31542 df-qqh 31968 df-rrh 31990 df-rrext 31994 df-esum 32041 df-siga 32122 df-sigagen 32152 df-meas 32209 df-mbfm 32263 df-sitg 32342 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |