Step | Hyp | Ref
| Expression |
1 | | sitgval.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
2 | | dmmeas 29591 |
. . . 4
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
4 | | sitgval.s |
. . . 4
⊢ 𝑆 = (sigaGen‘𝐽) |
5 | | sitgval.j |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝑊) |
6 | | fvex 6113 |
. . . . . . 7
⊢
(TopOpen‘𝑊)
∈ V |
7 | 5, 6 | eqeltri 2684 |
. . . . . 6
⊢ 𝐽 ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ V) |
9 | 8 | sgsiga 29532 |
. . . 4
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
10 | 4, 9 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
11 | | fconstmpt 5085 |
. . . 4
⊢ (∪ dom 𝑀 × { 0 }) = (𝑥 ∈ ∪ dom
𝑀 ↦ 0
) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) = (𝑥 ∈ ∪ dom
𝑀 ↦ 0
)) |
13 | | sibf0.2 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Mnd) |
14 | | sitgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
15 | | sitgval.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑊) |
16 | 14, 15 | mndidcl 17131 |
. . . . 5
⊢ (𝑊 ∈ Mnd → 0 ∈ 𝐵) |
17 | 13, 16 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐵) |
18 | | sibf0.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ TopSp) |
19 | 14, 5 | tpsuni 20553 |
. . . . . 6
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
21 | 4 | unieqi 4381 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ (sigaGen‘𝐽) |
22 | | unisg 29533 |
. . . . . . 7
⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
23 | 7, 22 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
24 | 21, 23 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝐽) |
25 | 20, 24 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → 𝐵 = ∪ 𝑆) |
26 | 17, 25 | eleqtrd 2690 |
. . 3
⊢ (𝜑 → 0 ∈ ∪ 𝑆) |
27 | 3, 10, 12, 26 | mbfmcst 29648 |
. 2
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ (dom 𝑀MblFnM𝑆)) |
28 | | xpeq1 5052 |
. . . . . . . 8
⊢ (∪ dom 𝑀 = ∅ → (∪ dom 𝑀 × { 0 }) = (∅ × {
0
})) |
29 | | 0xp 5122 |
. . . . . . . 8
⊢ (∅
× { 0 }) =
∅ |
30 | 28, 29 | syl6eq 2660 |
. . . . . . 7
⊢ (∪ dom 𝑀 = ∅ → (∪ dom 𝑀 × { 0 }) =
∅) |
31 | 30 | rneqd 5274 |
. . . . . 6
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) = ran
∅) |
32 | | rn0 5298 |
. . . . . 6
⊢ ran
∅ = ∅ |
33 | 31, 32 | syl6eq 2660 |
. . . . 5
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) =
∅) |
34 | | 0fin 8073 |
. . . . 5
⊢ ∅
∈ Fin |
35 | 33, 34 | syl6eqel 2696 |
. . . 4
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
36 | | rnxp 5483 |
. . . . 5
⊢ (∪ dom 𝑀 ≠ ∅ → ran (∪ dom 𝑀 × { 0 }) = { 0 }) |
37 | | snfi 7923 |
. . . . 5
⊢ { 0 } ∈
Fin |
38 | 36, 37 | syl6eqel 2696 |
. . . 4
⊢ (∪ dom 𝑀 ≠ ∅ → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
39 | 35, 38 | pm2.61ine 2865 |
. . 3
⊢ ran
(∪ dom 𝑀 × { 0 }) ∈
Fin |
40 | 39 | a1i 11 |
. 2
⊢ (𝜑 → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
41 | | noel 3878 |
. . . . . 6
⊢ ¬
𝑥 ∈
∅ |
42 | 33 | difeq1d 3689 |
. . . . . . . . 9
⊢ (∪ dom 𝑀 = ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = (∅
∖ { 0 })) |
43 | | 0dif 3929 |
. . . . . . . . 9
⊢ (∅
∖ { 0 }) =
∅ |
44 | 42, 43 | syl6eq 2660 |
. . . . . . . 8
⊢ (∪ dom 𝑀 = ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅) |
45 | 36 | difeq1d 3689 |
. . . . . . . . 9
⊢ (∪ dom 𝑀 ≠ ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ({ 0 } ∖ {
0
})) |
46 | | difid 3902 |
. . . . . . . . 9
⊢ ({ 0 } ∖ {
0 }) =
∅ |
47 | 45, 46 | syl6eq 2660 |
. . . . . . . 8
⊢ (∪ dom 𝑀 ≠ ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅) |
48 | 44, 47 | pm2.61ine 2865 |
. . . . . . 7
⊢ (ran
(∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅ |
49 | 48 | eleq2i 2680 |
. . . . . 6
⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↔
𝑥 ∈
∅) |
50 | 41, 49 | mtbir 312 |
. . . . 5
⊢ ¬
𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0
}) |
51 | 50 | pm2.21i 115 |
. . . 4
⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) →
(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
52 | 51 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ran (∪
dom 𝑀 × { 0 }) ∖ {
0 }))
→ (𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
53 | 52 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (ran (∪
dom 𝑀 × { 0 }) ∖ {
0
})(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
54 | | sitgval.x |
. . 3
⊢ · = (
·𝑠 ‘𝑊) |
55 | | sitgval.h |
. . 3
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
56 | | sitgval.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
57 | 14, 5, 4, 15, 54, 55, 56, 1 | issibf 29722 |
. 2
⊢ (𝜑 → ((∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀) ↔ ((∪ dom
𝑀 × { 0 }) ∈
(dom 𝑀MblFnM𝑆) ∧ ran (∪ dom 𝑀 × { 0 }) ∈ Fin ∧
∀𝑥 ∈ (ran
(∪ dom 𝑀 × { 0 }) ∖ { 0 })(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)))) |
58 | 27, 40, 53, 57 | mpbir3and 1238 |
1
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) |