Metamath Proof Explorer

Theorem sibfinima

Description: The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018)

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 ) )
sibfinima.g 
|- ( ph -> G e. dom ( W sitg M ) )
sibfinima.w 
|- ( ph -> W e. TopSp )
sibfinima.j 
|- ( ph -> J e. Fre )
Assertion sibfinima 
|- ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,) +oo ) )

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 sibfinima.g 
 |-  ( ph -> G e. dom ( W sitg M ) )
11 sibfinima.w 
 |-  ( ph -> W e. TopSp )
12 sibfinima.j 
 |-  ( ph -> J e. Fre )
13 measbasedom 
 |-  ( M e. U. ran measures <-> M e. ( measures ` dom M ) )
14 8 13 sylib 
 |-  ( ph -> M e. ( measures ` dom M ) )
15 14 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> M e. ( measures ` dom M ) )
16 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
17 8 16 syl 
 |-  ( ph -> dom M e. U. ran sigAlgebra )
18 17 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> dom M e. U. ran sigAlgebra )
19 12 sgsiga 
 |-  ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
20 3 19 eqeltrid 
 |-  ( ph -> S e. U. ran sigAlgebra )
21 20 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> S e. U. ran sigAlgebra )
22 1 2 3 4 5 6 7 8 9 sibfmbl 
 |-  ( ph -> F e. ( dom M MblFnM S ) )
23 22 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> F e. ( dom M MblFnM S ) )
24 2 tpstop 
 |-  ( W e. TopSp -> J e. Top )
25 cldssbrsiga 
 |-  ( J e. Top -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
26 11 24 25 3syl 
 |-  ( ph -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
27 26 3 sseqtrrdi 
 |-  ( ph -> ( Clsd ` J ) C_ S )
28 27 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( Clsd ` J ) C_ S )
29 12 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> J e. Fre )
30 1 2 3 4 5 6 7 8 9 sibff 
 |-  ( ph -> F : U. dom M --> U. J )
31 30 frnd 
 |-  ( ph -> ran F C_ U. J )
32 31 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ran F C_ U. J )
33 simp2 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> X e. ran F )
34 32 33 sseldd 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> X e. U. J )
35 eqid 
 |-  U. J = U. J
36 35 t1sncld 
 |-  ( ( J e. Fre /\ X e. U. J ) -> { X } e. ( Clsd ` J ) )
37 29 34 36 syl2anc 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> { X } e. ( Clsd ` J ) )
38 28 37 sseldd 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> { X } e. S )
39 18 21 23 38 mbfmcnvima 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( `' F " { X } ) e. dom M )
40 1 2 3 4 5 6 7 8 10 sibfmbl 
 |-  ( ph -> G e. ( dom M MblFnM S ) )
41 40 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> G e. ( dom M MblFnM S ) )
42 1 2 3 4 5 6 7 8 10 sibff 
 |-  ( ph -> G : U. dom M --> U. J )
43 42 frnd 
 |-  ( ph -> ran G C_ U. J )
