Metamath Proof Explorer

Theorem sitgclg

Description: Closure of the Bochner integral on simple functions, generic version. See sitgclbn for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018) (Proof shortened by AV, 12-Dec-2019)

Ref Expression
Hypotheses sitgval.b 
|- B = ( Base ` W )
sitgval.j 
|- J = ( TopOpen ` W )
sitgval.s 
|- S = ( sigaGen ` J )
sitgval.0 
|- .0. = ( 0g ` W )
sitgval.x 
|- .x. = ( .s ` W )
sitgval.h 
|- H = ( RRHom ` ( Scalar ` W ) )
sitgval.1 
|- ( ph -> W e. V )
sitgval.2 
|- ( ph -> M e. U. ran measures )
sibfmbl.1 
|- ( ph -> F e. dom ( W sitg M ) )
sitgclg.g 
|- G = ( Scalar ` W )
sitgclg.d 
|- D = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )
sitgclg.1 
|- ( ph -> W e. TopSp )
sitgclg.2 
|- ( ph -> W e. CMnd )
sitgclg.3 
|- ( ph -> ( Scalar ` W ) e. RRExt )
sitgclg.4 
|- ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B )
Assertion sitgclg 
|- ( ph -> ( ( W sitg M ) ` F ) e. B )

Proof

Step Hyp Ref Expression
1 sitgval.b 
 |-  B = ( Base ` W )
2 sitgval.j 
 |-  J = ( TopOpen ` W )
3 sitgval.s 
 |-  S = ( sigaGen ` J )
4 sitgval.0 
 |-  .0. = ( 0g ` W )
5 sitgval.x 
 |-  .x. = ( .s ` W )
6 sitgval.h 
 |-  H = ( RRHom ` ( Scalar ` W ) )
7 sitgval.1 
 |-  ( ph -> W e. V )
8 sitgval.2 
 |-  ( ph -> M e. U. ran measures )
9 sibfmbl.1 
 |-  ( ph -> F e. dom ( W sitg M ) )
10 sitgclg.g 
 |-  G = ( Scalar ` W )
11 sitgclg.d 
 |-  D = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )
12 sitgclg.1 
 |-  ( ph -> W e. TopSp )
13 sitgclg.2 
 |-  ( ph -> W e. CMnd )
14 sitgclg.3 
 |-  ( ph -> ( Scalar ` W ) e. RRExt )
15 sitgclg.4 
 |-  ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B )
16 1 2 3 4 5 6 7 8 9 sitgfval 
 |-  ( ph -> ( ( W sitg M ) ` F ) = ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) )
17 rnexg 
 |-  ( F e. dom ( W sitg M ) -> ran F e. _V )
18 difexg 
 |-  ( ran F e. _V -> ( ran F \ { .0. } ) e. _V )
19 9 17 18 3syl 
 |-  ( ph -> ( ran F \ { .0. } ) e. _V )
20 simpl 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> ph )
21 1 2 3 4 5 6 7 8 9 sibfima 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) )
22 10 fveq2i 
 |-  ( dist ` G ) = ( dist ` ( Scalar ` W ) )
23 10 fveq2i 
 |-  ( Base ` G ) = ( Base ` ( Scalar ` W ) )
24 23 23 xpeq12i 
 |-  ( ( Base ` G ) X. ( Base ` G ) ) = ( ( Base ` ( Scalar ` W ) ) X. ( Base ` ( Scalar ` W ) ) )
25 22 24 reseq12i 
 |-  ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) = ( ( dist ` ( Scalar ` W ) ) |` ( ( Base ` ( Scalar ` W ) ) X. ( Base ` ( Scalar ` W ) ) ) )
26 11 25 eqtri 
 |-  D = ( ( dist ` ( Scalar ` W ) ) |` ( ( Base ` ( Scalar ` W ) ) X. ( Base ` ( Scalar ` W ) ) ) )
27 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
28 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
29 10 fveq2i 
 |-  ( TopOpen ` G ) = ( TopOpen ` ( Scalar ` W ) )
30 10 fveq2i 
 |-  ( ZMod ` G ) = ( ZMod ` ( Scalar ` W ) )
