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 |
7
|
elexd |
⊢ ( 𝜑 → 𝑊 ∈ V ) |
10 |
|
2fveq3 |
⊢ ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) ) |
11 |
2
|
fveq2i |
⊢ ( sigaGen ‘ 𝐽 ) = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) |
12 |
3 11
|
eqtri |
⊢ 𝑆 = ( sigaGen ‘ ( TopOpen ‘ 𝑊 ) ) |
13 |
10 12
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) = 𝑆 ) |
14 |
13
|
oveq2d |
⊢ ( 𝑤 = 𝑊 → ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) = ( dom 𝑚 MblFnM 𝑆 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) ) |
16 |
15 4
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = 0 ) |
17 |
16
|
sneqd |
⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ 𝑤 ) } = { 0 } ) |
18 |
17
|
difeq2d |
⊢ ( 𝑤 = 𝑊 → ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) = ( ran 𝑔 ∖ { 0 } ) ) |
19 |
18
|
raleqdv |
⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) |
20 |
19
|
anbi2d |
⊢ ( 𝑤 = 𝑊 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) ) |
21 |
14 20
|
rabeqbidv |
⊢ ( 𝑤 = 𝑊 → { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ) |
22 |
|
id |
⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 ) |
23 |
17
|
difeq2d |
⊢ ( 𝑤 = 𝑊 → ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) = ( ran 𝑓 ∖ { 0 } ) ) |
24 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) ) |
25 |
24 5
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · ) |
26 |
|
2fveq3 |
⊢ ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) ) |
27 |
26 6
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) = 𝐻 ) |
28 |
27
|
fveq1d |
⊢ ( 𝑤 = 𝑊 → ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ) |
29 |
|
eqidd |
⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 ) |
30 |
25 28 29
|
oveq123d |
⊢ ( 𝑤 = 𝑊 → ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) = ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) |
31 |
23 30
|
mpteq12dv |
⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) |
32 |
22 31
|
oveq12d |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) |
33 |
21 32
|
mpteq12dv |
⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ) |
34 |
|
dmeq |
⊢ ( 𝑚 = 𝑀 → dom 𝑚 = dom 𝑀 ) |
35 |
34
|
oveq1d |
⊢ ( 𝑚 = 𝑀 → ( dom 𝑚 MblFnM 𝑆 ) = ( dom 𝑀 MblFnM 𝑆 ) ) |
36 |
|
fveq1 |
⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ) |
37 |
36
|
eleq1d |
⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) |
38 |
37
|
ralbidv |
⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) |
39 |
38
|
anbi2d |
⊢ ( 𝑚 = 𝑀 → ( ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) ) ) |
40 |
35 39
|
rabeqbidv |
⊢ ( 𝑚 = 𝑀 → { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } = { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ) |
41 |
|
simpl |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → 𝑚 = 𝑀 ) |
42 |
41
|
fveq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) = ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) |
43 |
42
|
fveq2d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ) |
44 |
43
|
oveq1d |
⊢ ( ( 𝑚 = 𝑀 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) = ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) |
45 |
44
|
mpteq2dva |
⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) |
46 |
45
|
oveq2d |
⊢ ( 𝑚 = 𝑀 → ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) |
47 |
40 46
|
mpteq12dv |
⊢ ( 𝑚 = 𝑀 → ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ) |
48 |
|
df-sitg |
⊢ sitg = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) ) |
49 |
|
ovex |
⊢ ( dom 𝑀 MblFnM 𝑆 ) ∈ V |
50 |
49
|
mptrabex |
⊢ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ∈ V |
51 |
33 47 48 50
|
ovmpo |
⊢ ( ( 𝑊 ∈ V ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ) |
52 |
9 8 51
|
syl2anc |
⊢ ( 𝜑 → ( 𝑊 sitg 𝑀 ) = ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑀 MblFnM 𝑆 ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { 0 } ) ( 𝑀 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ↦ ( ( 𝐻 ‘ ( 𝑀 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) · 𝑥 ) ) ) ) ) |