Step | Hyp | Ref
| Expression |
1 | | caratheodory.o |
. . 3
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | caratheodory.s |
. . 3
⊢ 𝑆 = (CaraGen‘𝑂) |
3 | 1, 2 | caragensal 44026 |
. 2
⊢ (𝜑 → 𝑆 ∈ SAlg) |
4 | | eqid 2740 |
. . . 4
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
5 | 1, 4 | omef 43997 |
. . 3
⊢ (𝜑 → 𝑂:𝒫 ∪ dom
𝑂⟶(0[,]+∞)) |
6 | | caragenval 43994 |
. . . . . . 7
⊢ (𝑂 ∈ OutMeas →
(CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)}) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)}) |
8 | 7 | eqcomd 2746 |
. . . . 5
⊢ (𝜑 → {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)} = (CaraGen‘𝑂)) |
9 | 2 | eqcomi 2749 |
. . . . . 6
⊢
(CaraGen‘𝑂) =
𝑆 |
10 | 9 | a1i 11 |
. . . . 5
⊢ (𝜑 → (CaraGen‘𝑂) = 𝑆) |
11 | 8, 10 | eqtr2d 2781 |
. . . 4
⊢ (𝜑 → 𝑆 = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)}) |
12 | | ssrab2 4018 |
. . . 4
⊢ {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)} ⊆ 𝒫 ∪ dom 𝑂 |
13 | 11, 12 | eqsstrdi 3980 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝒫 ∪ dom 𝑂) |
14 | 5, 13 | fssresd 6638 |
. 2
⊢ (𝜑 → (𝑂 ↾ 𝑆):𝑆⟶(0[,]+∞)) |
15 | 1, 2 | caragen0 44007 |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝑆) |
16 | | fvres 6788 |
. . . 4
⊢ (∅
∈ 𝑆 → ((𝑂 ↾ 𝑆)‘∅) = (𝑂‘∅)) |
17 | 15, 16 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑂 ↾ 𝑆)‘∅) = (𝑂‘∅)) |
18 | 1 | ome0 43998 |
. . 3
⊢ (𝜑 → (𝑂‘∅) = 0) |
19 | 17, 18 | eqtrd 2780 |
. 2
⊢ (𝜑 → ((𝑂 ↾ 𝑆)‘∅) = 0) |
20 | | simp1 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → 𝜑) |
21 | | simp2 1136 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → 𝑒:ℕ⟶𝑆) |
22 | | fveq2 6769 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑒‘𝑛) = (𝑒‘𝑚)) |
23 | 22 | cbvdisjv 5055 |
. . . . . 6
⊢
(Disj 𝑛
∈ ℕ (𝑒‘𝑛) ↔ Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) |
24 | 23 | biimpi 215 |
. . . . 5
⊢
(Disj 𝑛
∈ ℕ (𝑒‘𝑛) → Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) |
25 | 24 | 3ad2ant3 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) |
26 | 1 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) → 𝑂 ∈ OutMeas) |
27 | | simp2 1136 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) → 𝑒:ℕ⟶𝑆) |
28 | 23 | biimpri 227 |
. . . . . 6
⊢
(Disj 𝑚
∈ ℕ (𝑒‘𝑚) → Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) |
29 | 28 | 3ad2ant3 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) → Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) |
30 | | fveq2 6769 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑒‘𝑚) = (𝑒‘𝑛)) |
31 | 30 | cbviunv 4975 |
. . . . . 6
⊢ ∪ 𝑚 ∈ (1...𝑗)(𝑒‘𝑚) = ∪ 𝑛 ∈ (1...𝑗)(𝑒‘𝑛) |
32 | 31 | mpteq2i 5184 |
. . . . 5
⊢ (𝑗 ∈ ℕ ↦ ∪ 𝑚 ∈ (1...𝑗)(𝑒‘𝑚)) = (𝑗 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑗)(𝑒‘𝑛)) |
33 | 26, 4, 2, 27, 29, 32 | caratheodorylem2 44028 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑚 ∈ ℕ (𝑒‘𝑚)) → (𝑂‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑒‘𝑛))))) |
34 | 20, 21, 25, 33 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑂‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑒‘𝑛))))) |
35 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → 𝑆 ∈ SAlg) |
36 | | nnenom 13690 |
. . . . . . . 8
⊢ ℕ
≈ ω |
37 | | endom 8742 |
. . . . . . . 8
⊢ (ℕ
≈ ω → ℕ ≼ ω) |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
⊢ ℕ
≼ ω |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ℕ ≼
ω) |
40 | | ffvelrn 6954 |
. . . . . . 7
⊢ ((𝑒:ℕ⟶𝑆 ∧ 𝑛 ∈ ℕ) → (𝑒‘𝑛) ∈ 𝑆) |
41 | 40 | adantll 711 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒:ℕ⟶𝑆) ∧ 𝑛 ∈ ℕ) → (𝑒‘𝑛) ∈ 𝑆) |
42 | 35, 39, 41 | saliuncl 43826 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) |
43 | | fvres 6788 |
. . . . 5
⊢ (∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆 → ((𝑂 ↾ 𝑆)‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) = (𝑂‘∪
𝑛 ∈ ℕ (𝑒‘𝑛))) |
44 | 42, 43 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ((𝑂 ↾ 𝑆)‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) = (𝑂‘∪
𝑛 ∈ ℕ (𝑒‘𝑛))) |
45 | 44 | 3adant3 1131 |
. . 3
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → ((𝑂 ↾ 𝑆)‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) = (𝑂‘∪
𝑛 ∈ ℕ (𝑒‘𝑛))) |
46 | | fvres 6788 |
. . . . . . 7
⊢ ((𝑒‘𝑛) ∈ 𝑆 → ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛)) = (𝑂‘(𝑒‘𝑛))) |
47 | 41, 46 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒:ℕ⟶𝑆) ∧ 𝑛 ∈ ℕ) → ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛)) = (𝑂‘(𝑒‘𝑛))) |
48 | 47 | mpteq2dva 5179 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → (𝑛 ∈ ℕ ↦ ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝑂‘(𝑒‘𝑛)))) |
49 | 48 | fveq2d 6773 |
. . . 4
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) →
(Σ^‘(𝑛 ∈ ℕ ↦ ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑒‘𝑛))))) |
50 | 49 | 3adant3 1131 |
. . 3
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) →
(Σ^‘(𝑛 ∈ ℕ ↦ ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑒‘𝑛))))) |
51 | 34, 45, 50 | 3eqtr4d 2790 |
. 2
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → ((𝑂 ↾ 𝑆)‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ ((𝑂 ↾ 𝑆)‘(𝑒‘𝑛))))) |
52 | 3, 14, 19, 51 | ismeannd 43968 |
1
⊢ (𝜑 → (𝑂 ↾ 𝑆) ∈ Meas) |