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=BaseW
sitgval.j J=TopOpenW
sitgval.s S=𝛔J
sitgval.0 0˙=0W
sitgval.x ·˙=W
sitgval.h H=ℝHomScalarW
sitgval.1 φWV
sitgval.2 φMranmeasures
sibfmbl.1 φFMW
sibfinima.g φGMW
sibfinima.w φWTopSp
sibfinima.j φJFre
Assertion sibfinima φXranFYranGX0˙Y0˙MF-1XG-1Y0+∞

Proof

Step Hyp Ref Expression
1 sitgval.b B=BaseW
2 sitgval.j J=TopOpenW
3 sitgval.s S=𝛔J
4 sitgval.0 0˙=0W
5 sitgval.x ·˙=W
6 sitgval.h H=ℝHomScalarW
7 sitgval.1 φWV
8 sitgval.2 φMranmeasures
9 sibfmbl.1 φFMW
10 sibfinima.g φGMW
11 sibfinima.w φWTopSp
12 sibfinima.j φJFre
13 measbasedom MranmeasuresMmeasuresdomM
14 8 13 sylib φMmeasuresdomM
15 14 3ad2ant1 φXranFYranGMmeasuresdomM
16 dmmeas MranmeasuresdomMransigAlgebra
17 8 16 syl φdomMransigAlgebra
18 17 3ad2ant1 φXranFYranGdomMransigAlgebra
19 12 sgsiga φ𝛔JransigAlgebra
20 3 19 eqeltrid φSransigAlgebra
21 20 3ad2ant1 φXranFYranGSransigAlgebra
22 1 2 3 4 5 6 7 8 9 sibfmbl φFdomMMblFnμS
23 22 3ad2ant1 φXranFYranGFdomMMblFnμS
24 2 tpstop WTopSpJTop
25 cldssbrsiga JTopClsdJ𝛔J
26 11 24 25 3syl φClsdJ𝛔J
27 26 3 sseqtrrdi φClsdJS
28 27 3ad2ant1 φXranFYranGClsdJS
29 12 3ad2ant1 φXranFYranGJFre
30 1 2 3 4 5 6 7 8 9 sibff φF:domMJ
31 30 frnd φranFJ
32 31 3ad2ant1 φXranFYranGranFJ
33 simp2 φXranFYranGXranF
34 32 33 sseldd φXranFYranGXJ
35 eqid J=J
36 35 t1sncld JFreXJXClsdJ
37 29 34 36 syl2anc φXranFYranGXClsdJ
38 28 37 sseldd φXranFYranGXS
39 18 21 23 38 mbfmcnvima φXranFYranGF-1XdomM
40 1 2 3 4 5 6 7 8 10 sibfmbl φGdomMMblFnμS
41 40 3ad2ant1 φXranFYranGGdomMMblFnμS
42 1 2 3 4 5 6 7 8 10 sibff φG:domMJ
43 42 frnd φranGJ
44 43 3ad2ant1 φXranFYranGranGJ
45 simp3 φXranFYranGYranG
46 44 45 sseldd φXranFYranGYJ
47 35 t1sncld JFreYJYClsdJ
48 29 46 47 syl2anc φXranFYranGYClsdJ
49 28 48 sseldd φXranFYranGYS
50 18 21 41 49 mbfmcnvima φXranFYranGG-1YdomM
51 inelsiga domMransigAlgebraF-1XdomMG-1YdomMF-1XG-1YdomM
52 18 39 50 51 syl3anc φXranFYranGF-1XG-1YdomM
53 measvxrge0 MmeasuresdomMF-1XG-1YdomMMF-1XG-1Y0+∞
54 15 52 53 syl2anc φXranFYranGMF-1XG-1Y0+∞
55 elxrge0 MF-1XG-1Y0+∞MF-1XG-1Y*0MF-1XG-1Y
56 55 simplbi MF-1XG-1Y0+∞MF-1XG-1Y*
57 54 56 syl φXranFYranGMF-1XG-1Y*
58 57 adantr φXranFYranGX0˙Y0˙MF-1XG-1Y*
59 0re 0
60 59 a1i φXranFYranGX0˙Y0˙0
61 55 simprbi MF-1XG-1Y0+∞0MF-1XG-1Y
62 54 61 syl φXranFYranG0MF-1XG-1Y
63 62 adantr φXranFYranGX0˙Y0˙0MF-1XG-1Y
64 57 adantr φXranFYranGX0˙MF-1XG-1Y*
65 15 adantr φXranFYranGX0˙MmeasuresdomM
66 39 adantr φXranFYranGX0˙F-1XdomM
67 measvxrge0 MmeasuresdomMF-1XdomMMF-1X0+∞
68 65 66 67 syl2anc φXranFYranGX0˙MF-1X0+∞
69 elxrge0 MF-1X0+∞MF-1X*0MF-1X
70 69 simplbi MF-1X0+∞MF-1X*
71 68 70 syl φXranFYranGX0˙MF-1X*
72 pnfxr +∞*
73 72 a1i φXranFYranGX0˙+∞*
74 52 adantr φXranFYranGX0˙F-1XG-1YdomM
75 inss1 F-1XG-1YF-1X
76 75 a1i φXranFYranGX0˙F-1XG-1YF-1X
77 65 74 66 76 measssd φXranFYranGX0˙MF-1XG-1YMF-1X
78 simpl1 φXranFYranGX0˙φ
79 33 anim1i φXranFYranGX0˙XranFX0˙
80 eldifsn XranF0˙XranFX0˙
81 79 80 sylibr φXranFYranGX0˙XranF0˙
82 1 2 3 4 5 6 7 8 9 sibfima φXranF0˙MF-1X0+∞
83 78 81 82 syl2anc φXranFYranGX0˙MF-1X0+∞
84 elico2 0+∞*MF-1X0+∞MF-1X0MF-1XMF-1X<+∞
85 59 72 84 mp2an MF-1X0+∞MF-1X0MF-1XMF-1X<+∞
86 85 simp3bi MF-1X0+∞MF-1X<+∞
87 83 86 syl φXranFYranGX0˙MF-1X<+∞
88 64 71 73 77 87 xrlelttrd φXranFYranGX0˙MF-1XG-1Y<+∞
89 57 adantr φXranFYranGY0˙MF-1XG-1Y*
90 15 adantr φXranFYranGY0˙MmeasuresdomM
91 50 adantr φXranFYranGY0˙G-1YdomM
92 measvxrge0 MmeasuresdomMG-1YdomMMG-1Y0+∞
93 90 91 92 syl2anc φXranFYranGY0˙MG-1Y0+∞
94 elxrge0 MG-1Y0+∞MG-1Y*0MG-1Y
95 94 simplbi MG-1Y0+∞MG-1Y*
96 93 95 syl φXranFYranGY0˙MG-1Y*
97 72 a1i φXranFYranGY0˙+∞*
98 52 adantr φXranFYranGY0˙F-1XG-1YdomM
99 inss2 F-1XG-1YG-1Y
100 99 a1i φXranFYranGY0˙F-1XG-1YG-1Y
101 90 98 91 100 measssd φXranFYranGY0˙MF-1XG-1YMG-1Y
102 simpl1 φXranFYranGY0˙φ
103 45 anim1i φXranFYranGY0˙YranGY0˙
104 eldifsn YranG0˙YranGY0˙
105 103 104 sylibr φXranFYranGY0˙YranG0˙
106 1 2 3 4 5 6 7 8 10 sibfima φYranG0˙MG-1Y0+∞
107 102 105 106 syl2anc φXranFYranGY0˙MG-1Y0+∞
108 elico2 0+∞*MG-1Y0+∞MG-1Y0MG-1YMG-1Y<+∞
109 59 72 108 mp2an MG-1Y0+∞MG-1Y0MG-1YMG-1Y<+∞
110 109 simp3bi MG-1Y0+∞MG-1Y<+∞
111 107 110 syl φXranFYranGY0˙MG-1Y<+∞
112 89 96 97 101 111 xrlelttrd φXranFYranGY0˙MF-1XG-1Y<+∞
113 88 112 jaodan φXranFYranGX0˙Y0˙MF-1XG-1Y<+∞
114 xrre3 MF-1XG-1Y*00MF-1XG-1YMF-1XG-1Y<+∞MF-1XG-1Y
115 58 60 63 113 114 syl22anc φXranFYranGX0˙Y0˙MF-1XG-1Y
116 elico2 0+∞*MF-1XG-1Y0+∞MF-1XG-1Y0MF-1XG-1YMF-1XG-1Y<+∞
117 59 72 116 mp2an MF-1XG-1Y0+∞MF-1XG-1Y0MF-1XG-1YMF-1XG-1Y<+∞
118 115 63 113 117 syl3anbrc φXranFYranGX0˙Y0˙MF-1XG-1Y0+∞