31 10 14 eqeltrid 
 |-  ( ph -> G e. RRExt )
32 rrextdrg 
 |-  ( G e. RRExt -> G e. DivRing )
33 31 32 syl 
 |-  ( ph -> G e. DivRing )
34 10 33 eqeltrrid 
 |-  ( ph -> ( Scalar ` W ) e. DivRing )
35 rrextnrg 
 |-  ( G e. RRExt -> G e. NrmRing )
36 31 35 syl 
 |-  ( ph -> G e. NrmRing )
37 10 36 eqeltrrid 
 |-  ( ph -> ( Scalar ` W ) e. NrmRing )
38 eqid 
 |-  ( ZMod ` G ) = ( ZMod ` G )
39 38 rrextnlm 
 |-  ( G e. RRExt -> ( ZMod ` G ) e. NrmMod )
40 31 39 syl 
 |-  ( ph -> ( ZMod ` G ) e. NrmMod )
41 10 fveq2i 
 |-  ( chr ` G ) = ( chr ` ( Scalar ` W ) )
42 rrextchr 
 |-  ( G e. RRExt -> ( chr ` G ) = 0 )
43 31 42 syl 
 |-  ( ph -> ( chr ` G ) = 0 )
44 41 43 eqtr3id 
 |-  ( ph -> ( chr ` ( Scalar ` W ) ) = 0 )
45 rrextcusp 
 |-  ( G e. RRExt -> G e. CUnifSp )
46 31 45 syl 
 |-  ( ph -> G e. CUnifSp )
47 10 46 eqeltrrid 
 |-  ( ph -> ( Scalar ` W ) e. CUnifSp )
48 10 fveq2i 
 |-  ( UnifSt ` G ) = ( UnifSt ` ( Scalar ` W ) )
49 eqid 
 |-  ( Base ` G ) = ( Base ` G )
50 49 11 rrextust 
 |-  ( G e. RRExt -> ( UnifSt ` G ) = ( metUnif ` D ) )
51 31 50 syl 
 |-  ( ph -> ( UnifSt ` G ) = ( metUnif ` D ) )
52 48 51 eqtr3id 
 |-  ( ph -> ( UnifSt ` ( Scalar ` W ) ) = ( metUnif ` D ) )
53 26 27 28 29 30 34 37 40 44 47 52 rrhf 
 |-  ( ph -> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
54 6 feq1i 
 |-  ( H : RR --> ( Base ` ( Scalar ` W ) ) <-> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
55 53 54 sylibr 
 |-  ( ph -> H : RR --> ( Base ` ( Scalar ` W ) ) )
56 55 ffund 
 |-  ( ph -> Fun H )
57 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
58 55 fdmd 
 |-  ( ph -> dom H = RR )
59 57 58 sseqtrrid 
 |-  ( ph -> ( 0 [,) +oo ) C_ dom H )
60 funfvima2 
 |-  ( ( Fun H /\ ( 0 [,) +oo ) C_ dom H ) -> ( ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) -> ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) ) )
61 56 59 60 syl2anc 
 |-  ( ph -> ( ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) -> ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) ) )
62 20 21 61 sylc 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) )
63 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
64 8 63 syl 
 |-  ( ph -> dom M e. U. ran sigAlgebra )
65 2 fvexi 
 |-  J e. _V
66 65 a1i 
 |-  ( ph -> J e. _V )
67 66 sgsiga 
 |-  ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
68 3 67 eqeltrid 
 |-  ( ph -> S e. U. ran sigAlgebra )
69 1 2 3 4 5 6 7 8 9 sibfmbl 
 |-  ( ph -> F e. ( dom M MblFnM S ) )
70 64 68 69 mbfmf 
 |-  ( ph -> F : U. dom M --> U. S )
71 70 frnd 
 |-  ( ph -> ran F C_ U. S )
72 3 unieqi 
 |-  U. S = U. ( sigaGen ` J )
73 unisg 
 |-  ( J e. _V -> U. ( sigaGen ` J ) = U. J )
