Step | Hyp | Ref
| Expression |
1 | | funmpt 5926 |
. . . . . 6
/𝑒 |
2 | | ovex 6678 |
. . . . . . . 8
/𝑒 |
3 | 2 | rgenw 2924 |
. . . . . . 7
/𝑒 |
4 | | dmmptg 5632 |
. . . . . . 7
/𝑒 /𝑒 |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
/𝑒 |
6 | | df-fn 5891 |
. . . . . 6
/𝑒 /𝑒
/𝑒 |
7 | 1, 5, 6 | mpbir2an 955 |
. . . . 5
/𝑒 |
8 | 7 | a1i 11 |
. . . 4
measures
/𝑒 |
9 | | vex 3203 |
. . . . . . 7
|
10 | | eqid 2622 |
. . . . . . . 8
/𝑒 /𝑒 |
11 | 10 | elrnmpt 5372 |
. . . . . . 7
/𝑒
/𝑒 |
12 | 9, 11 | ax-mp 5 |
. . . . . 6
/𝑒
/𝑒 |
13 | | measfrge0 30266 |
. . . . . . . . . . 11
measures
|
14 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
15 | 13, 14 | sylan 488 |
. . . . . . . . . 10
measures
|
16 | 15 | adantlr 751 |
. . . . . . . . 9
measures |
17 | | simplr 792 |
. . . . . . . . 9
measures |
18 | 16, 17 | xrpxdivcld 29643 |
. . . . . . . 8
measures /𝑒 |
19 | | eleq1a 2696 |
. . . . . . . 8
/𝑒 /𝑒 |
20 | 18, 19 | syl 17 |
. . . . . . 7
measures /𝑒
|
21 | 20 | rexlimdva 3031 |
. . . . . 6
measures
/𝑒 |
22 | 12, 21 | syl5bi 232 |
. . . . 5
measures
/𝑒
|
23 | 22 | ssrdv 3609 |
. . . 4
measures
/𝑒
|
24 | | df-f 5892 |
. . . 4
/𝑒
/𝑒 /𝑒
|
25 | 8, 23, 24 | sylanbrc 698 |
. . 3
measures
/𝑒 |
26 | | measbase 30260 |
. . . . . . . 8
measures
sigAlgebra |
27 | | 0elsiga 30177 |
. . . . . . . 8
sigAlgebra |
28 | 26, 27 | syl 17 |
. . . . . . 7
measures
|
29 | 28 | adantr 481 |
. . . . . 6
measures
|
30 | | ovex 6678 |
. . . . . 6
/𝑒 |
31 | 29, 30 | jctir 561 |
. . . . 5
measures
/𝑒 |
32 | | fveq2 6191 |
. . . . . . 7
|
33 | 32 | oveq1d 6665 |
. . . . . 6
/𝑒 /𝑒 |
34 | 33, 10 | fvmptg 6280 |
. . . . 5
/𝑒 /𝑒 /𝑒 |
35 | 31, 34 | syl 17 |
. . . 4
measures
/𝑒 /𝑒 |
36 | | measvnul 30269 |
. . . . . 6
measures
|
37 | 36 | oveq1d 6665 |
. . . . 5
measures
/𝑒 /𝑒 |
38 | | xdiv0rp 29638 |
. . . . 5
/𝑒 |
39 | 37, 38 | sylan9eq 2676 |
. . . 4
measures
/𝑒 |
40 | 35, 39 | eqtrd 2656 |
. . 3
measures
/𝑒 |
41 | | simpll 790 |
. . . . . 6
measures
Disj measures
|
42 | | simplr 792 |
. . . . . . 7
measures
Disj |
43 | | simprl 794 |
. . . . . . 7
measures
Disj |
44 | | simprr 796 |
. . . . . . 7
measures
Disj Disj |
45 | 42, 43, 44 | 3jca 1242 |
. . . . . 6
measures
Disj Disj
|
46 | 9 | a1i 11 |
. . . . . . . . 9
measures |
47 | | simplll 798 |
. . . . . . . . . 10
measures
measures |
48 | | simplr 792 |
. . . . . . . . . . 11
measures
|
49 | | simpr 477 |
. . . . . . . . . . 11
measures
|
50 | | elpwg 4166 |
. . . . . . . . . . . . 13
|
51 | 9, 50 | ax-mp 5 |
. . . . . . . . . . . 12
|
52 | | ssel2 3598 |
. . . . . . . . . . . 12
|
53 | 51, 52 | sylanb 489 |
. . . . . . . . . . 11
|
54 | 48, 49, 53 | syl2anc 693 |
. . . . . . . . . 10
measures
|
55 | | measvxrge0 30268 |
. . . . . . . . . 10
measures
|
56 | 47, 54, 55 | syl2anc 693 |
. . . . . . . . 9
measures
|
57 | | simplr 792 |
. . . . . . . . 9
measures
|
58 | 46, 56, 57 | esumdivc 30145 |
. . . . . . . 8
measures Σ* /𝑒
Σ*
/𝑒 |
59 | 58 | 3ad2antr1 1226 |
. . . . . . 7
measures
Disj Σ* /𝑒
Σ*
/𝑒 |
60 | 26 | ad2antrr 762 |
. . . . . . . . . 10
measures
Disj sigAlgebra |
61 | | simpr1 1067 |
. . . . . . . . . 10
measures
Disj |
62 | | simpr2 1068 |
. . . . . . . . . 10
measures
Disj |
63 | | sigaclcu 30180 |
. . . . . . . . . 10
sigAlgebra
|
64 | 60, 61, 62, 63 | syl3anc 1326 |
. . . . . . . . 9
measures
Disj |
65 | | fveq2 6191 |
. . . . . . . . . . 11
|
66 | 65 | oveq1d 6665 |
. . . . . . . . . 10
/𝑒
/𝑒 |
67 | 66, 10, 2 | fvmpt3i 6287 |
. . . . . . . . 9
/𝑒
/𝑒 |
68 | 64, 67 | syl 17 |
. . . . . . . 8
measures
Disj /𝑒
/𝑒 |
69 | | simpll 790 |
. . . . . . . . . . 11
measures
Disj measures |
70 | 69, 61 | jca 554 |
. . . . . . . . . 10
measures
Disj measures
|
71 | | simpr3 1069 |
. . . . . . . . . . 11
measures
Disj Disj |
72 | 62, 71 | jca 554 |
. . . . . . . . . 10
measures
Disj Disj |
73 | | measvun 30272 |
. . . . . . . . . . . . 13
measures
Disj Σ* |
74 | 73 | 3expia 1267 |
. . . . . . . . . . . 12
measures
Disj Σ* |
75 | 74 | ralrimiva 2966 |
. . . . . . . . . . 11
measures
Disj Σ* |
76 | 75 | r19.21bi 2932 |
. . . . . . . . . 10
measures
Disj Σ* |
77 | 70, 72, 76 | sylc 65 |
. . . . . . . . 9
measures
Disj Σ* |
78 | 77 | oveq1d 6665 |
. . . . . . . 8
measures
Disj /𝑒 Σ*
/𝑒 |
79 | 68, 78 | eqtrd 2656 |
. . . . . . 7
measures
Disj /𝑒 Σ* /𝑒 |
80 | | fveq2 6191 |
. . . . . . . . . . . 12
|
81 | 80 | oveq1d 6665 |
. . . . . . . . . . 11
/𝑒 /𝑒 |
82 | 81, 10, 2 | fvmpt3i 6287 |
. . . . . . . . . 10
/𝑒 /𝑒 |
83 | 53, 82 | syl 17 |
. . . . . . . . 9
/𝑒 /𝑒 |
84 | 83 | esumeq2dv 30100 |
. . . . . . . 8
Σ* /𝑒
Σ*
/𝑒 |
85 | 61, 84 | syl 17 |
. . . . . . 7
measures
Disj Σ*
/𝑒 Σ* /𝑒 |
86 | 59, 79, 85 | 3eqtr4d 2666 |
. . . . . 6
measures
Disj /𝑒 Σ* /𝑒 |
87 | 41, 45, 86 | syl2anc 693 |
. . . . 5
measures
Disj /𝑒 Σ* /𝑒 |
88 | 87 | ex 450 |
. . . 4
measures Disj
/𝑒 Σ* /𝑒 |
89 | 88 | ralrimiva 2966 |
. . 3
measures
Disj /𝑒
Σ* /𝑒 |
90 | 25, 40, 89 | 3jca 1242 |
. 2
measures
/𝑒
/𝑒
Disj
/𝑒 Σ* /𝑒 |
91 | | ismeas 30262 |
. . . . 5
sigAlgebra
/𝑒 measures
/𝑒
/𝑒
Disj
/𝑒 Σ* /𝑒 |
92 | 26, 91 | syl 17 |
. . . 4
measures
/𝑒 measures
/𝑒
/𝑒
Disj
/𝑒 Σ* /𝑒 |
93 | 92 | biimprd 238 |
. . 3
measures
/𝑒
/𝑒
Disj
/𝑒 Σ* /𝑒
/𝑒 measures |
94 | 93 | adantr 481 |
. 2
measures
/𝑒
/𝑒
Disj
/𝑒 Σ* /𝑒
/𝑒 measures |
95 | 90, 94 | mpd 15 |
1
measures
/𝑒 measures |