| Step | Hyp | Ref
| Expression |
| 1 | | sitgval.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
| 2 | | dmmeas 34202 |
. . . 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 | 5 | fvexi 6920 |
. . . . . 6
⊢ 𝐽 ∈ V |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ V) |
| 8 | 7 | sgsiga 34143 |
. . . 4
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
| 9 | 4, 8 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
| 10 | | fconstmpt 5747 |
. . . 4
⊢ (∪ dom 𝑀 × { 0 }) = (𝑥 ∈ ∪ dom
𝑀 ↦ 0
) |
| 11 | 10 | a1i 11 |
. . 3
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) = (𝑥 ∈ ∪ dom
𝑀 ↦ 0
)) |
| 12 | | sibf0.2 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Mnd) |
| 13 | | sitgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
| 14 | | sitgval.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑊) |
| 15 | 13, 14 | mndidcl 18762 |
. . . . 5
⊢ (𝑊 ∈ Mnd → 0 ∈ 𝐵) |
| 16 | 12, 15 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐵) |
| 17 | | sibf0.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ TopSp) |
| 18 | 13, 5 | tpsuni 22942 |
. . . . . 6
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
| 19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
| 20 | 4 | unieqi 4919 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ (sigaGen‘𝐽) |
| 21 | | unisg 34144 |
. . . . . . 7
⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
| 22 | 6, 21 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
| 23 | 20, 22 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝐽) |
| 24 | 19, 23 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → 𝐵 = ∪ 𝑆) |
| 25 | 16, 24 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 0 ∈ ∪ 𝑆) |
| 26 | 3, 9, 11, 25 | mbfmcst 34261 |
. 2
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ (dom 𝑀MblFnM𝑆)) |
| 27 | | xpeq1 5699 |
. . . . . . . 8
⊢ (∪ dom 𝑀 = ∅ → (∪ dom 𝑀 × { 0 }) = (∅ × {
0
})) |
| 28 | | 0xp 5784 |
. . . . . . . 8
⊢ (∅
× { 0 }) =
∅ |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . . . 7
⊢ (∪ dom 𝑀 = ∅ → (∪ dom 𝑀 × { 0 }) =
∅) |
| 30 | 29 | rneqd 5949 |
. . . . . 6
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) = ran
∅) |
| 31 | | rn0 5936 |
. . . . . 6
⊢ ran
∅ = ∅ |
| 32 | 30, 31 | eqtrdi 2793 |
. . . . 5
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) =
∅) |
| 33 | | 0fi 9082 |
. . . . 5
⊢ ∅
∈ Fin |
| 34 | 32, 33 | eqeltrdi 2849 |
. . . 4
⊢ (∪ dom 𝑀 = ∅ → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
| 35 | | rnxp 6190 |
. . . . 5
⊢ (∪ dom 𝑀 ≠ ∅ → ran (∪ dom 𝑀 × { 0 }) = { 0 }) |
| 36 | | snfi 9083 |
. . . . 5
⊢ { 0 } ∈
Fin |
| 37 | 35, 36 | eqeltrdi 2849 |
. . . 4
⊢ (∪ dom 𝑀 ≠ ∅ → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
| 38 | 34, 37 | pm2.61ine 3025 |
. . 3
⊢ ran
(∪ dom 𝑀 × { 0 }) ∈
Fin |
| 39 | 38 | a1i 11 |
. 2
⊢ (𝜑 → ran (∪ dom 𝑀 × { 0 }) ∈
Fin) |
| 40 | | noel 4338 |
. . . . . 6
⊢ ¬
𝑥 ∈
∅ |
| 41 | 32 | difeq1d 4125 |
. . . . . . . . 9
⊢ (∪ dom 𝑀 = ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = (∅
∖ { 0 })) |
| 42 | | 0dif 4405 |
. . . . . . . . 9
⊢ (∅
∖ { 0 }) =
∅ |
| 43 | 41, 42 | eqtrdi 2793 |
. . . . . . . 8
⊢ (∪ dom 𝑀 = ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅) |
| 44 | 35 | difeq1d 4125 |
. . . . . . . . 9
⊢ (∪ dom 𝑀 ≠ ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) = ({ 0 } ∖ {
0
})) |
| 45 | | difid 4376 |
. . . . . . . . 9
⊢ ({ 0 } ∖ {
0 }) =
∅ |
| 46 | 44, 45 | eqtrdi 2793 |
. . . . . . . 8
⊢ (∪ dom 𝑀 ≠ ∅ → (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅) |
| 47 | 43, 46 | pm2.61ine 3025 |
. . . . . . 7
⊢ (ran
(∪ dom 𝑀 × { 0 }) ∖ { 0 }) =
∅ |
| 48 | 47 | eleq2i 2833 |
. . . . . 6
⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) ↔
𝑥 ∈
∅) |
| 49 | 40, 48 | mtbir 323 |
. . . . 5
⊢ ¬
𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0
}) |
| 50 | 49 | pm2.21i 119 |
. . . 4
⊢ (𝑥 ∈ (ran (∪ dom 𝑀 × { 0 }) ∖ { 0 }) →
(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
| 51 | 50 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ran (∪
dom 𝑀 × { 0 }) ∖ {
0 }))
→ (𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
| 52 | 51 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (ran (∪
dom 𝑀 × { 0 }) ∖ {
0
})(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)) |
| 53 | | sitgval.x |
. . 3
⊢ · = (
·𝑠 ‘𝑊) |
| 54 | | sitgval.h |
. . 3
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
| 55 | | sitgval.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
| 56 | 13, 5, 4, 14, 53, 54, 55, 1 | issibf 34335 |
. 2
⊢ (𝜑 → ((∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀) ↔ ((∪ dom
𝑀 × { 0 }) ∈
(dom 𝑀MblFnM𝑆) ∧ ran (∪ dom 𝑀 × { 0 }) ∈ Fin ∧
∀𝑥 ∈ (ran
(∪ dom 𝑀 × { 0 }) ∖ { 0 })(𝑀‘(◡(∪ dom 𝑀 × { 0 }) “ {𝑥})) ∈
(0[,)+∞)))) |
| 57 | 26, 39, 52, 56 | mpbir3and 1343 |
1
⊢ (𝜑 → (∪ dom 𝑀 × { 0 }) ∈ dom (𝑊sitg𝑀)) |