Step |
Hyp |
Ref |
Expression |
1 |
|
sitgval.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
sitgval.j |
⊢ 𝐽 = ( TopOpen ‘ 𝑊 ) |
3 |
|
sitgval.s |
⊢ 𝑆 = ( sigaGen ‘ 𝐽 ) |
4 |
|
sitgval.0 |
⊢ 0 = ( 0g ‘ 𝑊 ) |
5 |
|
sitgval.x |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
6 |
|
sitgval.h |
⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) |
7 |
|
sitgval.1 |
⊢ ( 𝜑 → 𝑊 ∈ 𝑉 ) |
8 |
|
sitgval.2 |
⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures ) |
9 |
|
sitg0.1 |
⊢ ( 𝜑 → 𝑊 ∈ TopSp ) |
10 |
|
sitg0.2 |
⊢ ( 𝜑 → 𝑊 ∈ Mnd ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
sibf0 |
⊢ ( 𝜑 → ( ∪ dom 𝑀 × { 0 } ) ∈ dom ( 𝑊 sitg 𝑀 ) ) |
12 |
1 2 3 4 5 6 7 8 11
|
sitgfval |
⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ ( ∪ dom 𝑀 × { 0 } ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) |
13 |
|
rnxpss |
⊢ ran ( ∪ dom 𝑀 × { 0 } ) ⊆ { 0 } |
14 |
|
ssdif0 |
⊢ ( ran ( ∪ dom 𝑀 × { 0 } ) ⊆ { 0 } ↔ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ ) |
15 |
13 14
|
mpbi |
⊢ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ |
16 |
|
mpteq1 |
⊢ ( ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) = ∅ → ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) |
17 |
15 16
|
ax-mp |
⊢ ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) |
18 |
|
mpt0 |
⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ∅ |
19 |
17 18
|
eqtri |
⊢ ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) = ∅ |
20 |
19
|
oveq2i |
⊢ ( 𝑊 Σg ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σg ∅ ) |
21 |
4
|
gsum0 |
⊢ ( 𝑊 Σg ∅ ) = 0 |
22 |
20 21
|
eqtri |
⊢ ( 𝑊 Σg ( 𝑥 ∈ ( ran ( ∪ dom 𝑀 × { 0 } ) ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ ( ∪ dom 𝑀 × { 0 } ) “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = 0 |
23 |
12 22
|
eqtrdi |
⊢ ( 𝜑 → ( ( 𝑊 sitg 𝑀 ) ‘ ( ∪ dom 𝑀 × { 0 } ) ) = 0 ) |