74 65 73 mp1i 
 |-  ( ph -> U. ( sigaGen ` J ) = U. J )
75 72 74 syl5eq 
 |-  ( ph -> U. S = U. J )
76 1 2 tpsuni 
 |-  ( W e. TopSp -> B = U. J )
77 12 76 syl 
 |-  ( ph -> B = U. J )
78 75 77 eqtr4d 
 |-  ( ph -> U. S = B )
79 71 78 sseqtrd 
 |-  ( ph -> ran F C_ B )
80 79 ssdifd 
 |-  ( ph -> ( ran F \ { .0. } ) C_ ( B \ { .0. } ) )
81 80 sselda 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> x e. ( B \ { .0. } ) )
82 81 eldifad 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> x e. B )
83 simp2 
 |-  ( ( ph /\ ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) )
84 eleq1 
 |-  ( m = ( H ` ( M ` ( `' F " { x } ) ) ) -> ( m e. ( H " ( 0 [,) +oo ) ) <-> ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) ) )
85 84 3anbi2d 
 |-  ( m = ( H ` ( M ` ( `' F " { x } ) ) ) -> ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) <-> ( ph /\ ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) ) )
86 oveq1 
 |-  ( m = ( H ` ( M ` ( `' F " { x } ) ) ) -> ( m .x. x ) = ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) )
87 86 eleq1d 
 |-  ( m = ( H ` ( M ` ( `' F " { x } ) ) ) -> ( ( m .x. x ) e. B <-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) e. B ) )
88 85 87 imbi12d 
 |-  ( m = ( H ` ( M ` ( `' F " { x } ) ) ) -> ( ( ( ph /\ m e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( m .x. x ) e. B ) <-> ( ( ph /\ ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) e. B ) ) )
89 88 15 vtoclg 
 |-  ( ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) -> ( ( ph /\ ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) e. B ) )
90 83 89 mpcom 
 |-  ( ( ph /\ ( H ` ( M ` ( `' F " { x } ) ) ) e. ( H " ( 0 [,) +oo ) ) /\ x e. B ) -> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) e. B )
91 20 62 82 90 syl3anc 
 |-  ( ( ph /\ x e. ( ran F \ { .0. } ) ) -> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) e. B )
92 91 fmpttd 
 |-  ( ph -> ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) : ( ran F \ { .0. } ) --> B )
93 mptexg 
 |-  ( ( ran F \ { .0. } ) e. _V -> ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) e. _V )
94 19 93 syl 
 |-  ( ph -> ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) e. _V )
95 4 fvexi 
 |-  .0. e. _V
96 suppimacnv 
 |-  ( ( ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) e. _V /\ .0. e. _V ) -> ( ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) supp .0. ) = ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) )
97 94 95 96 sylancl 
 |-  ( ph -> ( ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) supp .0. ) = ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) )
98 1 2 3 4 5 6 7 8 9 sibfrn 
 |-  ( ph -> ran F e. Fin )
99 cnvimass 
 |-  ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) C_ dom ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) )
100 eqid 
 |-  ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) = ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) )
101 100 dmmptss 
 |-  dom ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) C_ ( ran F \ { .0. } )
102 99 101 sstri 
 |-  ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) C_ ( ran F \ { .0. } )
103 difss 
 |-  ( ran F \ { .0. } ) C_ ran F
104 102 103 sstri 
 |-  ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) C_ ran F
105 ssfi 
 |-  ( ( ran F e. Fin /\ ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) C_ ran F ) -> ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) e. Fin )
106 98 104 105 sylancl 
 |-  ( ph -> ( `' ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) " ( _V \ { .0. } ) ) e. Fin )
107 97 106 eqeltrd 
 |-  ( ph -> ( ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) supp .0. ) e. Fin )
108 1 4 13 19 92 107 gsumcl2 
 |-  ( ph -> ( W gsum ( x e. ( ran F \ { .0. } ) |-> ( ( H ` ( M ` ( `' F " { x } ) ) ) .x. x ) ) ) e. B )
109 16 108 eqeltrd 
 |-  ( ph -> ( ( W sitg M ) ` F ) e. B )