Step | Hyp | Ref
| Expression |
1 | | sitgval.2 |
. . . . . . . 8
β’ (π β π β βͺ ran
measures) |
2 | | measbasedom 32562 |
. . . . . . . 8
β’ (π β βͺ ran measures β π β (measuresβdom π)) |
3 | 1, 2 | sylib 217 |
. . . . . . 7
β’ (π β π β (measuresβdom π)) |
4 | 3 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β (measuresβdom π)) |
5 | | dmmeas 32561 |
. . . . . . . . 9
β’ (π β βͺ ran measures β dom π β βͺ ran
sigAlgebra) |
6 | 1, 5 | syl 17 |
. . . . . . . 8
β’ (π β dom π β βͺ ran
sigAlgebra) |
7 | 6 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β dom π β βͺ ran
sigAlgebra) |
8 | | sitgval.s |
. . . . . . . . . 10
β’ π = (sigaGenβπ½) |
9 | | sibfinima.j |
. . . . . . . . . . 11
β’ (π β π½ β Fre) |
10 | 9 | sgsiga 32502 |
. . . . . . . . . 10
β’ (π β (sigaGenβπ½) β βͺ ran sigAlgebra) |
11 | 8, 10 | eqeltrid 2843 |
. . . . . . . . 9
β’ (π β π β βͺ ran
sigAlgebra) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β βͺ ran
sigAlgebra) |
13 | | sitgval.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
14 | | sitgval.j |
. . . . . . . . . 10
β’ π½ = (TopOpenβπ) |
15 | | sitgval.0 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
16 | | sitgval.x |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
17 | | sitgval.h |
. . . . . . . . . 10
β’ π» =
(βHomβ(Scalarβπ)) |
18 | | sitgval.1 |
. . . . . . . . . 10
β’ (π β π β π) |
19 | | sibfmbl.1 |
. . . . . . . . . 10
β’ (π β πΉ β dom (πsitgπ)) |
20 | 13, 14, 8, 15, 16, 17, 18, 1, 19 | sibfmbl 32696 |
. . . . . . . . 9
β’ (π β πΉ β (dom πMblFnMπ)) |
21 | 20 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β πΉ β (dom πMblFnMπ)) |
22 | | sibfinima.w |
. . . . . . . . . . . 12
β’ (π β π β TopSp) |
23 | 14 | tpstop 22208 |
. . . . . . . . . . . 12
β’ (π β TopSp β π½ β Top) |
24 | | cldssbrsiga 32547 |
. . . . . . . . . . . 12
β’ (π½ β Top β
(Clsdβπ½) β
(sigaGenβπ½)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (Clsdβπ½) β (sigaGenβπ½)) |
26 | 25, 8 | sseqtrrdi 3994 |
. . . . . . . . . 10
β’ (π β (Clsdβπ½) β π) |
27 | 26 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β (Clsdβπ½) β π) |
28 | 9 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π½ β Fre) |
29 | 13, 14, 8, 15, 16, 17, 18, 1, 19 | sibff 32697 |
. . . . . . . . . . . . 13
β’ (π β πΉ:βͺ dom πβΆβͺ π½) |
30 | 29 | frnd 6672 |
. . . . . . . . . . . 12
β’ (π β ran πΉ β βͺ π½) |
31 | 30 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β ran πΉ β βͺ π½) |
32 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β ran πΉ) |
33 | 31, 32 | sseldd 3944 |
. . . . . . . . . 10
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β βͺ π½) |
34 | | eqid 2738 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
35 | 34 | t1sncld 22599 |
. . . . . . . . . 10
β’ ((π½ β Fre β§ π β βͺ π½)
β {π} β
(Clsdβπ½)) |
36 | 28, 33, 35 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β {π} β (Clsdβπ½)) |
37 | 27, 36 | sseldd 3944 |
. . . . . . . 8
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β {π} β π) |
38 | 7, 12, 21, 37 | mbfmcnvima 32616 |
. . . . . . 7
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β (β‘πΉ β {π}) β dom π) |
39 | | sibfinima.g |
. . . . . . . . . 10
β’ (π β πΊ β dom (πsitgπ)) |
40 | 13, 14, 8, 15, 16, 17, 18, 1, 39 | sibfmbl 32696 |
. . . . . . . . 9
β’ (π β πΊ β (dom πMblFnMπ)) |
41 | 40 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β πΊ β (dom πMblFnMπ)) |
42 | 13, 14, 8, 15, 16, 17, 18, 1, 39 | sibff 32697 |
. . . . . . . . . . . . 13
β’ (π β πΊ:βͺ dom πβΆβͺ π½) |
43 | 42 | frnd 6672 |
. . . . . . . . . . . 12
β’ (π β ran πΊ β βͺ π½) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β ran πΊ β βͺ π½) |
45 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β ran πΊ) |
46 | 44, 45 | sseldd 3944 |
. . . . . . . . . 10
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β π β βͺ π½) |
47 | 34 | t1sncld 22599 |
. . . . . . . . . 10
β’ ((π½ β Fre β§ π β βͺ π½)
β {π} β
(Clsdβπ½)) |
48 | 28, 46, 47 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β {π} β (Clsdβπ½)) |
49 | 27, 48 | sseldd 3944 |
. . . . . . . 8
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β {π} β π) |
50 | 7, 12, 41, 49 | mbfmcnvima 32616 |
. . . . . . 7
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β (β‘πΊ β {π}) β dom π) |
51 | | inelsiga 32495 |
. . . . . . 7
β’ ((dom
π β βͺ ran sigAlgebra β§ (β‘πΉ β {π}) β dom π β§ (β‘πΊ β {π}) β dom π) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom π) |
52 | 7, 38, 50, 51 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom π) |
53 | | measvxrge0 32565 |
. . . . . 6
β’ ((π β (measuresβdom
π) β§ ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom π) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,]+β)) |
54 | 4, 52, 53 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,]+β)) |
55 | | elxrge0 13303 |
. . . . . 6
β’ ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,]+β) β ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β* β§ 0 β€
(πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) |
56 | 55 | simplbi 499 |
. . . . 5
β’ ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,]+β) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β
β*) |
57 | 54, 56 | syl 17 |
. . . 4
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β
β*) |
58 | 57 | adantr 482 |
. . 3
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β
β*) |
59 | | 0re 11091 |
. . . 4
β’ 0 β
β |
60 | 59 | a1i 11 |
. . 3
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β 0 β
β) |
61 | 55 | simprbi 498 |
. . . . 5
β’ ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,]+β) β 0 β€
(πβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
62 | 54, 61 | syl 17 |
. . . 4
β’ ((π β§ π β ran πΉ β§ π β ran πΊ) β 0 β€ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
63 | 62 | adantr 482 |
. . 3
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β 0 β€ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
64 | 57 | adantr 482 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β
β*) |
65 | 4 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π β (measuresβdom π)) |
66 | 38 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (β‘πΉ β {π}) β dom π) |
67 | | measvxrge0 32565 |
. . . . . . 7
β’ ((π β (measuresβdom
π) β§ (β‘πΉ β {π}) β dom π) β (πβ(β‘πΉ β {π})) β (0[,]+β)) |
68 | 65, 66, 67 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΉ β {π})) β (0[,]+β)) |
69 | | elxrge0 13303 |
. . . . . . 7
β’ ((πβ(β‘πΉ β {π})) β (0[,]+β) β ((πβ(β‘πΉ β {π})) β β* β§ 0 β€
(πβ(β‘πΉ β {π})))) |
70 | 69 | simplbi 499 |
. . . . . 6
β’ ((πβ(β‘πΉ β {π})) β (0[,]+β) β (πβ(β‘πΉ β {π})) β
β*) |
71 | 68, 70 | syl 17 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΉ β {π})) β
β*) |
72 | | pnfxr 11143 |
. . . . . 6
β’ +β
β β* |
73 | 72 | a1i 11 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β +β β
β*) |
74 | 52 | adantr 482 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom π) |
75 | | inss1 4187 |
. . . . . . 7
β’ ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΉ β {π}) |
76 | 75 | a1i 11 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΉ β {π})) |
77 | 65, 74, 66, 76 | measssd 32575 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β€ (πβ(β‘πΉ β {π}))) |
78 | | simpl1 1192 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π) |
79 | 32 | anim1i 616 |
. . . . . . . 8
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (π β ran πΉ β§ π β 0 )) |
80 | | eldifsn 4746 |
. . . . . . . 8
β’ (π β (ran πΉ β { 0 }) β (π β ran πΉ β§ π β 0 )) |
81 | 79, 80 | sylibr 233 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π β (ran πΉ β { 0 })) |
82 | 13, 14, 8, 15, 16, 17, 18, 1, 19 | sibfima 32699 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β { 0 })) β (πβ(β‘πΉ β {π})) β (0[,)+β)) |
83 | 78, 81, 82 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΉ β {π})) β (0[,)+β)) |
84 | | elico2 13257 |
. . . . . . . 8
β’ ((0
β β β§ +β β β*) β ((πβ(β‘πΉ β {π})) β (0[,)+β) β ((πβ(β‘πΉ β {π})) β β β§ 0 β€ (πβ(β‘πΉ β {π})) β§ (πβ(β‘πΉ β {π})) < +β))) |
85 | 59, 72, 84 | mp2an 691 |
. . . . . . 7
β’ ((πβ(β‘πΉ β {π})) β (0[,)+β) β ((πβ(β‘πΉ β {π})) β β β§ 0 β€ (πβ(β‘πΉ β {π})) β§ (πβ(β‘πΉ β {π})) < +β)) |
86 | 85 | simp3bi 1148 |
. . . . . 6
β’ ((πβ(β‘πΉ β {π})) β (0[,)+β) β (πβ(β‘πΉ β {π})) < +β) |
87 | 83, 86 | syl 17 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΉ β {π})) < +β) |
88 | 64, 71, 73, 77, 87 | xrlelttrd 13008 |
. . . 4
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β) |
89 | 57 | adantr 482 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β
β*) |
90 | 4 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π β (measuresβdom π)) |
91 | 50 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (β‘πΊ β {π}) β dom π) |
92 | | measvxrge0 32565 |
. . . . . . 7
β’ ((π β (measuresβdom
π) β§ (β‘πΊ β {π}) β dom π) β (πβ(β‘πΊ β {π})) β (0[,]+β)) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΊ β {π})) β (0[,]+β)) |
94 | | elxrge0 13303 |
. . . . . . 7
β’ ((πβ(β‘πΊ β {π})) β (0[,]+β) β ((πβ(β‘πΊ β {π})) β β* β§ 0 β€
(πβ(β‘πΊ β {π})))) |
95 | 94 | simplbi 499 |
. . . . . 6
β’ ((πβ(β‘πΊ β {π})) β (0[,]+β) β (πβ(β‘πΊ β {π})) β
β*) |
96 | 93, 95 | syl 17 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΊ β {π})) β
β*) |
97 | 72 | a1i 11 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β +β β
β*) |
98 | 52 | adantr 482 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom π) |
99 | | inss2 4188 |
. . . . . . 7
β’ ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΊ β {π}) |
100 | 99 | a1i 11 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΊ β {π})) |
101 | 90, 98, 91, 100 | measssd 32575 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β€ (πβ(β‘πΊ β {π}))) |
102 | | simpl1 1192 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π) |
103 | 45 | anim1i 616 |
. . . . . . . 8
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (π β ran πΊ β§ π β 0 )) |
104 | | eldifsn 4746 |
. . . . . . . 8
β’ (π β (ran πΊ β { 0 }) β (π β ran πΊ β§ π β 0 )) |
105 | 103, 104 | sylibr 233 |
. . . . . . 7
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β π β (ran πΊ β { 0 })) |
106 | 13, 14, 8, 15, 16, 17, 18, 1, 39 | sibfima 32699 |
. . . . . . 7
β’ ((π β§ π β (ran πΊ β { 0 })) β (πβ(β‘πΊ β {π})) β (0[,)+β)) |
107 | 102, 105,
106 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΊ β {π})) β (0[,)+β)) |
108 | | elico2 13257 |
. . . . . . . 8
β’ ((0
β β β§ +β β β*) β ((πβ(β‘πΊ β {π})) β (0[,)+β) β ((πβ(β‘πΊ β {π})) β β β§ 0 β€ (πβ(β‘πΊ β {π})) β§ (πβ(β‘πΊ β {π})) < +β))) |
109 | 59, 72, 108 | mp2an 691 |
. . . . . . 7
β’ ((πβ(β‘πΊ β {π})) β (0[,)+β) β ((πβ(β‘πΊ β {π})) β β β§ 0 β€ (πβ(β‘πΊ β {π})) β§ (πβ(β‘πΊ β {π})) < +β)) |
110 | 109 | simp3bi 1148 |
. . . . . 6
β’ ((πβ(β‘πΊ β {π})) β (0[,)+β) β (πβ(β‘πΊ β {π})) < +β) |
111 | 107, 110 | syl 17 |
. . . . 5
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ(β‘πΊ β {π})) < +β) |
112 | 89, 96, 97, 101, 111 | xrlelttrd 13008 |
. . . 4
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ π β 0 ) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β) |
113 | 88, 112 | jaodan 957 |
. . 3
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β) |
114 | | xrre3 13019 |
. . 3
β’ ((((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β* β§ 0
β β) β§ (0 β€ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β§ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β)) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
115 | 58, 60, 63, 113, 114 | syl22anc 838 |
. 2
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
116 | | elico2 13257 |
. . 3
β’ ((0
β β β§ +β β β*) β ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,)+β) β ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β β§ 0 β€ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β§ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β))) |
117 | 59, 72, 116 | mp2an 691 |
. 2
β’ ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,)+β) β ((πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β β§ 0 β€ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β§ (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) < +β)) |
118 | 115, 63, 113, 117 | syl3anbrc 1344 |
1
β’ (((π β§ π β ran πΉ β§ π β ran πΊ) β§ (π β 0 β¨ π β 0 )) β (πβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β (0[,)+β)) |