44 43 3ad2ant1 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ran G C_ U. J )
45 simp3 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> Y e. ran G )
46 44 45 sseldd 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> Y e. U. J )
47 35 t1sncld 
 |-  ( ( J e. Fre /\ Y e. U. J ) -> { Y } e. ( Clsd ` J ) )
48 29 46 47 syl2anc 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> { Y } e. ( Clsd ` J ) )
49 28 48 sseldd 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> { Y } e. S )
50 18 21 41 49 mbfmcnvima 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( `' G " { Y } ) e. dom M )
51 inelsiga 
 |-  ( ( dom M e. U. ran sigAlgebra /\ ( `' F " { X } ) e. dom M /\ ( `' G " { Y } ) e. dom M ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) e. dom M )
52 18 39 50 51 syl3anc 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) e. dom M )
53 measvxrge0 
 |-  ( ( M e. ( measures ` dom M ) /\ ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) e. dom M ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,] +oo ) )
54 15 52 53 syl2anc 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,] +oo ) )
55 elxrge0 
 |-  ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,] +oo ) <-> ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* /\ 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) ) )
56 55 simplbi 
 |-  ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,] +oo ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* )
57 54 56 syl 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* )
58 57 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* )
59 0re 
 |-  0 e. RR
60 59 a1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> 0 e. RR )
61 55 simprbi 
 |-  ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,] +oo ) -> 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) )
62 54 61 syl 
 |-  ( ( ph /\ X e. ran F /\ Y e. ran G ) -> 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) )
63 62 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) )
64 57 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* )
65 15 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> M e. ( measures ` dom M ) )
66 39 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( `' F " { X } ) e. dom M )
67 measvxrge0 
 |-  ( ( M e. ( measures ` dom M ) /\ ( `' F " { X } ) e. dom M ) -> ( M ` ( `' F " { X } ) ) e. ( 0 [,] +oo ) )
68 65 66 67 syl2anc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( `' F " { X } ) ) e. ( 0 [,] +oo ) )
69 elxrge0 
 |-  ( ( M ` ( `' F " { X } ) ) e. ( 0 [,] +oo ) <-> ( ( M ` ( `' F " { X } ) ) e. RR* /\ 0 <_ ( M ` ( `' F " { X } ) ) ) )
70 69 simplbi 
 |-  ( ( M ` ( `' F " { X } ) ) e. ( 0 [,] +oo ) -> ( M ` ( `' F " { X } ) ) e. RR* )
71 68 70 syl 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( `' F " { X } ) ) e. RR* )
72 pnfxr 
 |-  +oo e. RR*
73 72 a1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> +oo e. RR* )
74 52 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) e. dom M )
75 inss1 
 |-  ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) C_ ( `' F " { X } )
76 75 a1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) C_ ( `' F " { X } ) )
77 65 74 66 76 measssd 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) <_ ( M ` ( `' F " { X } ) ) )
78 simpl1 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ph )
79 33 anim1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( X e. ran F /\ X =/= .0. ) )
80 eldifsn 
 |-  ( X e. ( ran F \ { .0. } ) <-> ( X e. ran F /\ X =/= .0. ) )
81 79 80 sylibr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> X e. ( ran F \ { .0. } ) )
82 1 2 3 4 5 6 7 8 9 sibfima 
 |-  ( ( ph /\ X e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { X } ) ) e. ( 0 [,) +oo ) )
83 78 81 82 syl2anc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( `' F " { X } ) ) e. ( 0 [,) +oo ) )
84 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( M ` ( `' F " { X } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' F " { X } ) ) e. RR /\ 0 <_ ( M ` ( `' F " { X } ) ) /\ ( M ` ( `' F " { X } ) ) < +oo ) ) )
85 59 72 84 mp2an 
 |-  ( ( M ` ( `' F " { X } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' F " { X } ) ) e. RR /\ 0 <_ ( M ` ( `' F " { X } ) ) /\ ( M ` ( `' F " { X } ) ) < +oo ) )
86 85 simp3bi 
 |-  ( ( M ` ( `' F " { X } ) ) e. ( 0 [,) +oo ) -> ( M ` ( `' F " { X } ) ) < +oo )
87 83 86 syl 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( `' F " { X } ) ) < +oo )
88 64 71 73 77 87 xrlelttrd 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ X =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo )
89 57 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* )
90 15 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> M e. ( measures ` dom M ) )
91 50 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( `' G " { Y } ) e. dom M )
92 measvxrge0 
 |-  ( ( M e. ( measures ` dom M ) /\ ( `' G " { Y } ) e. dom M ) -> ( M ` ( `' G " { Y } ) ) e. ( 0 [,] +oo ) )
93 90 91 92 syl2anc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( `' G " { Y } ) ) e. ( 0 [,] +oo ) )
94 elxrge0 
 |-  ( ( M ` ( `' G " { Y } ) ) e. ( 0 [,] +oo ) <-> ( ( M ` ( `' G " { Y } ) ) e. RR* /\ 0 <_ ( M ` ( `' G " { Y } ) ) ) )
95 94 simplbi 
 |-  ( ( M ` ( `' G " { Y } ) ) e. ( 0 [,] +oo ) -> ( M ` ( `' G " { Y } ) ) e. RR* )
96 93 95 syl 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( `' G " { Y } ) ) e. RR* )
97 72 a1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> +oo e. RR* )
98 52 adantr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) e. dom M )
99 inss2 
 |-  ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) C_ ( `' G " { Y } )
100 99 a1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) C_ ( `' G " { Y } ) )
101 90 98 91 100 measssd 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) <_ ( M ` ( `' G " { Y } ) ) )
102 simpl1 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ph )
103 45 anim1i 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( Y e. ran G /\ Y =/= .0. ) )
104 eldifsn 
 |-  ( Y e. ( ran G \ { .0. } ) <-> ( Y e. ran G /\ Y =/= .0. ) )
105 103 104 sylibr 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> Y e. ( ran G \ { .0. } ) )
106 1 2 3 4 5 6 7 8 10 sibfima 
 |-  ( ( ph /\ Y e. ( ran G \ { .0. } ) ) -> ( M ` ( `' G " { Y } ) ) e. ( 0 [,) +oo ) )
107 102 105 106 syl2anc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( `' G " { Y } ) ) e. ( 0 [,) +oo ) )
108 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( M ` ( `' G " { Y } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' G " { Y } ) ) e. RR /\ 0 <_ ( M ` ( `' G " { Y } ) ) /\ ( M ` ( `' G " { Y } ) ) < +oo ) ) )
109 59 72 108 mp2an 
 |-  ( ( M ` ( `' G " { Y } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' G " { Y } ) ) e. RR /\ 0 <_ ( M ` ( `' G " { Y } ) ) /\ ( M ` ( `' G " { Y } ) ) < +oo ) )
110 109 simp3bi 
 |-  ( ( M ` ( `' G " { Y } ) ) e. ( 0 [,) +oo ) -> ( M ` ( `' G " { Y } ) ) < +oo )
111 107 110 syl 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( `' G " { Y } ) ) < +oo )
112 89 96 97 101 111 xrlelttrd 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ Y =/= .0. ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo )
113 88 112 jaodan 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo )
114 xrre3 
 |-  ( ( ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR* /\ 0 e. RR ) /\ ( 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) /\ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR )
115 58 60 63 113 114 syl22anc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR )
116 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR /\ 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) /\ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo ) ) )
117 59 72 116 mp2an 
 |-  ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. RR /\ 0 <_ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) /\ ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) < +oo ) )
118 115 63 113 117 syl3anbrc 
 |-  ( ( ( ph /\ X e. ran F /\ Y e. ran G ) /\ ( X =/= .0. \/ Y =/= .0. ) ) -> ( M ` ( ( `' F " { X } ) i^i ( `' G " { Y } ) ) ) e. ( 0 [,) +oo ) )